Metamath Proof Explorer

Theorem grpissubg

Description: If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019)

Ref Expression
Hypotheses grpissubg.b 
|- B = ( Base ` G )
grpissubg.s 
|- S = ( Base ` H )
Assertion grpissubg 
|- ( ( G e. Grp /\ H e. Grp ) -> ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. ( SubGrp ` G ) ) )

Proof

Step Hyp Ref Expression
1 grpissubg.b 
 |-  B = ( Base ` G )
2 grpissubg.s 
 |-  S = ( Base ` H )
3 simpl 
 |-  ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S C_ B )
4 3 adantl 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S C_ B )
5 2 grpbn0 
 |-  ( H e. Grp -> S =/= (/) )
6 5 ad2antlr 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S =/= (/) )
7 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
8 mndmgm 
 |-  ( G e. Mnd -> G e. Mgm )
9 7 8 syl 
 |-  ( G e. Grp -> G e. Mgm )
10 grpmnd 
 |-  ( H e. Grp -> H e. Mnd )
11 mndmgm 
 |-  ( H e. Mnd -> H e. Mgm )
12 10 11 syl 
 |-  ( H e. Grp -> H e. Mgm )
13 9 12 anim12i 
 |-  ( ( G e. Grp /\ H e. Grp ) -> ( G e. Mgm /\ H e. Mgm ) )
14 13 adantr 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( G e. Mgm /\ H e. Mgm ) )
15 14 ad2antrr 
 |-  ( ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) /\ b e. S ) -> ( G e. Mgm /\ H e. Mgm ) )
16 simpr 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) )
17 16 ad2antrr 
 |-  ( ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) /\ b e. S ) -> ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) )
18 simpr 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) -> a e. S )
19 18 anim1i 
 |-  ( ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) /\ b e. S ) -> ( a e. S /\ b e. S ) )
20 1 2 mgmsscl 
 |-  ( ( ( G e. Mgm /\ H e. Mgm ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) /\ ( a e. S /\ b e. S ) ) -> ( a ( +g ` G ) b ) e. S )
21 15 17 19 20 syl3anc 
 |-  ( ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) /\ b e. S ) -> ( a ( +g ` G ) b ) e. S )
22 21 ralrimiva 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) -> A. b e. S ( a ( +g ` G ) b ) e. S )
23 simpl 
 |-  ( ( G e. Grp /\ H e. Grp ) -> G e. Grp )
24 23 adantr 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> G e. Grp )
25 simplr 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> H e. Grp )
26 1 sseq2i 
 |-  ( S C_ B <-> S C_ ( Base ` G ) )
27 26 biimpi 
 |-  ( S C_ B -> S C_ ( Base ` G ) )
28 27 adantr 
 |-  ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S C_ ( Base ` G ) )
29 28 adantl 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S C_ ( Base ` G ) )
30 ovres 
 |-  ( ( x e. S /\ y e. S ) -> ( x ( ( +g ` G ) |` ( S X. S ) ) y ) = ( x ( +g ` G ) y ) )
31 30 adantl 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x ( ( +g ` G ) |` ( S X. S ) ) y ) = ( x ( +g ` G ) y ) )
32 oveq 
 |-  ( ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) -> ( x ( +g ` H ) y ) = ( x ( ( +g ` G ) |` ( S X. S ) ) y ) )
33 32 adantl 
 |-  ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( x ( +g ` H ) y ) = ( x ( ( +g ` G ) |` ( S X. S ) ) y ) )
34 33 eqcomd 
 |-  ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( x ( ( +g ` G ) |` ( S X. S ) ) y ) = ( x ( +g ` H ) y ) )
35 34 ad2antlr 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x ( ( +g ` G ) |` ( S X. S ) ) y ) = ( x ( +g ` H ) y ) )
36 31 35 eqtr3d 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
37 36 ralrimivva 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> A. x e. S A. y e. S ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
38 24 25 2 29 37 grpinvssd 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( a e. S -> ( ( invg ` H ) ` a ) = ( ( invg ` G ) ` a ) ) )
39 38 imp 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) -> ( ( invg ` H ) ` a ) = ( ( invg ` G ) ` a ) )
40 eqid 
 |-  ( invg ` H ) = ( invg ` H )
41 2 40 grpinvcl 
 |-  ( ( H e. Grp /\ a e. S ) -> ( ( invg ` H ) ` a ) e. S )
42 41 ad4ant24 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) -> ( ( invg ` H ) ` a ) e. S )
43 39 42 eqeltrrd 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) -> ( ( invg ` G ) ` a ) e. S )
44 22 43 jca 
 |-  ( ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ a e. S ) -> ( A. b e. S ( a ( +g ` G ) b ) e. S /\ ( ( invg ` G ) ` a ) e. S ) )
45 44 ralrimiva 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> A. a e. S ( A. b e. S ( a ( +g ` G ) b ) e. S /\ ( ( invg ` G ) ` a ) e. S ) )
46 eqid 
 |-  ( +g ` G ) = ( +g ` G )
47 eqid 
 |-  ( invg ` G ) = ( invg ` G )
48 1 46 47 issubg2 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ S =/= (/) /\ A. a e. S ( A. b e. S ( a ( +g ` G ) b ) e. S /\ ( ( invg ` G ) ` a ) e. S ) ) ) )
49 48 ad2antrr 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ S =/= (/) /\ A. a e. S ( A. b e. S ( a ( +g ` G ) b ) e. S /\ ( ( invg ` G ) ` a ) e. S ) ) ) )
50 4 6 45 49 mpbir3and 
 |-  ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S e. ( SubGrp ` G ) )
51 50 ex 
 |-  ( ( G e. Grp /\ H e. Grp ) -> ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. ( SubGrp ` G ) ) )