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 ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑍 ‘ 𝐼 ) )