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 
|- A = ( N Mat R )
cramerimplem1.v 
|- V = ( ( Base ` R ) ^m N )
cramerimplem1.e 
|- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )
cramerimplem1.d 
|- D = ( N maDet R )
Assertion cramerimplem1 
|- ( ( ( N e. Fin /\ R e. CRing /\ I e. N ) /\ Z e. V ) -> ( D ` E ) = ( Z ` I ) )

Proof

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