Metamath Proof Explorer

Theorem cramerimp

Description: One direction of 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 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."): The ith component of the solution vector of a system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the righthand side vector of the system of linear equations divided by the determinant of the matrix of the system of linear equations. (Contributed by AV, 19-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramerimp.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cramerimp.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cramerimp.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
cramerimp.e ⊢ 𝐸 = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
cramerimp.h ⊢ 𝐻 = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 )
cramerimp.x ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
cramerimp.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
cramerimp.q ⊢ / = ( /r ‘ 𝑅 )
Assertion cramerimp ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝐷 ‘ 𝐻 ) / ( 𝐷 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cramerimp.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cramerimp.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cramerimp.v ⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4 cramerimp.e ⊢ 𝐸 = ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
5 cramerimp.h ⊢ 𝐻 = ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 )
6 cramerimp.x ⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
7 cramerimp.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
8 cramerimp.q ⊢ / = ( /r ‘ 𝑅 )
9 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 9 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ Ring )
11 10 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 7 1 2 12 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
14 13 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
15 14 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
16 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
17 16 simpld ⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
18 17 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑁 ∈ Fin )
19 10 18 anim12i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
20 19 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
21 ne0i ⊢ ( 𝐼 ∈ 𝑁 → 𝑁 ≠ ∅ )
22 9 21 anim12ci ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) )
23 22 anim1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
24 23 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) )
25 simpl ⊢ ( ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
26 25 3ad2ant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
27 1 2 3 6 slesolvec ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 → 𝑍 ∈ 𝑉 ) )
28 24 26 27 sylc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝑍 ∈ 𝑉 )
29 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
30 29 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝐼 ∈ 𝑁 )
31 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
32 1 2 3 31 ma1repvcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁 ) ) → ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
33 20 28 30 32 syl12anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 1r ‘ 𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
34 4 33 eqeltrid ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝐸 ∈ 𝐵 )
35 15 34 ffvelrnd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) )
36 simpr ⊢ ( ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
37 36 3ad2ant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
38 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
39 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
40 12 38 8 39 dvrcan3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( 𝐷 ‘ 𝐸 ) )
41 11 35 37 40 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( 𝐷 ‘ 𝐸 ) )
42 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ CRing )
43 42 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → 𝑅 ∈ CRing )
44 12 38 unitcl ⊢ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
45 44 adantl ⊢ ( ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
46 45 3ad2ant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
47 12 39 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) )
48 43 35 46 47 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) )
49 48 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐷 ‘ 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑋 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
50 18 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑁 ∈ Fin )
51 42 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑅 ∈ CRing )
52 29 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐼 ∈ 𝑁 )
53 50 51 52 3jca ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) )
54 53 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) )
55 1 3 4 7 cramerimplem1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑍 ‘ 𝐼 ) )
56 54 28 55 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑍 ‘ 𝐼 ) )
57 41 49 56 3eqtr3rd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) / ( 𝐷 ‘ 𝑋 ) ) )
58 1 2 3 4 5 6 7 39 cramerimplem3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) = ( 𝐷 ‘ 𝐻 ) )
59 58 3adant3r ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) = ( 𝐷 ‘ 𝐻 ) )
60 59 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( ( 𝐷 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝐸 ) ) / ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐷 ‘ 𝐻 ) / ( 𝐷 ‘ 𝑋 ) ) )
61 57 60 eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑋 · 𝑍 ) = 𝑌 ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑍 ‘ 𝐼 ) = ( ( 𝐷 ‘ 𝐻 ) / ( 𝐷 ‘ 𝑋 ) ) )