Metamath Proof Explorer

Theorem mavmul0g

Description: The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 mavmul0.t 
 |-  .x. = ( R maVecMul <. N , N >. )
2 oveq12 
 |-  ( ( X = (/) /\ Y = (/) ) -> ( X .x. Y ) = ( (/) .x. (/) ) )
3 1 mavmul0 
 |-  ( ( N = (/) /\ R e. V ) -> ( (/) .x. (/) ) = (/) )
4 2 3 sylan9eq 
 |-  ( ( ( X = (/) /\ Y = (/) ) /\ ( N = (/) /\ R e. V ) ) -> ( X .x. Y ) = (/) )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 simpr 
 |-  ( ( N = (/) /\ R e. V ) -> R e. V )
8 0fi 
 |-  (/) e. Fin
9 eleq1 
 |-  ( N = (/) -> ( N e. Fin <-> (/) e. Fin ) )
10 8 9 mpbiri 
 |-  ( N = (/) -> N e. Fin )
11 10 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> N e. Fin )
12 1 5 6 7 11 11 mvmulfval 
 |-  ( ( N = (/) /\ R e. V ) -> .x. = ( i e. ( ( Base ` R ) ^m ( N X. N ) ) , j e. ( ( Base ` R ) ^m N ) |-> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) ) )
13 12 dmeqd 
 |-  ( ( N = (/) /\ R e. V ) -> dom .x. = dom ( i e. ( ( Base ` R ) ^m ( N X. N ) ) , j e. ( ( Base ` R ) ^m N ) |-> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) ) )
14 0ex 
 |-  (/) e. _V
15 eleq1 
 |-  ( N = (/) -> ( N e. _V <-> (/) e. _V ) )
16 14 15 mpbiri 
 |-  ( N = (/) -> N e. _V )
17 16 mptexd 
 |-  ( N = (/) -> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) e. _V )
18 17 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) e. _V )
19 18 adantr 
 |-  ( ( ( N = (/) /\ R e. V ) /\ ( i e. ( ( Base ` R ) ^m ( N X. N ) ) /\ j e. ( ( Base ` R ) ^m N ) ) ) -> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) e. _V )
20 19 ralrimivva 
 |-  ( ( N = (/) /\ R e. V ) -> A. i e. ( ( Base ` R ) ^m ( N X. N ) ) A. j e. ( ( Base ` R ) ^m N ) ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) e. _V )
21 eqid 
 |-  ( i e. ( ( Base ` R ) ^m ( N X. N ) ) , j e. ( ( Base ` R ) ^m N ) |-> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) ) = ( i e. ( ( Base ` R ) ^m ( N X. N ) ) , j e. ( ( Base ` R ) ^m N ) |-> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) )
22 21 dmmpoga 
 |-  ( A. i e. ( ( Base ` R ) ^m ( N X. N ) ) A. j e. ( ( Base ` R ) ^m N ) ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) e. _V -> dom ( i e. ( ( Base ` R ) ^m ( N X. N ) ) , j e. ( ( Base ` R ) ^m N ) |-> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) ) = ( ( ( Base ` R ) ^m ( N X. N ) ) X. ( ( Base ` R ) ^m N ) ) )
23 20 22 syl 
 |-  ( ( N = (/) /\ R e. V ) -> dom ( i e. ( ( Base ` R ) ^m ( N X. N ) ) , j e. ( ( Base ` R ) ^m N ) |-> ( k e. N |-> ( R gsum ( l e. N |-> ( ( k i l ) ( .r ` R ) ( j ` l ) ) ) ) ) ) = ( ( ( Base ` R ) ^m ( N X. N ) ) X. ( ( Base ` R ) ^m N ) ) )
24 id 
 |-  ( N = (/) -> N = (/) )
25 24 24 xpeq12d 
 |-  ( N = (/) -> ( N X. N ) = ( (/) X. (/) ) )
26 0xp 
 |-  ( (/) X. (/) ) = (/)
27 25 26 eqtrdi 
 |-  ( N = (/) -> ( N X. N ) = (/) )
28 27 oveq2d 
 |-  ( N = (/) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( ( Base ` R ) ^m (/) ) )
29 fvex 
 |-  ( Base ` R ) e. _V
30 map0e 
 |-  ( ( Base ` R ) e. _V -> ( ( Base ` R ) ^m (/) ) = 1o )
31 29 30 mp1i 
 |-  ( N = (/) -> ( ( Base ` R ) ^m (/) ) = 1o )
32 28 31 eqtrd 
 |-  ( N = (/) -> ( ( Base ` R ) ^m ( N X. N ) ) = 1o )
33 32 adantr 
 |-  ( ( N = (/) /\ R e. V ) -> ( ( Base ` R ) ^m ( N X. N ) ) = 1o )
34 df1o2 
 |-  1o = { (/) }
35 33 34 eqtrdi 
 |-  ( ( N = (/) /\ R e. V ) -> ( ( Base ` R ) ^m ( N X. N ) ) = { (/) } )
36 oveq2 
 |-  ( N = (/) -> ( ( Base ` R ) ^m N ) = ( ( Base ` R ) ^m (/) ) )
37 29 30 mp1i 
 |-  ( R e. V -> ( ( Base ` R ) ^m (/) ) = 1o )
38 37 34 eqtrdi 
 |-  ( R e. V -> ( ( Base ` R ) ^m (/) ) = { (/) } )
39 36 38 sylan9eq 
 |-  ( ( N = (/) /\ R e. V ) -> ( ( Base ` R ) ^m N ) = { (/) } )
40 35 39 xpeq12d 
 |-  ( ( N = (/) /\ R e. V ) -> ( ( ( Base ` R ) ^m ( N X. N ) ) X. ( ( Base ` R ) ^m N ) ) = ( { (/) } X. { (/) } ) )
41 13 23 40 3eqtrd 
 |-  ( ( N = (/) /\ R e. V ) -> dom .x. = ( { (/) } X. { (/) } ) )
42 elsni 
 |-  ( X e. { (/) } -> X = (/) )
43 elsni 
 |-  ( Y e. { (/) } -> Y = (/) )
44 42 43 anim12i 
 |-  ( ( X e. { (/) } /\ Y e. { (/) } ) -> ( X = (/) /\ Y = (/) ) )
45 44 con3i 
 |-  ( -. ( X = (/) /\ Y = (/) ) -> -. ( X e. { (/) } /\ Y e. { (/) } ) )
46 ndmovg 
 |-  ( ( dom .x. = ( { (/) } X. { (/) } ) /\ -. ( X e. { (/) } /\ Y e. { (/) } ) ) -> ( X .x. Y ) = (/) )
47 41 45 46 syl2anr 
 |-  ( ( -. ( X = (/) /\ Y = (/) ) /\ ( N = (/) /\ R e. V ) ) -> ( X .x. Y ) = (/) )
48 4 47 pm2.61ian 
 |-  ( ( N = (/) /\ R e. V ) -> ( X .x. Y ) = (/) )