Metamath Proof Explorer

Theorem xpsgrp

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

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

Proof

Step Hyp Ref Expression
1 xpsgrp.t 
 |-  T = ( R Xs. S )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 simpl 
 |-  ( ( R e. Grp /\ S e. Grp ) -> R e. Grp )
5 simpr 
 |-  ( ( R e. Grp /\ S e. Grp ) -> S e. Grp )
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. Grp /\ S e. Grp ) -> 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. Grp /\ S e. Grp ) -> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
12 11 f1oeq3d 
 |-  ( ( R e. Grp /\ S e. Grp ) -> ( ( 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. Grp /\ S e. Grp ) -> ( 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. Grp /\ S e. Grp ) -> `' ( 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. Grp /\ S e. Grp ) -> 2o e. On )
19 fvexd 
 |-  ( ( R e. Grp /\ S e. Grp ) -> ( Scalar ` R ) e. _V )
20 xpscf 
 |-  ( { <. (/) , R >. , <. 1o , S >. } : 2o --> Grp <-> ( R e. Grp /\ S e. Grp ) )
21 20 biimpri 
 |-  ( ( R e. Grp /\ S e. Grp ) -> { <. (/) , R >. , <. 1o , S >. } : 2o --> Grp )
22 8 18 19 21 prdsgrpd 
 |-  ( ( R e. Grp /\ S e. Grp ) -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. Grp )
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 imasgrpf1 
 |-  ( ( `' ( 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. Grp ) -> ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. Grp )
26 16 22 25 syl2anc 
 |-  ( ( R e. Grp /\ S e. Grp ) -> ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. Grp )
27 9 26 eqeltrd 
 |-  ( ( R e. Grp /\ S e. Grp ) -> T e. Grp )