Metamath Proof Explorer

Theorem cramer0

Description: Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-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 cramer0 
|- ( ( ( 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 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
8 2 7 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
9 fvoveq1 
 |-  ( N = (/) -> ( Base ` ( N Mat R ) ) = ( Base ` ( (/) Mat R ) ) )
10 8 9 eqtrid 
 |-  ( N = (/) -> B = ( Base ` ( (/) Mat R ) ) )
11 10 adantr 
 |-  ( ( N = (/) /\ R e. CRing ) -> B = ( Base ` ( (/) Mat R ) ) )
12 11 eleq2d 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( X e. B <-> X e. ( Base ` ( (/) Mat R ) ) ) )
13 mat0dimbas0 
 |-  ( R e. CRing -> ( Base ` ( (/) Mat R ) ) = { (/) } )
14 13 eleq2d 
 |-  ( R e. CRing -> ( X e. ( Base ` ( (/) Mat R ) ) <-> X e. { (/) } ) )
15 14 adantl 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( X e. ( Base ` ( (/) Mat R ) ) <-> X e. { (/) } ) )
16 12 15 bitrd 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( X e. B <-> X e. { (/) } ) )
17 3 a1i 
 |-  ( ( N = (/) /\ R e. CRing ) -> V = ( ( Base ` R ) ^m N ) )
18 oveq2 
 |-  ( N = (/) -> ( ( Base ` R ) ^m N ) = ( ( Base ` R ) ^m (/) ) )
19 18 adantr 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( ( Base ` R ) ^m N ) = ( ( Base ` R ) ^m (/) ) )
20 fvex 
 |-  ( Base ` R ) e. _V
21 map0e 
 |-  ( ( Base ` R ) e. _V -> ( ( Base ` R ) ^m (/) ) = 1o )
22 20 21 mp1i 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( ( Base ` R ) ^m (/) ) = 1o )
23 17 19 22 3eqtrd 
 |-  ( ( N = (/) /\ R e. CRing ) -> V = 1o )
24 23 eleq2d 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( Y e. V <-> Y e. 1o ) )
25 el1o 
 |-  ( Y e. 1o <-> Y = (/) )
26 24 25 bitrdi 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( Y e. V <-> Y = (/) ) )
27 16 26 anbi12d 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( ( X e. B /\ Y e. V ) <-> ( X e. { (/) } /\ Y = (/) ) ) )
28 elsni 
 |-  ( X e. { (/) } -> X = (/) )
29 mpteq1 
 |-  ( N = (/) -> ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) = ( i e. (/) |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) )
30 mpt0 
 |-  ( i e. (/) |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) = (/)
31 29 30 eqtrdi 
 |-  ( N = (/) -> ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) = (/) )
32 31 eqeq2d 
 |-  ( N = (/) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) <-> Z = (/) ) )
33 32 ad2antrr 
 |-  ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) <-> Z = (/) ) )
34 simplrl 
 |-  ( ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) /\ Z = (/) ) -> X = (/) )
35 simpr 
 |-  ( ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) /\ Z = (/) ) -> Z = (/) )
36 34 35 oveq12d 
 |-  ( ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) /\ Z = (/) ) -> ( X .x. Z ) = ( (/) .x. (/) ) )
37 5 mavmul0 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( (/) .x. (/) ) = (/) )
38 37 ad2antrr 
 |-  ( ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) /\ Z = (/) ) -> ( (/) .x. (/) ) = (/) )
39 simpr 
 |-  ( ( X = (/) /\ Y = (/) ) -> Y = (/) )
40 39 eqcomd 
 |-  ( ( X = (/) /\ Y = (/) ) -> (/) = Y )
41 40 ad2antlr 
 |-  ( ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) /\ Z = (/) ) -> (/) = Y )
42 36 38 41 3eqtrd 
 |-  ( ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) /\ Z = (/) ) -> ( X .x. Z ) = Y )
43 42 ex 
 |-  ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) -> ( Z = (/) -> ( X .x. Z ) = Y ) )
44 33 43 sylbid 
 |-  ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )
45 44 a1d 
 |-  ( ( ( N = (/) /\ R e. CRing ) /\ ( X = (/) /\ Y = (/) ) ) -> ( ( D ` X ) e. ( Unit ` R ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) )
46 45 ex 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( ( X = (/) /\ Y = (/) ) -> ( ( D ` X ) e. ( Unit ` R ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) ) )
47 28 46 sylani 
 |-  ( ( N = (/) /\ R e. CRing ) -> ( ( X e. { (/) } /\ Y = (/) ) -> ( ( D ` X ) e. ( Unit ` R ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) ) ) )
48 27 47 sylbid 
 |-  ( ( 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 ) ) ) )
49 48 3imp 
 |-  ( ( ( 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 ) )