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 syl5eq ⊢ ( ( 𝑆 ∈ ( 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 ‘ 𝐺 ) ∧ 𝐴 ⊆ 𝑆 ) ) )