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

Theorem subsubg 18302
Description: A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.)
Hypothesis
Ref Expression
subsubg.h 𝐻 = (𝐺s 𝑆)
Assertion
Ref Expression
subsubg (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)))

Proof of Theorem subsubg
StepHypRef Expression
1 subgrcl 18284 . . . . 5 (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
21adantr 484 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝐺 ∈ Grp)
3 eqid 2824 . . . . . . . 8 (Base‘𝐻) = (Base‘𝐻)
43subgss 18280 . . . . . . 7 (𝐴 ∈ (SubGrp‘𝐻) → 𝐴 ⊆ (Base‘𝐻))
54adantl 485 . . . . . 6 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝐴 ⊆ (Base‘𝐻))
6 subsubg.h . . . . . . . 8 𝐻 = (𝐺s 𝑆)
76subgbas 18283 . . . . . . 7 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻))
87adantr 484 . . . . . 6 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝑆 = (Base‘𝐻))
95, 8sseqtrrd 3994 . . . . 5 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝐴𝑆)
10 eqid 2824 . . . . . . 7 (Base‘𝐺) = (Base‘𝐺)
1110subgss 18280 . . . . . 6 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺))
1211adantr 484 . . . . 5 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝑆 ⊆ (Base‘𝐺))
139, 12sstrd 3963 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝐴 ⊆ (Base‘𝐺))
146oveq1i 7159 . . . . . . 7 (𝐻s 𝐴) = ((𝐺s 𝑆) ↾s 𝐴)
15 ressabs 16563 . . . . . . 7 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆) → ((𝐺s 𝑆) ↾s 𝐴) = (𝐺s 𝐴))
1614, 15syl5eq 2871 . . . . . 6 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆) → (𝐻s 𝐴) = (𝐺s 𝐴))
179, 16syldan 594 . . . . 5 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → (𝐻s 𝐴) = (𝐺s 𝐴))
18 eqid 2824 . . . . . . 7 (𝐻s 𝐴) = (𝐻s 𝐴)
1918subggrp 18282 . . . . . 6 (𝐴 ∈ (SubGrp‘𝐻) → (𝐻s 𝐴) ∈ Grp)
2019adantl 485 . . . . 5 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → (𝐻s 𝐴) ∈ Grp)
2117, 20eqeltrrd 2917 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → (𝐺s 𝐴) ∈ Grp)
2210issubg 18279 . . . 4 (𝐴 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝐺) ∧ (𝐺s 𝐴) ∈ Grp))
232, 13, 21, 22syl3anbrc 1340 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → 𝐴 ∈ (SubGrp‘𝐺))
2423, 9jca 515 . 2 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (SubGrp‘𝐻)) → (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆))
256subggrp 18282 . . . 4 (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
2625adantr 484 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → 𝐻 ∈ Grp)
27 simprr 772 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → 𝐴𝑆)
287adantr 484 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → 𝑆 = (Base‘𝐻))
2927, 28sseqtrd 3993 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → 𝐴 ⊆ (Base‘𝐻))
3016adantrl 715 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → (𝐻s 𝐴) = (𝐺s 𝐴))
31 eqid 2824 . . . . . 6 (𝐺s 𝐴) = (𝐺s 𝐴)
3231subggrp 18282 . . . . 5 (𝐴 ∈ (SubGrp‘𝐺) → (𝐺s 𝐴) ∈ Grp)
3332ad2antrl 727 . . . 4 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → (𝐺s 𝐴) ∈ Grp)
3430, 33eqeltrd 2916 . . 3 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → (𝐻s 𝐴) ∈ Grp)
353issubg 18279 . . 3 (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐻 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝐻) ∧ (𝐻s 𝐴) ∈ Grp))
3626, 29, 34, 35syl3anbrc 1340 . 2 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)) → 𝐴 ∈ (SubGrp‘𝐻))
3724, 36impbida 800 1 (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wss 3919  cfv 6343  (class class class)co 7149  Basecbs 16483  s cress 16484  Grpcgrp 18103  SubGrpcsubg 18273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-1cn 10593  ax-addcl 10595
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-nn 11635  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-subg 18276
This theorem is referenced by:  nmznsg  18320  subgslw  18741  subgdmdprd  19156  subgdprd  19157  ablfac1c  19193  pgpfaclem1  19203  pgpfaclem2  19204  ablfaclem3  19209
  Copyright terms: Public domain W3C validator