Metamath Proof Explorer


Theorem subsubg

Description: A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis subsubg.h 𝐻 = ( 𝐺s 𝑆 )
Assertion subsubg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 subsubg.h 𝐻 = ( 𝐺s 𝑆 )
2 subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3 2 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝐺 ∈ Grp )
4 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5 4 subgss ( 𝐴 ∈ ( SubGrp ‘ 𝐻 ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
6 5 adantl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
7 1 subgbas ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
8 7 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
9 6 8 sseqtrrd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝐴𝑆 )
10 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 10 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
12 11 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 9 12 sstrd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
14 1 oveq1i ( 𝐻s 𝐴 ) = ( ( 𝐺s 𝑆 ) ↾s 𝐴 )
15 ressabs ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) → ( ( 𝐺s 𝑆 ) ↾s 𝐴 ) = ( 𝐺s 𝐴 ) )
16 14 15 eqtrid ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) → ( 𝐻s 𝐴 ) = ( 𝐺s 𝐴 ) )
17 9 16 syldan ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → ( 𝐻s 𝐴 ) = ( 𝐺s 𝐴 ) )
18 eqid ( 𝐻s 𝐴 ) = ( 𝐻s 𝐴 )
19 18 subggrp ( 𝐴 ∈ ( SubGrp ‘ 𝐻 ) → ( 𝐻s 𝐴 ) ∈ Grp )
20 19 adantl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → ( 𝐻s 𝐴 ) ∈ Grp )
21 17 20 eqeltrrd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → ( 𝐺s 𝐴 ) ∈ Grp )
22 10 issubg ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺s 𝐴 ) ∈ Grp ) )
23 3 13 21 22 syl3anbrc ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
24 23 9 jca ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ) → ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) )
25 1 subggrp ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
26 25 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐻 ∈ Grp )
27 simprr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐴𝑆 )
28 7 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
29 27 28 sseqtrd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐴 ⊆ ( Base ‘ 𝐻 ) )
30 16 adantrl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐻s 𝐴 ) = ( 𝐺s 𝐴 ) )
31 eqid ( 𝐺s 𝐴 ) = ( 𝐺s 𝐴 )
32 31 subggrp ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺s 𝐴 ) ∈ Grp )
33 32 ad2antrl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐺s 𝐴 ) ∈ Grp )
34 30 33 eqeltrd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → ( 𝐻s 𝐴 ) ∈ Grp )
35 4 issubg ( 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝐻 ∈ Grp ∧ 𝐴 ⊆ ( Base ‘ 𝐻 ) ∧ ( 𝐻s 𝐴 ) ∈ Grp ) )
36 26 29 34 35 syl3anbrc ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) → 𝐴 ∈ ( SubGrp ‘ 𝐻 ) )
37 24 36 impbida ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑆 ) ) )