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 biimpi 
 |-  ( Y e. V -> Y e. ( ( Base ` R ) ^m N ) )
40 39 adantl 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. ( ( Base ` R ) ^m N ) )
41 10 40 anim12i 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) )
42 41 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 ) ) )
43 simp3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .x. Z ) = Y )
44 eqid 
 |-  ( ( Base ` R ) ^m ( N X. N ) ) = ( ( Base ` R ) ^m ( N X. N ) )
45 eqid 
 |-  ( ( Base ` R ) ^m N ) = ( ( Base ` R ) ^m N )
46 8 44 3 6 45 mavmulsolcl 
 |-  ( ( ( N e. Fin /\ N e. Fin /\ N =/= (/) ) /\ ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
47 46 imp 
 |-  ( ( ( ( N e. Fin /\ N e. Fin /\ N =/= (/) ) /\ ( R e. CRing /\ Y e. ( ( Base ` R ) ^m N ) ) ) /\ ( X .x. Z ) = Y ) -> Z e. V )
48 37 42 43 47 syl21anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> Z e. V )
49 simpr 
 |-  ( ( R e. CRing /\ I e. N ) -> I e. N )
50 49 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> I e. N )
51 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
52 1 2 3 51 ma1repvcl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( Z e. V /\ I e. N ) ) -> ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I ) e. B )
53 4 52 eqeltrid 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( Z e. V /\ I e. N ) ) -> E e. B )
54 33 48 50 53 syl12anc 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> E e. B )
55 20 eqcomd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
56 55 ad2ant2r 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) ) -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
57 56 3adant3 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( ( Base ` R ) ^m ( N X. N ) ) = B )
58 54 57 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 ) ) )
59 7 8 9 11 15 15 15 29 58 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 ) ) ) ) ) )
60 31 3ad2ant1 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> R e. Ring )
61 60 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 )
62 simpl 
 |-  ( ( X e. B /\ Y e. V ) -> X e. B )
63 62 3ad2ant2 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> X e. B )
64 63 48 50 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 ) )
65 64 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 ) )
66 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 )
67 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 )
68 43 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 )
69 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
70 1 2 3 51 69 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 ) ) )
71 61 65 66 67 68 70 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 ) ) )
72 71 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 ) ) ) )
73 simpr 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. V )
74 73 3ad2ant2 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> Y e. V )
75 eqid 
 |-  ( N matRepV R ) = ( N matRepV R )
76 1 2 75 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 ) ) ) )
77 63 74 50 76 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 ) ) ) )
78 5 77 syl5req 
 |-  ( ( ( 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 )
79 59 72 78 3eqtrd 
 |-  ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .X. E ) = H )