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 
|- A = ( N Mat R )
cramerimp.b 
|- B = ( Base ` A )
cramerimp.v 
|- V = ( ( Base ` R ) ^m N )
cramerimp.e 
|- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )
cramerimp.h 
|- H = ( ( X ( N matRepV R ) Y ) ` I )
cramerimp.x 
|- .x. = ( R maVecMul <. N , N >. )
cramerimp.m 
|- .X. = ( R maMul <. N , N , N >. )
Assertion cramerimplem2 
|- ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .X. E ) = H )

Proof

Step Hyp Ref Expression
1 cramerimp.a 
 |-  A = ( N Mat R )
2 cramerimp.b 
 |-  B = ( Base ` A )
3 cramerimp.v 
 |-  V = ( ( Base ` R ) ^m N )
4 cramerimp.e 
 |-  E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )
5 cramerimp.h 
 |-  H = ( ( X ( N matRepV R ) Y ) ` I )
6 cramerimp.x 
 |-  .x. = ( R maVecMul <. N , N >. )
7 cramerimp.m 
 |-  .X. = ( R maMul <. N , N , N >. )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 simpl 
 |-  ( ( R e. CRing /\ I e. N ) -> R e. CRing )
11 10 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> R e. CRing )
12 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
13 12 simpld 
 |-  ( X e. B -> N e. Fin )
14 13 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> N e. Fin )
15 14 3ad2ant2 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> N e. Fin )
16 13 anim2i 
 |-  ( ( R e. CRing /\ X e. B ) -> ( R e. CRing /\ N e. Fin ) )
17 16 ancomd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( N e. Fin /\ R e. CRing ) )
18 1 8 matbas2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
19 17 18 syl 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
20 2 19 eqtr4id 
 |-  ( ( R e. CRing /\ X e. B ) -> B = ( ( Base ` R ) ^m ( N X. N ) ) )
21 20 eleq2d 
 |-  ( ( R e. CRing /\ X e. B ) -> ( X e. B <-> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) )
22 21 biimpd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) )
23 22 ex 
 |-  ( R e. CRing -> ( X e. B -> ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) )
24 23 adantr 
 |-  ( ( R e. CRing /\ I e. N ) -> ( X e. B -> ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) )
25 24 com12 
 |-  ( X e. B -> ( ( R e. CRing /\ I e. N ) -> ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) )
26 25 pm2.43a 
 |-  ( X e. B -> ( ( R e. CRing /\ I e. N ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) )
27 26 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> ( ( R e. CRing /\ I e. N ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) )
28 27 impcom 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
29 28 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
30 crngring 
 |-  ( R e. CRing -> R e. Ring )
31 30 adantr 
 |-  ( ( R e. CRing /\ I e. N ) -> R e. Ring )
32 31 14 anim12i 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( R e. Ring /\ N e. Fin ) )
33 32 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( R e. Ring /\ N e. Fin ) )
34 ne0i 
 |-  ( I e. N -> N =/= (/) )
35 34 adantl 
 |-  ( ( R e. CRing /\ I e. N ) -> N =/= (/) )
36 35 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> N =/= (/) )
37 15 15 36 3jca 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( N e. Fin /\ N e. Fin /\ N =/= (/) ) )
38 3 eleq2i 
 |-  ( Y e. V <-> Y e. ( ( Base ` R ) ^m N ) )
39 38 bilani 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. ( ( Base ` R ) ^m N ) )
40 10 39 anim12i 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) )
41 40 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) )
42 simp3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .x. Z ) = Y )
43 eqid 
 |-  ( ( Base ` R ) ^m ( N X. N ) ) = ( ( Base ` R ) ^m ( N X. N ) )
44 eqid 
 |-  ( ( Base ` R ) ^m N ) = ( ( Base ` R ) ^m N )
45 8 43 3 6 44 mavmulsolcl 
 |-  ( ( ( N e. Fin /\ N e. Fin /\ N =/= (/) ) /\ ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
46 45 imp 
 |-  ( ( ( ( N e. Fin /\ N e. Fin /\ N =/= (/) ) /\ ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) ) /\ ( X .x. Z ) = Y ) -> Z e. V )
47 37 41 42 46 syl21anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> Z e. V )
48 simpr 
 |-  ( ( R e. CRing /\ I e. N ) -> I e. N )
49 48 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> I e. N )
50 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
51 1 2 3 50 ma1repvcl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( Z e. V /\ I e. N ) ) -> ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I ) e. B )
52 4 51 eqeltrid 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( Z e. V /\ I e. N ) ) -> E e. B )
53 33 47 49 52 syl12anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> E e. B )
54 20 eqcomd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
55 54 ad2ant2r 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
56 55 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
57 53 56 eleqtrrd 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> E e. ( ( Base ` R ) ^m ( N X. N ) ) )
58 7 8 9 11 15 15 15 29 57 mamuval 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .X. E ) = ( i e. N , j e. N |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l E j ) ) ) ) ) )
59 31 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> R e. Ring )
60 59 3ad2ant1 
 |-  ( ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) /\ i e. N /\ j e. N ) -> R e. Ring )
61 simpl 
 |-  ( ( X e. B /\ Y e. V ) -> X e. B )
62 61 3ad2ant2 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> X e. B )
63 62 47 49 3jca 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X e. B /\ Z e. V /\ I e. N ) )
64 63 3ad2ant1 
 |-  ( ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) /\ i e. N /\ j e. N ) -> ( X e. B /\ Z e. V /\ I e. N ) )
65 simp2 
 |-  ( ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) /\ i e. N /\ j e. N ) -> i e. N )
66 simp3 
 |-  ( ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) /\ i e. N /\ j e. N ) -> j e. N )
67 42 3ad2ant1 
 |-  ( ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) /\ i e. N /\ j e. N ) -> ( X .x. Z ) = Y )
68 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
69 1 2 3 50 68 4 6 mulmarep1gsum2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Z e. V /\ I e. N ) /\ ( i e. N /\ j e. N /\ ( X .x. Z ) = Y ) ) -> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l E j ) ) ) ) = if ( j = I , ( Y ` i ) , ( i X j ) ) )
70 60 64 65 66 67 69 syl113anc 
 |-  ( ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) /\ i e. N /\ j e. N ) -> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l E j ) ) ) ) = if ( j = I , ( Y ` i ) , ( i X j ) ) )
71 70 mpoeq3dva 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( i e. N , j e. N |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l E j ) ) ) ) ) = ( i e. N , j e. N |-> if ( j = I , ( Y ` i ) , ( i X j ) ) ) )
72 simpr 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. V )
73 72 3ad2ant2 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> Y e. V )
74 eqid 
 |-  ( N matRepV R ) = ( N matRepV R )
75 1 2 74 3 marepvval 
 |-  ( ( X e. B /\ Y e. V /\ I e. N ) -> ( ( X ( N matRepV R ) Y ) ` I ) = ( i e. N , j e. N |-> if ( j = I , ( Y ` i ) , ( i X j ) ) ) )
76 62 73 49 75 syl3anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( ( X ( N matRepV R ) Y ) ` I ) = ( i e. N , j e. N |-> if ( j = I , ( Y ` i ) , ( i X j ) ) ) )
77 5 76 eqtr2id 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( i e. N , j e. N |-> if ( j = I , ( Y ` i ) , ( i X j ) ) ) = H )
78 58 71 77 3eqtrd 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .X. E ) = H )