Metamath Proof Explorer

Theorem cramerlem3

Description: Lemma 3 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramer.a 
|- A = ( N Mat R )
cramer.b 
|- B = ( Base ` A )
cramer.v 
|- V = ( ( Base ` R ) ^m N )
cramer.d 
|- D = ( N maDet R )
cramer.x 
|- .x. = ( R maVecMul <. N , N >. )
cramer.q 
|- ./ = ( /r ` R )
Assertion cramerlem3 
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )

Proof

Step Hyp Ref Expression
1 cramer.a 
 |-  A = ( N Mat R )
2 cramer.b 
 |-  B = ( Base ` A )
3 cramer.v 
 |-  V = ( ( Base ` R ) ^m N )
4 cramer.d 
 |-  D = ( N maDet R )
5 cramer.x 
 |-  .x. = ( R maVecMul <. N , N >. )
6 cramer.q 
 |-  ./ = ( /r ` R )
7 1 2 3 5 4 slesolex 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> E. v e. V ( X .x. v ) = Y )
8 1 2 3 4 5 6 cramerlem2 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
9 8 3adant1l 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
10 oveq2 
 |-  ( z = v -> ( X .x. z ) = ( X .x. v ) )
11 10 eqeq1d 
 |-  ( z = v -> ( ( X .x. z ) = Y <-> ( X .x. v ) = Y ) )
12 oveq2 
 |-  ( v = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. v ) = ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
13 12 eqeq1d 
 |-  ( v = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( ( X .x. v ) = Y <-> ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y ) )
14 11 13 rexraleqim 
 |-  ( ( E. v e. V ( X .x. v ) = Y /\ A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) ) -> ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y )
15 oveq2 
 |-  ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
16 15 adantl 
 |-  ( ( ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y /\ Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) -> ( X .x. Z ) = ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
17 simpl 
 |-  ( ( ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y /\ Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) -> ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y )
18 16 17 eqtrd 
 |-  ( ( ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y /\ Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) -> ( X .x. Z ) = Y )
19 18 ex 
 |-  ( ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )
20 19 a1d 
 |-  ( ( X .x. ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) = Y -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) )
21 14 20 syl 
 |-  ( ( E. v e. V ( X .x. v ) = Y /\ A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) ) -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) )
22 21 expcom 
 |-  ( A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) -> ( E. v e. V ( X .x. v ) = Y -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) ) )
23 22 com23 
 |-  ( A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( E. v e. V ( X .x. v ) = Y -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) ) )
24 9 23 mpcom 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( E. v e. V ( X .x. v ) = Y -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) )
25 7 24 mpd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )