Metamath Proof Explorer

Theorem cramerlem1

Description: Lemma 1 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 cramerlem1 
|- ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) )

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 simp1 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> R e. CRing )
8 7 anim1i 
 |-  ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) /\ a e. N ) -> ( R e. CRing /\ a e. N ) )
9 simpl2 
 |-  ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) /\ a e. N ) -> ( X e. B /\ Y e. V ) )
10 pm3.22 
 |-  ( ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) -> ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) )
11 10 3adant2 
 |-  ( ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) -> ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) )
12 11 3ad2ant3 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) )
13 12 adantr 
 |-  ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) /\ a e. N ) -> ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) )
14 eqid 
 |-  ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` a ) = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` a )
15 eqid 
 |-  ( ( X ( N matRepV R ) Y ) ` a ) = ( ( X ( N matRepV R ) Y ) ` a )
16 1 2 3 14 15 5 4 6 cramerimp 
 |-  ( ( ( R e. CRing /\ a e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( Z ` a ) = ( ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) ./ ( D ` X ) ) )
17 8 9 13 16 syl3anc 
 |-  ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) /\ a e. N ) -> ( Z ` a ) = ( ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) ./ ( D ` X ) ) )
18 17 ralrimiva 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> A. a e. N ( Z ` a ) = ( ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) ./ ( D ` X ) ) )
19 elmapfn 
 |-  ( Z e. ( ( Base ` R ) ^m N ) -> Z Fn N )
20 19 3 eleq2s 
 |-  ( Z e. V -> Z Fn N )
21 20 3ad2ant2 
 |-  ( ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) -> Z Fn N )
22 21 3ad2ant3 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> Z Fn N )
23 2fveq3 
 |-  ( a = i -> ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) = ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) )
24 23 oveq1d 
 |-  ( a = i -> ( ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) ./ ( D ` X ) ) = ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) )
25 ovexd 
 |-  ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) /\ a e. N ) -> ( ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) ./ ( D ` X ) ) e. _V )
26 ovexd 
 |-  ( ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) /\ i e. N ) -> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) e. _V )
27 22 24 25 26 fnmptfvd 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) <-> A. a e. N ( Z ` a ) = ( ( D ` ( ( X ( N matRepV R ) Y ) ` a ) ) ./ ( D ` X ) ) ) )
28 18 27 mpbird 
 |-  ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) )