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 )