Metamath Proof Explorer


Theorem cramerimplem2

Description: Lemma 2 for cramerimp : The matrix of a system of linear equations multiplied with the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the matrix of the system of linear equations with the ith column replaced by the right-hand side vector 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.m × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
Assertion cramerimplem2 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = 𝐻 )

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.m × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
8 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ( .r𝑅 ) = ( .r𝑅 )
10 simpl ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝑅 ∈ CRing )
11 10 3ad2ant1 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑅 ∈ CRing )
12 1 2 matrcl ( 𝑋𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
13 12 simpld ( 𝑋𝐵𝑁 ∈ Fin )
14 13 adantr ( ( 𝑋𝐵𝑌𝑉 ) → 𝑁 ∈ Fin )
15 14 3ad2ant2 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑁 ∈ Fin )
16 13 anim2i ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) )
17 16 ancomd ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
18 1 8 matbas2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
19 17 18 syl ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
20 2 19 eqtr4id ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
21 20 eleq2d ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑋𝐵𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
22 21 biimpd ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( 𝑋𝐵𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
23 22 ex ( 𝑅 ∈ CRing → ( 𝑋𝐵 → ( 𝑋𝐵𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) )
24 23 adantr ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → ( 𝑋𝐵 → ( 𝑋𝐵𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) )
25 24 com12 ( 𝑋𝐵 → ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → ( 𝑋𝐵𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) )
26 25 pm2.43a ( 𝑋𝐵 → ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
27 26 adantr ( ( 𝑋𝐵𝑌𝑉 ) → ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) )
28 27 impcom ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
29 28 3adant3 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
30 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
31 30 adantr ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝑅 ∈ Ring )
32 31 14 anim12i ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
33 32 3adant3 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
34 ne0i ( 𝐼𝑁𝑁 ≠ ∅ )
35 34 adantl ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝑁 ≠ ∅ )
36 35 3ad2ant1 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑁 ≠ ∅ )
37 15 15 36 3jca ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) )
38 3 eleq2i ( 𝑌𝑉𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
39 38 biimpi ( 𝑌𝑉𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
40 39 adantl ( ( 𝑋𝐵𝑌𝑉 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
41 10 40 anim12i ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ) → ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
42 41 3adant3 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
43 simp3 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
44 eqid ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) )
45 eqid ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
46 8 44 3 6 45 mavmulsolcl ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌𝑍𝑉 ) )
47 46 imp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ∧ ( 𝑅 ∈ CRing ∧ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍𝑉 )
48 37 42 43 47 syl21anc ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍𝑉 )
49 simpr ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝐼𝑁 )
50 49 3ad2ant1 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐼𝑁 )
51 eqid ( 1r𝐴 ) = ( 1r𝐴 )
52 1 2 3 51 ma1repvcl ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍𝑉𝐼𝑁 ) ) → ( ( ( 1r𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ 𝐵 )
53 4 52 eqeltrid ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍𝑉𝐼𝑁 ) ) → 𝐸𝐵 )
54 33 48 50 53 syl12anc ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐸𝐵 )
55 20 eqcomd ( ( 𝑅 ∈ CRing ∧ 𝑋𝐵 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
56 55 ad2ant2r ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
57 56 3adant3 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
58 54 57 eleqtrrd ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝐸 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
59 7 8 9 11 15 15 15 29 58 mamuval ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑅 Σg ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) ) )
60 31 3ad2ant1 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑅 ∈ Ring )
61 60 3ad2ant1 ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑅 ∈ Ring )
62 simpl ( ( 𝑋𝐵𝑌𝑉 ) → 𝑋𝐵 )
63 62 3ad2ant2 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑋𝐵 )
64 63 48 50 3jca ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋𝐵𝑍𝑉𝐼𝑁 ) )
65 64 3ad2ant1 ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑋𝐵𝑍𝑉𝐼𝑁 ) )
66 simp2 ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑖𝑁 )
67 simp3 ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑗𝑁 )
68 43 3ad2ant1 ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑋 · 𝑍 ) = 𝑌 )
69 eqid ( 0g𝑅 ) = ( 0g𝑅 )
70 1 2 3 51 69 4 6 mulmarep1gsum2 ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝐵𝑍𝑉𝐼𝑁 ) ∧ ( 𝑖𝑁𝑗𝑁 ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → ( 𝑅 Σg ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑌𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) )
71 61 65 66 67 68 70 syl113anc ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑅 Σg ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) = if ( 𝑗 = 𝐼 , ( 𝑌𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) )
72 71 mpoeq3dva ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝑅 Σg ( 𝑙𝑁 ↦ ( ( 𝑖 𝑋 𝑙 ) ( .r𝑅 ) ( 𝑙 𝐸 𝑗 ) ) ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
73 simpr ( ( 𝑋𝐵𝑌𝑉 ) → 𝑌𝑉 )
74 73 3ad2ant2 ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑌𝑉 )
75 eqid ( 𝑁 matRepV 𝑅 ) = ( 𝑁 matRepV 𝑅 )
76 1 2 75 3 marepvval ( ( 𝑋𝐵𝑌𝑉𝐼𝑁 ) → ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
77 63 74 50 76 syl3anc ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝑋 ( 𝑁 matRepV 𝑅 ) 𝑌 ) ‘ 𝐼 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) )
78 5 77 eqtr2id ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑗 = 𝐼 , ( 𝑌𝑖 ) , ( 𝑖 𝑋 𝑗 ) ) ) = 𝐻 )
79 59 72 78 3eqtrd ( ( ( 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ ( 𝑋𝐵𝑌𝑉 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 × 𝐸 ) = 𝐻 )