Metamath Proof Explorer

Theorem xpsmnd

Description: The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypothesis xpsmnd.t 
|- T = ( R Xs. S )
Assertion xpsmnd 
|- ( ( R e. Mnd /\ S e. Mnd ) -> T e. Mnd )

Proof

Step Hyp Ref Expression
1 xpsmnd.t 
 |-  T = ( R Xs. S )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 simpl 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> R e. Mnd )
5 simpr 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> S e. Mnd )
6 eqid 
 |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
7 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
8 eqid 
 |-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
9 1 2 3 4 5 6 7 8 xpsval 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> T = ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
10 6 xpsff1o2 
 |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
11 1 2 3 4 5 6 7 8 xpsrnbas 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
12 11 f1oeq3d 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) <-> ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) )
13 10 12 mpbii 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
14 f1ocnv 
 |-  ( ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
15 f1of1 
 |-  ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) -1-1-> ( ( Base ` R ) X. ( Base ` S ) ) )
16 13 14 15 3syl 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) -1-1-> ( ( Base ` R ) X. ( Base ` S ) ) )
17 2on 
 |-  2o e. On
18 17 a1i 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> 2o e. On )
19 fvexd 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( Scalar ` R ) e. _V )
20 xpscf 
 |-  ( { <. (/) , R >. , <. 1o , S >. } : 2o --> Mnd <-> ( R e. Mnd /\ S e. Mnd ) )
21 20 biimpri 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> { <. (/) , R >. , <. 1o , S >. } : 2o --> Mnd )
22 8 18 19 21 prdsmndd 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. Mnd )
23 eqid 
 |-  ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
24 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
25 23 24 imasmndf1 
 |-  ( ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) -1-1-> ( ( Base ` R ) X. ( Base ` S ) ) /\ ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. Mnd ) -> ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. Mnd )
26 16 22 25 syl2anc 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. Mnd )
27 9 26 eqeltrd 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> T e. Mnd )