Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpissubg Structured version   Visualization version   GIF version

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

Proof of Theorem grpissubg
Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 487 . . . 4 ((𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))) → 𝑆𝐵)
21adantl 486 . . 3 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆𝐵)
3 grpissubg.s . . . . 5 𝑆 = (Base‘𝐻)
43grpbn0 18189 . . . 4 (𝐻 ∈ Grp → 𝑆 ≠ ∅)
54ad2antlr 727 . . 3 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ≠ ∅)
6 grpmnd 18166 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
7 mndmgm 17974 . . . . . . . . . . 11 (𝐺 ∈ Mnd → 𝐺 ∈ Mgm)
86, 7syl 17 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝐺 ∈ Mgm)
9 grpmnd 18166 . . . . . . . . . . 11 (𝐻 ∈ Grp → 𝐻 ∈ Mnd)
10 mndmgm 17974 . . . . . . . . . . 11 (𝐻 ∈ Mnd → 𝐻 ∈ Mgm)
119, 10syl 17 . . . . . . . . . 10 (𝐻 ∈ Grp → 𝐻 ∈ Mgm)
128, 11anim12i 616 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → (𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm))
1312adantr 485 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → (𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm))
1413ad2antrr 726 . . . . . . 7 (((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) ∧ 𝑏𝑆) → (𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm))
15 simpr 489 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))))
1615ad2antrr 726 . . . . . . 7 (((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) ∧ 𝑏𝑆) → (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))))
17 simpr 489 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) → 𝑎𝑆)
1817anim1i 618 . . . . . . 7 (((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) ∧ 𝑏𝑆) → (𝑎𝑆𝑏𝑆))
19 grpissubg.b . . . . . . . 8 𝐵 = (Base‘𝐺)
2019, 3mgmsscl 17913 . . . . . . 7 (((𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))) ∧ (𝑎𝑆𝑏𝑆)) → (𝑎(+g𝐺)𝑏) ∈ 𝑆)
2114, 16, 18, 20syl3anc 1369 . . . . . 6 (((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) ∧ 𝑏𝑆) → (𝑎(+g𝐺)𝑏) ∈ 𝑆)
2221ralrimiva 3114 . . . . 5 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) → ∀𝑏𝑆 (𝑎(+g𝐺)𝑏) ∈ 𝑆)
23 simpl 487 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → 𝐺 ∈ Grp)
2423adantr 485 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → 𝐺 ∈ Grp)
25 simplr 769 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → 𝐻 ∈ Grp)
2619sseq2i 3922 . . . . . . . . . . 11 (𝑆𝐵𝑆 ⊆ (Base‘𝐺))
2726biimpi 219 . . . . . . . . . 10 (𝑆𝐵𝑆 ⊆ (Base‘𝐺))
2827adantr 485 . . . . . . . . 9 ((𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ⊆ (Base‘𝐺))
2928adantl 486 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ⊆ (Base‘𝐺))
30 ovres 7308 . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → (𝑥((+g𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g𝐺)𝑦))
3130adantl 486 . . . . . . . . . 10 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥((+g𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g𝐺)𝑦))
32 oveq 7154 . . . . . . . . . . . . 13 ((+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)) → (𝑥(+g𝐻)𝑦) = (𝑥((+g𝐺) ↾ (𝑆 × 𝑆))𝑦))
3332adantl 486 . . . . . . . . . . . 12 ((𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))) → (𝑥(+g𝐻)𝑦) = (𝑥((+g𝐺) ↾ (𝑆 × 𝑆))𝑦))
3433eqcomd 2765 . . . . . . . . . . 11 ((𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))) → (𝑥((+g𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g𝐻)𝑦))
3534ad2antlr 727 . . . . . . . . . 10 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥((+g𝐺) ↾ (𝑆 × 𝑆))𝑦) = (𝑥(+g𝐻)𝑦))
3631, 35eqtr3d 2796 . . . . . . . . 9 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝐻)𝑦))
3736ralrimivva 3121 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝐺)𝑦) = (𝑥(+g𝐻)𝑦))
3824, 25, 3, 29, 37grpinvssd 18233 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → (𝑎𝑆 → ((invg𝐻)‘𝑎) = ((invg𝐺)‘𝑎)))
3938imp 411 . . . . . 6 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) → ((invg𝐻)‘𝑎) = ((invg𝐺)‘𝑎))
40 eqid 2759 . . . . . . . 8 (invg𝐻) = (invg𝐻)
413, 40grpinvcl 18208 . . . . . . 7 ((𝐻 ∈ Grp ∧ 𝑎𝑆) → ((invg𝐻)‘𝑎) ∈ 𝑆)
4241ad4ant24 754 . . . . . 6 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) → ((invg𝐻)‘𝑎) ∈ 𝑆)
4339, 42eqeltrrd 2854 . . . . 5 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) → ((invg𝐺)‘𝑎) ∈ 𝑆)
4422, 43jca 516 . . . 4 ((((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) ∧ 𝑎𝑆) → (∀𝑏𝑆 (𝑎(+g𝐺)𝑏) ∈ 𝑆 ∧ ((invg𝐺)‘𝑎) ∈ 𝑆))
4544ralrimiva 3114 . . 3 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → ∀𝑎𝑆 (∀𝑏𝑆 (𝑎(+g𝐺)𝑏) ∈ 𝑆 ∧ ((invg𝐺)‘𝑎) ∈ 𝑆))
46 eqid 2759 . . . . 5 (+g𝐺) = (+g𝐺)
47 eqid 2759 . . . . 5 (invg𝐺) = (invg𝐺)
4819, 46, 47issubg2 18351 . . . 4 (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑎𝑆 (∀𝑏𝑆 (𝑎(+g𝐺)𝑏) ∈ 𝑆 ∧ ((invg𝐺)‘𝑎) ∈ 𝑆))))
4948ad2antrr 726 . . 3 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆𝐵𝑆 ≠ ∅ ∧ ∀𝑎𝑆 (∀𝑏𝑆 (𝑎(+g𝐺)𝑏) ∈ 𝑆 ∧ ((invg𝐺)‘𝑎) ∈ 𝑆))))
502, 5, 45, 49mpbir3and 1340 . 2 (((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) ∧ (𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆)))) → 𝑆 ∈ (SubGrp‘𝐺))
5150ex 417 1 ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆𝐵 ∧ (+g𝐻) = ((+g𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071   ⊆ wss 3859  ∅c0 4226   × cxp 5520   ↾ cres 5524  ‘cfv 6333  (class class class)co 7148  Basecbs 16531  +gcplusg 16613  Mgmcmgm 17906  Mndcmnd 17967  Grpcgrp 18159  invgcminusg 18160  SubGrpcsubg 18330 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-er 8297  df-en 8526  df-dom 8527  df-sdom 8528  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-nn 11665  df-2 11727  df-ndx 16534  df-slot 16535  df-base 16537  df-sets 16538  df-ress 16539  df-plusg 16626  df-0g 16763  df-mgm 17908  df-sgrp 17957  df-mnd 17968  df-grp 18162  df-minusg 18163  df-subg 18333 This theorem is referenced by:  resgrpisgrp  18357  pgrpsubgsymg  18594
 Copyright terms: Public domain W3C validator