Theorem cramer

Description: Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule : "[Cramer's rule] ... expresses the [unique solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp ). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit or slesolinv . For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in Lang p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019) (Revised by Alexander van der Vekens, 1-Mar-2019)

	Ref	Expression
Hypotheses	cramer.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cramer.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cramer.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
	cramer.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	cramer.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	cramer.q	⊢ / = ( /r ‘ 𝑅 )
Assertion	cramer	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ↔ ( 𝑋 · 𝑍 ) = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cramer.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cramer.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cramer.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4		cramer.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
5		cramer.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
6		cramer.q	⊢ / = ( /r ‘ 𝑅 )
7		pm3.22	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) → ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) )
8	1 2 3 4 5 6	cramerlem3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )
9	7 8	syl3an1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 ) )
10		simpl1l	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑅 ∈ CRing )
11		simpl2	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) )
12		simpl3	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
13		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14	13	anim1ci	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) → ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) )
15	14	anim1i	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
16	15	3adant3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
17	1 2 3 5	slesolvec	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
18	17	imp	⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 ∈ 𝑉 )
19	16 18	sylan	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 ∈ 𝑉 )
20		simpr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
21	1 2 3 4 5 6	cramerlem1	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑍 ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )
22	10 11 12 19 20 21	syl113anc	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) )
23	22	ex	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ) )
24	9 23	impbid	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑍 = ( 𝑖 ∈ 𝑁 ↦ ( ( 𝐷 ‘ ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝑖 ) ) / ( 𝐷 ‘ 𝑋 ) ) ) ↔ ( 𝑋 · 𝑍 ) = 𝑌 ) )