Metamath Proof Explorer

Theorem mamudm

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

Ref Expression
Hypotheses mamudm.e 
|- E = ( R freeLMod ( M X. N ) )
mamudm.b 
|- B = ( Base ` E )
mamudm.f 
|- F = ( R freeLMod ( N X. P ) )
mamudm.c 
|- C = ( Base ` F )
mamudm.m 
|- .X. = ( R maMul <. M , N , P >. )
Assertion mamudm 
|- ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom .X. = ( B X. C ) )

Proof

Step Hyp Ref Expression
1 mamudm.e 
 |-  E = ( R freeLMod ( M X. N ) )
2 mamudm.b 
 |-  B = ( Base ` E )
3 mamudm.f 
 |-  F = ( R freeLMod ( N X. P ) )
4 mamudm.c 
 |-  C = ( Base ` F )
5 mamudm.m 
 |-  .X. = ( R maMul <. M , N , P >. )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 simpl 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> R e. V )
9 simpr1 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> M e. Fin )
10 simpr2 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> N e. Fin )
11 simpr3 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> P e. Fin )
12 5 6 7 8 9 10 11 mamufval 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> .X. = ( x e. ( ( Base ` R ) ^m ( M X. N ) ) , y e. ( ( Base ` R ) ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) ) )
13 12 dmeqd 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom .X. = dom ( x e. ( ( Base ` R ) ^m ( M X. N ) ) , y e. ( ( Base ` R ) ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) ) )
14 mpoexga 
 |-  ( ( M e. Fin /\ P e. Fin ) -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) e. _V )
15 14 3adant2 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) e. _V )
16 15 adantl 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) e. _V )
17 16 a1d 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( x e. ( ( Base ` R ) ^m ( M X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. P ) ) ) -> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) e. _V ) )
18 17 ralrimivv 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> A. x e. ( ( Base ` R ) ^m ( M X. N ) ) A. y e. ( ( Base ` R ) ^m ( N X. P ) ) ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) e. _V )
19 eqid 
 |-  ( x e. ( ( Base ` R ) ^m ( M X. N ) ) , y e. ( ( Base ` R ) ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) ) = ( x e. ( ( Base ` R ) ^m ( M X. N ) ) , y e. ( ( Base ` R ) ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) )
20 19 dmmpoga 
 |-  ( A. x e. ( ( Base ` R ) ^m ( M X. N ) ) A. y e. ( ( Base ` R ) ^m ( N X. P ) ) ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) e. _V -> dom ( x e. ( ( Base ` R ) ^m ( M X. N ) ) , y e. ( ( Base ` R ) ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) ) = ( ( ( Base ` R ) ^m ( M X. N ) ) X. ( ( Base ` R ) ^m ( N X. P ) ) ) )
21 18 20 syl 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom ( x e. ( ( Base ` R ) ^m ( M X. N ) ) , y e. ( ( Base ` R ) ^m ( N X. P ) ) |-> ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( i x j ) ( .r ` R ) ( j y k ) ) ) ) ) ) = ( ( ( Base ` R ) ^m ( M X. N ) ) X. ( ( Base ` R ) ^m ( N X. P ) ) ) )
22 xpfi 
 |-  ( ( M e. Fin /\ N e. Fin ) -> ( M X. N ) e. Fin )
23 22 3adant3 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( M X. N ) e. Fin )
24 1 6 frlmfibas 
 |-  ( ( R e. V /\ ( M X. N ) e. Fin ) -> ( ( Base ` R ) ^m ( M X. N ) ) = ( Base ` E ) )
25 23 24 sylan2 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( Base ` R ) ^m ( M X. N ) ) = ( Base ` E ) )
26 25 2 eqtr4di 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( Base ` R ) ^m ( M X. N ) ) = B )
27 xpfi 
 |-  ( ( N e. Fin /\ P e. Fin ) -> ( N X. P ) e. Fin )
28 27 3adant1 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( N X. P ) e. Fin )
29 3 6 frlmfibas 
 |-  ( ( R e. V /\ ( N X. P ) e. Fin ) -> ( ( Base ` R ) ^m ( N X. P ) ) = ( Base ` F ) )
30 28 29 sylan2 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( Base ` R ) ^m ( N X. P ) ) = ( Base ` F ) )
31 30 4 eqtr4di 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( Base ` R ) ^m ( N X. P ) ) = C )
32 26 31 xpeq12d 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( ( Base ` R ) ^m ( M X. N ) ) X. ( ( Base ` R ) ^m ( N X. P ) ) ) = ( B X. C ) )
33 13 21 32 3eqtrd 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom .X. = ( B X. C ) )