Metamath Proof Explorer

Theorem mavmuldm

Description: The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019)

Ref Expression
Hypotheses mavmuldm.b 
|- B = ( Base ` R )
mavmuldm.c 
|- C = ( B ^m ( M X. N ) )
mavmuldm.d 
|- D = ( B ^m N )
mavmuldm.t 
|- .x. = ( R maVecMul <. M , N >. )
Assertion mavmuldm 
|- ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom .x. = ( C X. D ) )

Proof

Step Hyp Ref Expression
1 mavmuldm.b 
 |-  B = ( Base ` R )
2 mavmuldm.c 
 |-  C = ( B ^m ( M X. N ) )
3 mavmuldm.d 
 |-  D = ( B ^m N )
4 mavmuldm.t 
 |-  .x. = ( R maVecMul <. M , N >. )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 simp1 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> R e. V )
7 simp2 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> M e. Fin )
8 simp3 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> N e. Fin )
9 4 1 5 6 7 8 mvmulfval 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> .x. = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) ) )
10 9 dmeqd 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom .x. = dom ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) ) )
11 mptexg 
 |-  ( M e. Fin -> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) e. _V )
12 11 3ad2ant2 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) e. _V )
13 12 a1d 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> ( ( x e. ( B ^m ( M X. N ) ) /\ y e. ( B ^m N ) ) -> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) e. _V ) )
14 13 ralrimivv 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> A. x e. ( B ^m ( M X. N ) ) A. y e. ( B ^m N ) ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) e. _V )
15 eqid 
 |-  ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) ) = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) )
16 15 dmmpoga 
 |-  ( A. x e. ( B ^m ( M X. N ) ) A. y e. ( B ^m N ) ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) e. _V -> dom ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) ) = ( ( B ^m ( M X. N ) ) X. ( B ^m N ) ) )
17 14 16 syl 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( y ` j ) ) ) ) ) ) = ( ( B ^m ( M X. N ) ) X. ( B ^m N ) ) )
18 2 eqcomi 
 |-  ( B ^m ( M X. N ) ) = C
19 18 a1i 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> ( B ^m ( M X. N ) ) = C )
20 3 a1i 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> D = ( B ^m N ) )
21 20 eqcomd 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> ( B ^m N ) = D )
22 19 21 xpeq12d 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> ( ( B ^m ( M X. N ) ) X. ( B ^m N ) ) = ( C X. D ) )
23 10 17 22 3eqtrd 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom .x. = ( C X. D ) )