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 
|- H = ( G |`s S )
Assertion subsubg 
|- ( S e. ( SubGrp ` G ) -> ( A e. ( SubGrp ` H ) <-> ( A e. ( SubGrp ` G ) /\ A C_ S ) ) )

Proof

Step Hyp Ref Expression
1 subsubg.h 
 |-  H = ( G |`s S )
2 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
3 2 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> G e. Grp )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 4 subgss 
 |-  ( A e. ( SubGrp ` H ) -> A C_ ( Base ` H ) )
6 5 adantl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> A C_ ( Base ` H ) )
7 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
8 7 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> S = ( Base ` H ) )
9 6 8 sseqtrrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> A C_ S )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 10 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
12 11 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> S C_ ( Base ` G ) )
13 9 12 sstrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> A C_ ( Base ` G ) )
14 1 oveq1i 
 |-  ( H |`s A ) = ( ( G |`s S ) |`s A )
15 ressabs 
 |-  ( ( S e. ( SubGrp ` G ) /\ A C_ S ) -> ( ( G |`s S ) |`s A ) = ( G |`s A ) )
16 14 15 syl5eq 
 |-  ( ( S e. ( SubGrp ` G ) /\ A C_ S ) -> ( H |`s A ) = ( G |`s A ) )
17 9 16 syldan 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> ( H |`s A ) = ( G |`s A ) )
18 eqid 
 |-  ( H |`s A ) = ( H |`s A )
19 18 subggrp 
 |-  ( A e. ( SubGrp ` H ) -> ( H |`s A ) e. Grp )
20 19 adantl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> ( H |`s A ) e. Grp )
21 17 20 eqeltrrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> ( G |`s A ) e. Grp )
22 10 issubg 
 |-  ( A e. ( SubGrp ` G ) <-> ( G e. Grp /\ A C_ ( Base ` G ) /\ ( G |`s A ) e. Grp ) )
23 3 13 21 22 syl3anbrc 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> A e. ( SubGrp ` G ) )
24 23 9 jca 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. ( SubGrp ` H ) ) -> ( A e. ( SubGrp ` G ) /\ A C_ S ) )
25 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
26 25 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> H e. Grp )
27 simprr 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> A C_ S )
28 7 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> S = ( Base ` H ) )
29 27 28 sseqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> A C_ ( Base ` H ) )
30 16 adantrl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> ( H |`s A ) = ( G |`s A ) )
31 eqid 
 |-  ( G |`s A ) = ( G |`s A )
32 31 subggrp 
 |-  ( A e. ( SubGrp ` G ) -> ( G |`s A ) e. Grp )
33 32 ad2antrl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> ( G |`s A ) e. Grp )
34 30 33 eqeltrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> ( H |`s A ) e. Grp )
35 4 issubg 
 |-  ( A e. ( SubGrp ` H ) <-> ( H e. Grp /\ A C_ ( Base ` H ) /\ ( H |`s A ) e. Grp ) )
36 26 29 34 35 syl3anbrc 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( A e. ( SubGrp ` G ) /\ A C_ S ) ) -> A e. ( SubGrp ` H ) )
37 24 36 impbida 
 |-  ( S e. ( SubGrp ` G ) -> ( A e. ( SubGrp ` H ) <-> ( A e. ( SubGrp ` G ) /\ A C_ S ) ) )