Metamath Proof Explorer


Theorem cramerimplem1

Description: Lemma 1 for cramerimp : The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019) (Revised by AV, 5-Jul-2022)

Ref Expression
Hypotheses cramerimplem1.a 𝐴 = ( 𝑁 Mat 𝑅 )
cramerimplem1.v 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
cramerimplem1.e 𝐸 = ( ( ( 1r𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
cramerimplem1.d 𝐷 = ( 𝑁 maDet 𝑅 )
Assertion cramerimplem1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐷𝐸 ) = ( 𝑍𝐼 ) )

Proof

Step Hyp Ref Expression
1 cramerimplem1.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 cramerimplem1.v 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
3 cramerimplem1.e 𝐸 = ( ( ( 1r𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 )
4 cramerimplem1.d 𝐷 = ( 𝑁 maDet 𝑅 )
5 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
7 6 ancomd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
8 7 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
9 simp3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝐼𝑁 )
10 9 anim1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐼𝑁𝑍𝑉 ) )
11 1 fveq2i ( 1r𝐴 ) = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
12 2 11 3 1marepvmarrepid ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼𝑁𝑍𝑉 ) ) → ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) = 𝐸 )
13 8 10 12 syl2an2r ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) = 𝐸 )
14 13 eqcomd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → 𝐸 = ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) )
15 14 fveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐷𝐸 ) = ( 𝐷 ‘ ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) ) )
16 4 a1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → 𝐷 = ( 𝑁 maDet 𝑅 ) )
17 16 fveq1d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐷 ‘ ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) ) = ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) ) )
18 simpl2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → 𝑅 ∈ CRing )
19 9 anim1ci ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝑍𝑉𝐼𝑁 ) )
20 1 eqcomi ( 𝑁 Mat 𝑅 ) = 𝐴
21 20 fveq2i ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ 𝐴 )
22 eqid ( 1r𝐴 ) = ( 1r𝐴 )
23 1 21 2 22 ma1repvcl ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑍𝑉𝐼𝑁 ) ) → ( ( ( 1r𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
24 8 19 23 syl2an2r ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( ( 1r𝐴 ) ( 𝑁 matRepV 𝑅 ) 𝑍 ) ‘ 𝐼 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
25 3 24 eqeltrid ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → 𝐸 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
26 9 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → 𝐼𝑁 )
27 elmapi ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → 𝑍 : 𝑁 ⟶ ( Base ‘ 𝑅 ) )
28 ffvelrn ( ( 𝑍 : 𝑁 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼𝑁 ) → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) )
29 28 ex ( 𝑍 : 𝑁 ⟶ ( Base ‘ 𝑅 ) → ( 𝐼𝑁 → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
30 27 29 syl ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) → ( 𝐼𝑁 → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
31 30 2 eleq2s ( 𝑍𝑉 → ( 𝐼𝑁 → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
32 31 com12 ( 𝐼𝑁 → ( 𝑍𝑉 → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
33 32 3ad2ant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → ( 𝑍𝑉 → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) )
34 33 imp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) )
35 smadiadetr ( ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) ∧ ( 𝐼𝑁 ∧ ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) ) = ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) ) ) )
36 18 25 26 34 35 syl22anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) ) = ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) ) ) )
37 17 36 eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐷 ‘ ( 𝐼 ( 𝐸 ( 𝑁 matRRep 𝑅 ) ( 𝑍𝐼 ) ) 𝐼 ) ) = ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) ) ) )
38 2 11 3 1marepvsma1 ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼𝑁𝑍𝑉 ) ) → ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) = ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) )
39 8 10 38 syl2an2r ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) = ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) )
40 39 fveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) ) = ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) ) )
41 40 oveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) ) ) = ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) ) ) )
42 diffi ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
43 42 anim1ci ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 ∈ CRing ∧ ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ) )
44 43 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → ( 𝑅 ∈ CRing ∧ ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ) )
45 44 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝑅 ∈ CRing ∧ ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ) )
46 eqid ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) = ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 )
47 eqid ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) = ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 )
48 eqid ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) = ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) )
49 eqid ( 1r𝑅 ) = ( 1r𝑅 )
50 46 47 48 49 mdet1 ( ( 𝑅 ∈ CRing ∧ ( 𝑁 ∖ { 𝐼 } ) ∈ Fin ) → ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) ) = ( 1r𝑅 ) )
51 45 50 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) ) = ( 1r𝑅 ) )
52 51 oveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 1r ‘ ( ( 𝑁 ∖ { 𝐼 } ) Mat 𝑅 ) ) ) ) = ( ( 𝑍𝐼 ) ( .r𝑅 ) ( 1r𝑅 ) ) )
53 5 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) → 𝑅 ∈ Ring )
54 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
55 eqid ( .r𝑅 ) = ( .r𝑅 )
56 54 55 49 ringridm ( ( 𝑅 ∈ Ring ∧ ( 𝑍𝐼 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑍𝐼 ) ( .r𝑅 ) ( 1r𝑅 ) ) = ( 𝑍𝐼 ) )
57 53 34 56 syl2an2r ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( 𝑍𝐼 ) ( .r𝑅 ) ( 1r𝑅 ) ) = ( 𝑍𝐼 ) )
58 41 52 57 3eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( ( 𝑍𝐼 ) ( .r𝑅 ) ( ( ( 𝑁 ∖ { 𝐼 } ) maDet 𝑅 ) ‘ ( 𝐼 ( ( 𝑁 subMat 𝑅 ) ‘ 𝐸 ) 𝐼 ) ) ) = ( 𝑍𝐼 ) )
59 15 37 58 3eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼𝑁 ) ∧ 𝑍𝑉 ) → ( 𝐷𝐸 ) = ( 𝑍𝐼 ) )