Metamath Proof Explorer

Theorem subsubm

Description: A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypothesis subsubm.h 
|- H = ( G |`s S )
Assertion subsubm 
|- ( S e. ( SubMnd ` G ) -> ( A e. ( SubMnd ` H ) <-> ( A e. ( SubMnd ` G ) /\ A C_ S ) ) )

Proof

Step Hyp Ref Expression
1 subsubm.h 
 |-  H = ( G |`s S )
2 eqid 
 |-  ( Base ` H ) = ( Base ` H )
3 2 submss 
 |-  ( A e. ( SubMnd ` H ) -> A C_ ( Base ` H ) )
4 3 adantl 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> A C_ ( Base ` H ) )
5 1 submbas 
 |-  ( S e. ( SubMnd ` G ) -> S = ( Base ` H ) )
6 5 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> S = ( Base ` H ) )
7 4 6 sseqtrrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> A C_ S )
8 eqid 
 |-  ( Base ` G ) = ( Base ` G )
9 8 submss 
 |-  ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
10 9 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> S C_ ( Base ` G ) )
11 7 10 sstrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> A C_ ( Base ` G ) )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 1 12 subm0 
 |-  ( S e. ( SubMnd ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
14 13 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( 0g ` G ) = ( 0g ` H ) )
15 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
16 15 subm0cl 
 |-  ( A e. ( SubMnd ` H ) -> ( 0g ` H ) e. A )
17 16 adantl 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( 0g ` H ) e. A )
18 14 17 eqeltrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( 0g ` G ) e. A )
19 1 oveq1i 
 |-  ( H |`s A ) = ( ( G |`s S ) |`s A )
20 ressabs 
 |-  ( ( S e. ( SubMnd ` G ) /\ A C_ S ) -> ( ( G |`s S ) |`s A ) = ( G |`s A ) )
21 19 20 eqtrid 
 |-  ( ( S e. ( SubMnd ` G ) /\ A C_ S ) -> ( H |`s A ) = ( G |`s A ) )
22 7 21 syldan 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( H |`s A ) = ( G |`s A ) )
23 eqid 
 |-  ( H |`s A ) = ( H |`s A )
24 23 submmnd 
 |-  ( A e. ( SubMnd ` H ) -> ( H |`s A ) e. Mnd )
25 24 adantl 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( H |`s A ) e. Mnd )
26 22 25 eqeltrrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( G |`s A ) e. Mnd )
27 submrcl 
 |-  ( S e. ( SubMnd ` G ) -> G e. Mnd )
28 27 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> G e. Mnd )
29 eqid 
 |-  ( G |`s A ) = ( G |`s A )
30 8 12 29 issubm2 
 |-  ( G e. Mnd -> ( A e. ( SubMnd ` G ) <-> ( A C_ ( Base ` G ) /\ ( 0g ` G ) e. A /\ ( G |`s A ) e. Mnd ) ) )
31 28 30 syl 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( A e. ( SubMnd ` G ) <-> ( A C_ ( Base ` G ) /\ ( 0g ` G ) e. A /\ ( G |`s A ) e. Mnd ) ) )
32 11 18 26 31 mpbir3and 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> A e. ( SubMnd ` G ) )
33 32 7 jca 
 |-  ( ( S e. ( SubMnd ` G ) /\ A e. ( SubMnd ` H ) ) -> ( A e. ( SubMnd ` G ) /\ A C_ S ) )
34 simprr 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> A C_ S )
35 5 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> S = ( Base ` H ) )
36 34 35 sseqtrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> A C_ ( Base ` H ) )
37 13 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( 0g ` G ) = ( 0g ` H ) )
38 12 subm0cl 
 |-  ( A e. ( SubMnd ` G ) -> ( 0g ` G ) e. A )
39 38 ad2antrl 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( 0g ` G ) e. A )
40 37 39 eqeltrrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( 0g ` H ) e. A )
41 21 adantrl 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( H |`s A ) = ( G |`s A ) )
42 29 submmnd 
 |-  ( A e. ( SubMnd ` G ) -> ( G |`s A ) e. Mnd )
43 42 ad2antrl 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( G |`s A ) e. Mnd )
44 41 43 eqeltrd 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( H |`s A ) e. Mnd )
45 1 submmnd 
 |-  ( S e. ( SubMnd ` G ) -> H e. Mnd )
46 45 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> H e. Mnd )
47 2 15 23 issubm2 
 |-  ( H e. Mnd -> ( A e. ( SubMnd ` H ) <-> ( A C_ ( Base ` H ) /\ ( 0g ` H ) e. A /\ ( H |`s A ) e. Mnd ) ) )
48 46 47 syl 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> ( A e. ( SubMnd ` H ) <-> ( A C_ ( Base ` H ) /\ ( 0g ` H ) e. A /\ ( H |`s A ) e. Mnd ) ) )
49 36 40 44 48 mpbir3and 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( A e. ( SubMnd ` G ) /\ A C_ S ) ) -> A e. ( SubMnd ` H ) )
50 33 49 impbida 
 |-  ( S e. ( SubMnd ` G ) -> ( A e. ( SubMnd ` H ) <-> ( A e. ( SubMnd ` G ) /\ A C_ S ) ) )