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 𝐵 = ( Base ‘ 𝐺 )
grpissubg.s 𝑆 = ( Base ‘ 𝐻 )
Assertion grpissubg ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 grpissubg.b 𝐵 = ( Base ‘ 𝐺 )
2 grpissubg.s 𝑆 = ( Base ‘ 𝐻 )
3 simpl ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆𝐵 )
4 3 adantl ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆𝐵 )
5 2 grpbn0 ( 𝐻 ∈ Grp → 𝑆 ≠ ∅ )
6 5 ad2antlr ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ≠ ∅ )
7 grpmnd ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
8 mndmgm ( 𝐺 ∈ Mnd → 𝐺 ∈ Mgm )
9 7 8 syl ( 𝐺 ∈ Grp → 𝐺 ∈ Mgm )
10 grpmnd ( 𝐻 ∈ Grp → 𝐻 ∈ Mnd )
11 mndmgm ( 𝐻 ∈ Mnd → 𝐻 ∈ Mgm )
12 10 11 syl ( 𝐻 ∈ Grp → 𝐻 ∈ Mgm )
13 9 12 anim12i ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) )
14 13 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) )
15 14 ad2antrr ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) ∧ 𝑏𝑆 ) → ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) )
16 simpr ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) )
17 16 ad2antrr ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) ∧ 𝑏𝑆 ) → ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) )
18 simpr ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) → 𝑎𝑆 )
19 18 anim1i ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) ∧ 𝑏𝑆 ) → ( 𝑎𝑆𝑏𝑆 ) )
20 1 2 mgmsscl ( ( ( 𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 )
21 15 17 19 20 syl3anc ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) ∧ 𝑏𝑆 ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 )
22 21 ralrimiva ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) → ∀ 𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 )
23 simpl ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → 𝐺 ∈ Grp )
24 23 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝐺 ∈ Grp )
25 simplr ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝐻 ∈ Grp )
26 1 sseq2i ( 𝑆𝐵𝑆 ⊆ ( Base ‘ 𝐺 ) )
27 26 biimpi ( 𝑆𝐵𝑆 ⊆ ( Base ‘ 𝐺 ) )
28 27 adantr ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
29 28 adantl ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
30 ovres ( ( 𝑥𝑆𝑦𝑆 ) → ( 𝑥 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g𝐺 ) 𝑦 ) )
31 30 adantl ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g𝐺 ) 𝑦 ) )
32 oveq ( ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑥 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) )
33 32 adantl ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑥 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) )
34 33 eqcomd ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑥 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
35 34 ad2antlr ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
36 31 35 eqtr3d ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
37 36 ralrimivva ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
38 24 25 2 29 37 grpinvssd ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑎𝑆 → ( ( invg𝐻 ) ‘ 𝑎 ) = ( ( invg𝐺 ) ‘ 𝑎 ) ) )
39 38 imp ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) → ( ( invg𝐻 ) ‘ 𝑎 ) = ( ( invg𝐺 ) ‘ 𝑎 ) )
40 eqid ( invg𝐻 ) = ( invg𝐻 )
41 2 40 grpinvcl ( ( 𝐻 ∈ Grp ∧ 𝑎𝑆 ) → ( ( invg𝐻 ) ‘ 𝑎 ) ∈ 𝑆 )
42 41 ad4ant24 ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) → ( ( invg𝐻 ) ‘ 𝑎 ) ∈ 𝑆 )
43 39 42 eqeltrrd ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) → ( ( invg𝐺 ) ‘ 𝑎 ) ∈ 𝑆 )
44 22 43 jca ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎𝑆 ) → ( ∀ 𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) )
45 44 ralrimiva ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑎𝑆 ( ∀ 𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) )
46 eqid ( +g𝐺 ) = ( +g𝐺 )
47 eqid ( invg𝐺 ) = ( invg𝐺 )
48 1 46 47 issubg2 ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆𝐵𝑆 ≠ ∅ ∧ ∀ 𝑎𝑆 ( ∀ 𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) ) )
49 48 ad2antrr ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆𝐵𝑆 ≠ ∅ ∧ ∀ 𝑎𝑆 ( ∀ 𝑏𝑆 ( 𝑎 ( +g𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) ) )
50 4 6 45 49 mpbir3and ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
51 50 ex ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆𝐵 ∧ ( +g𝐻 ) = ( ( +g𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )