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 birani ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
28 27 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
29 ovres ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
30 29 adantl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
31 oveq ⊢ ( ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) )
32 31 adantl ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) )
33 32 eqcomd ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
34 33 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
35 30 34 eqtr3d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
36 35 ralrimivva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
37 24 25 2 28 36 grpinvssd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑎 ∈ 𝑆 → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) )
38 37 imp ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) )
39 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
40 2 39 grpinvcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) ∈ 𝑆 )
41 40 ad4ant24 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐻 ) ‘ 𝑎 ) ∈ 𝑆 )
42 38 41 eqeltrrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 )
43 22 42 jca ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) ∧ 𝑎 ∈ 𝑆 ) → ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) )
44 43 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ∀ 𝑎 ∈ 𝑆 ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) )
45 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
46 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
47 1 45 46 issubg2 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝑆 ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) ) )
48 47 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝑆 ( ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) ) )
49 4 6 44 48 mpbir3and ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) ∧ ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
50 49 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ Grp ) → ( ( 𝑆 ⊆ 𝐵 ∧ ( +g ‘ 𝐻 ) = ( ( +g ‘ 𝐺 ) ↾ ( 𝑆 × 𝑆 ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )