Main derivation
S01 · equivalent
Before
L(x,y)=z
After
ax+by=c\ \land\ dx+ey=f
Conditions: none
Rule: solution_def · Uses: G1, solution_def, mko_linear_system
Leaf basis: solution_def + cartesian_product_def + eq_congruence
By the MKO, the solution set is described by L(x,y)=z. L(x,y)=(ax+by−c, dx+ey−f) equals z=(0,0) exactly when both components are 0, i.e. ax+by−c=0 and dx+ey−f=0, which after adding the constants to both sides says both equations hold at once. So 'solution' always means an (x,y) satisfying both rows.
S02 · equivalent
Before
D=ae-bd
After
D=2\cdot(-1)-3\cdot 1=-5\neq 0
Conditions: none
Rule: numeric_evaluation · Uses: G2
Leaf basis: numeric_evaluation
Substitute a=2, b=3, d=1, e=−1: D=2·(−1)−3·1=−2−3=−5, which is nonzero.
S03 · theorem_application
Before
D=-5\neq 0
After
x=\frac{7\cdot(-1)-3\cdot 1}{-5}=2,\quad y=\frac{2\cdot 1-7\cdot 1}{-5}=1Conditions: D\neq 0
Rule: L_cramer · Uses: S02, G2, L_cramer
Leaf basis: eq_congruence + distributive + mul_inverse_nonzero + frac_rules
Since D≠0, Lemma L_cramer applies: System I has exactly one solution, x=(ce−bf)/D=(−7−3)/(−5)=2 and y=(af−cd)/D=(2−7)/(−5)=1. So the unique solution is (2,1). The lemma is proved in sub-steps S03.1 to S03.4.
S04 · implies
Before
(x,y)=(2,1)
After
2\cdot 2+3\cdot 1=7\ \land\ 2-1=1
Conditions: none
Rule: numeric_evaluation · Uses: S03, G2, solution_def
Leaf basis: numeric_evaluation + solution_def
Independent check: substitute (2,1) into both rows; row one gives 4+3=7 and row two gives 2−1=1, so both rows hold. This step does not depend on the formula and can catch arithmetic slips made in applying it.
S05 · implies
Before
(x,y)=(5,-1)
After
2\cdot 5+3\cdot(-1)=7,\ \ 5-(-1)=6\neq 1
Conditions: none
Rule: solution_def · Uses: G2, solution_def
Leaf basis: solution_def + numeric_evaluation
The one-row trap: (5,−1) satisfies row one (10−3=7), but row two gives 5−(−1)=6≠1. By the definition of a solution both rows must hold at once, so (5,−1) is not a solution of System I. This agrees with the unique solution (2,1) of S03.
S06 · implies
Before
x+2y=3,\ 2x+4y=7
After
D=1\cdot 4-2\cdot 2=0
Conditions: none
Rule: mko_linear_system · Uses: G3, mko_linear_system
Leaf basis: mko_linear_system + numeric_evaluation
System II has D=1·4−2·2=0, so L_cramer does not apply and the division in the formula is undefined. By the MKO, consistency must be checked separately when D=0. (Its Cramer numerator ce−bf=3·4−2·7=−2≠0, but this guide does not use numerators as the criterion; S07 decides directly by a row operation.)
S07 · equivalent
Before
x+2y=3\ \land\ 2x+4y=7
After
x+2y=3\ \land\ 0x+0y=1
Conditions: \lambda=2
Rule: L_row_replace · Uses: S06, L_row_replace
Leaf basis: eq_congruence + distributive + numeric_evaluation
By Lemma L_row_replace with λ=2, replace row two by row two minus 2 times row one: (2−2·1)x+(4−2·2)y=7−2·3, that is 0x+0y=1. The new system has the same solution set as the original.
S08 · implies
Before
0x+0y=1
After
0=1\ \text{for every}\ (x,y),\ \text{solution set of II}=\varnothingConditions: none
Rule: mul_zero · Uses: S07, mul_zero, add_zero
Leaf basis: mul_zero + add_zero + numeric_evaluation
For every (x,y), 0x+0y=0+0=0 (multiplying by zero, additive identity), so 0x+0y=1 demands 0=1, which no (x,y) satisfies. By the equivalence in S07, System II has no solution. MKO assumption a2: a zero row 0=c with c≠0 is inconsistent.
S09 · equivalent
Before
x+2y=3\ \land\ 2x+4y=6
After
x+2y=3\ \land\ 0x+0y=0\ \Leftrightarrow\ x+2y=3
Conditions: \lambda=2
Rule: L_row_replace · Uses: G3, L_row_replace, mul_zero, add_zero
Leaf basis: eq_congruence + distributive + mul_zero + add_zero + and_intro_elim
System III also has D=1·4−2·2=0. The same row operation with λ=2 turns row two into 0x+0y=6−2·3=0. For every (x,y), 0x+0y=0 always holds and imposes no restriction (MKO assumption a2), so System III is equivalent to the single equation x+2y=3.
S10 · equivalent
Before
\{(x,y)\in\mathbb{R}^2\mid x+2y=3\}After
\{(3-2t,\,t)\mid t\in\mathbb{R}\}Conditions: none
Rule: set_extensionality · Uses: S09, set_extensionality
Leaf basis: set_extensionality + eq_congruence + add_inverse + numeric_evaluation
⊆: if x+2y=3, take t=y; then x=3−2t (subtract 2y from both sides), so (x,y)=(3−2t,t). ⊇: for every real t, (3−2t)+2t=3 (N17), so (3−2t,t) is a solution. Both directions hold, so the two sets are equal.
S11 · implies
Before
\{(3-2t,\,t)\mid t\in\mathbb{R}\}After
\text{infinitely many solutions, e.g.}\ (3,0),\ (1,1)Conditions: none
Rule: cartesian_product_def · Uses: S10, cartesian_product_def
Leaf basis: cartesian_product_def + injective_surjective_def + numeric_evaluation
Different values of t give different solutions, because the second component is t itself (equal ordered pairs need equal second components). ℝ has infinitely many elements, so System III has infinitely many solutions. For example t=0 gives (3,0) and t=1 gives (1,1); both satisfy both original rows: 3+0=3, 6+0=6; 1+2=3, 2+4=6 (N18 checks row two for general t).
S12 · implies
Before
0x+0y=1,\ 0x+0y=2
After
D=0,\ ce-bf=0,\ af-cd=0,\ \text{yet no solution}Conditions: none
Rule: mul_zero · Uses: G3, mul_zero, add_zero
Leaf basis: mul_zero + add_zero + numeric_evaluation
System IV: a=b=d=e=0, c=1, f=2. D=0·0−0·0=0, ce−bf=1·0−0·2=0, af−cd=0·2−1·0=0, all three zero. Yet row one reads 0=1 for every (x,y), which is false, so the system has no solution. Hence 'D and both Cramer numerators are zero' does not imply infinitely many solutions; inconsistent zero rows must be checked first (MKO paragraph three).
S13 · implies
Before
\text{S03, S04, S08, S10, S11, S12}After
\text{I}:\ \{(2,1)\};\ \text{II}:\ \varnothing;\ \text{III}:\ \{(3-2t,t)\mid t\in\mathbb{R}\};\ \text{IV}:\ \varnothingConditions: none
Rule: and_intro_elim · Uses: S03, S04, S08, S10, S11, S12
Leaf basis: and_intro_elim
Summary: System I has D=−5≠0 and the unique solution (2,1), checked in both rows; System II has D=0 and a row operation produces 0=1, so no solution; System III has D=0 and the row operation gives 0=0, with solution set {(3−2t,t) ∣ t∈ℝ}, infinitely many; System IV has all three determinant values zero yet no solution.
Substeps and lemmas
S03.1 · implies
Before
ax+by=c\ \land\ dx+ey=f
After
(ae-bd)x=ce-bf
Conditions: none
Rule: eq_congruence · Uses: eq_congruence, distributive
Leaf basis: eq_congruence + distributive + mul_comm + add_inverse
Let (x,y) be a solution. Multiply row one by e and row two by b, then subtract: e(ax+by)−b(dx+ey)=ec−bf. The left side expands to aex+bey−bdx−bey=(ae−bd)x (N4 checks this identity). So every solution satisfies (ae−bd)x=ce−bf.
S03.2 · implies
Before
ax+by=c\ \land\ dx+ey=f
After
(ae-bd)y=af-cd
Conditions: none
Rule: eq_congruence · Uses: eq_congruence, distributive
Leaf basis: eq_congruence + distributive + mul_comm + add_inverse
Likewise eliminate x: multiply row two by a and row one by d, then subtract: a(dx+ey)−d(ax+by)=af−dc. The left side expands to adx+aey−adx−bdy=(ae−bd)y (N5). So every solution satisfies (ae−bd)y=af−cd.
S03.3 · implies
Before
Dx=ce-bf,\quad Dy=af-cd,\quad D\neq 0
After
x=\frac{ce-bf}{D},\quad y=\frac{af-cd}{D}Conditions: D\neq 0
Rule: mul_inverse_nonzero · Uses: S03.1, S03.2, mul_inverse_nonzero
Leaf basis: mul_inverse_nonzero + eq_congruence + mul_assoc + mul_one
Since D≠0, 1/D exists, and multiplying both equations by 1/D gives the values of x and y. So every solution equals this pair: there is at most one solution (uniqueness). If D=0 there is no 1/D and the step cannot be taken, which is exactly why the MKO forbids the unique-solution division when D=0.
S03.4 · implies
Before
x_0=\frac{ce-bf}{D},\ y_0=\frac{af-cd}{D}After
ax_0+by_0=c\ \land\ dx_0+ey_0=f
Conditions: D\neq 0
Rule: frac_rules · Uses: frac_rules, distributive
Leaf basis: frac_rules + distributive + mul_comm + add_inverse + mul_inverse_nonzero
Existence: substituting into row one, ax₀+by₀=(a(ce−bf)+b(af−cd))/D=(ace−abf+abf−bcd)/D=c(ae−bd)/D=c; into row two, dx₀+ey₀=(d(ce−bf)+e(af−cd))/D=(cde−bdf+aef−cde)/D=f(ae−bd)/D=f (N6 and N7 check the two identities). S03.1 to S03.4 together prove Lemma L_cramer: when D≠0 there is exactly one solution.
S07.1 · equivalent
Before
ax+by=c\ \land\ dx+ey=f
After
ax+by=c\ \land\ (d-\lambda a)x+(e-\lambda b)y=f-\lambda c
Conditions: none
Rule: eq_congruence · Uses: eq_congruence, distributive
Leaf basis: eq_congruence + distributive + add_inverse + add_assoc
⇒: assume both rows. Multiplying row one by λ gives λ(ax+by)=λc; subtracting this from both sides of row two gives (dx+ey)−λ(ax+by)=f−λc, which distributivity rearranges to (d−λa)x+(e−λb)y=f−λc; row one is kept. ⇐: assume the new system and add λ times row one back to the new row two, giving dx+ey=f. Both directions only apply the same operation to both sides of an equation. This proves Lemma L_row_replace.