Metamath Proof Explorer

Theorem mavmul0

Description: Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019)

Ref Expression
Hypothesis mavmul0.t 
|- .x. = ( R maVecMul <. N , N >. )
Assertion mavmul0 
|- ( ( N = (/) /\ R e. V ) -> ( (/) .x. (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 mavmul0.t 
 |-  .x. = ( R maVecMul <. N , N >. )
2 eqid 
 |-  ( N Mat R ) = ( N Mat R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 simpr 
 |-  ( ( N = (/) /\ R e. V ) -> R e. V )
6 0fin 
 |-  (/) e. Fin
7 eleq1 
 |-  ( N = (/) -> ( N e. Fin <-> (/) e. Fin ) )
8 6 7 mpbiri 
 |-  ( N = (/) -> N e. Fin )
9 8 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> N e. Fin )
10 0ex 
 |-  (/) e. _V
11 snidg 
 |-  ( (/) e. _V -> (/) e. { (/) } )
12 10 11 mp1i 
 |-  ( ( N = (/) /\ R e. V ) -> (/) e. { (/) } )
13 oveq1 
 |-  ( N = (/) -> ( N Mat R ) = ( (/) Mat R ) )
14 13 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> ( N Mat R ) = ( (/) Mat R ) )
15 14 fveq2d 
 |-  ( ( N = (/) /\ R e. V ) -> ( Base ` ( N Mat R ) ) = ( Base ` ( (/) Mat R ) ) )
16 mat0dimbas0 
 |-  ( R e. V -> ( Base ` ( (/) Mat R ) ) = { (/) } )
17 16 adantl 
 |-  ( ( N = (/) /\ R e. V ) -> ( Base ` ( (/) Mat R ) ) = { (/) } )
18 15 17 eqtrd 
 |-  ( ( N = (/) /\ R e. V ) -> ( Base ` ( N Mat R ) ) = { (/) } )
19 12 18 eleqtrrd 
 |-  ( ( N = (/) /\ R e. V ) -> (/) e. ( Base ` ( N Mat R ) ) )
20 eqidd 
 |-  ( N = (/) -> (/) = (/) )
21 el1o 
 |-  ( (/) e. 1o <-> (/) = (/) )
22 20 21 sylibr 
 |-  ( N = (/) -> (/) e. 1o )
23 oveq2 
 |-  ( N = (/) -> ( ( Base ` R ) ^m N ) = ( ( Base ` R ) ^m (/) ) )
24 fvex 
 |-  ( Base ` R ) e. _V
25 map0e 
 |-  ( ( Base ` R ) e. _V -> ( ( Base ` R ) ^m (/) ) = 1o )
26 24 25 mp1i 
 |-  ( N = (/) -> ( ( Base ` R ) ^m (/) ) = 1o )
27 23 26 eqtrd 
 |-  ( N = (/) -> ( ( Base ` R ) ^m N ) = 1o )
28 22 27 eleqtrrd 
 |-  ( N = (/) -> (/) e. ( ( Base ` R ) ^m N ) )
29 28 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> (/) e. ( ( Base ` R ) ^m N ) )
30 2 1 3 4 5 9 19 29 mavmulval 
 |-  ( ( N = (/) /\ R e. V ) -> ( (/) .x. (/) ) = ( i e. N |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) )
31 mpteq1 
 |-  ( N = (/) -> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) = ( i e. (/) |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) )
32 31 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) = ( i e. (/) |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) )
33 mpt0 
 |-  ( i e. (/) |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) = (/)
34 32 33 eqtrdi 
 |-  ( ( N = (/) /\ R e. V ) -> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i (/) j ) ( .r ` R ) ( (/) ` j ) ) ) ) ) = (/) )
35 30 34 eqtrd 
 |-  ( ( N = (/) /\ R e. V ) -> ( (/) .x. (/) ) = (/) )