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
Assertion subsubm SSubMndGASubMndHASubMndGAS

Proof

Step Hyp Ref Expression
1 subsubm.h H=G𝑠S
2 eqid BaseH=BaseH
3 2 submss ASubMndHABaseH
4 3 adantl SSubMndGASubMndHABaseH
5 1 submbas SSubMndGS=BaseH
6 5 adantr SSubMndGASubMndHS=BaseH
7 4 6 sseqtrrd SSubMndGASubMndHAS
8 eqid BaseG=BaseG
9 8 submss SSubMndGSBaseG
10 9 adantr SSubMndGASubMndHSBaseG
11 7 10 sstrd SSubMndGASubMndHABaseG
12 eqid 0G=0G
13 1 12 subm0 SSubMndG0G=0H
14 13 adantr SSubMndGASubMndH0G=0H
15 eqid 0H=0H
16 15 subm0cl ASubMndH0HA
17 16 adantl SSubMndGASubMndH0HA
18 14 17 eqeltrd SSubMndGASubMndH0GA
19 1 oveq1i H𝑠A=G𝑠S𝑠A
20 ressabs SSubMndGASG𝑠S𝑠A=G𝑠A
21 19 20 eqtrid SSubMndGASH𝑠A=G𝑠A
22 7 21 syldan SSubMndGASubMndHH𝑠A=G𝑠A
23 eqid H𝑠A=H𝑠A
24 23 submmnd ASubMndHH𝑠AMnd
25 24 adantl SSubMndGASubMndHH𝑠AMnd
26 22 25 eqeltrrd SSubMndGASubMndHG𝑠AMnd
27 submrcl SSubMndGGMnd
28 27 adantr SSubMndGASubMndHGMnd
29 eqid G𝑠A=G𝑠A
30 8 12 29 issubm2 GMndASubMndGABaseG0GAG𝑠AMnd
31 28 30 syl SSubMndGASubMndHASubMndGABaseG0GAG𝑠AMnd
32 11 18 26 31 mpbir3and SSubMndGASubMndHASubMndG
33 32 7 jca SSubMndGASubMndHASubMndGAS
34 simprr SSubMndGASubMndGASAS
35 5 adantr SSubMndGASubMndGASS=BaseH
36 34 35 sseqtrd SSubMndGASubMndGASABaseH
37 13 adantr SSubMndGASubMndGAS0G=0H
38 12 subm0cl ASubMndG0GA
39 38 ad2antrl SSubMndGASubMndGAS0GA
40 37 39 eqeltrrd SSubMndGASubMndGAS0HA
41 21 adantrl SSubMndGASubMndGASH𝑠A=G𝑠A
42 29 submmnd ASubMndGG𝑠AMnd
43 42 ad2antrl SSubMndGASubMndGASG𝑠AMnd
44 41 43 eqeltrd SSubMndGASubMndGASH𝑠AMnd
45 1 submmnd SSubMndGHMnd
46 45 adantr SSubMndGASubMndGASHMnd
47 2 15 23 issubm2 HMndASubMndHABaseH0HAH𝑠AMnd
48 46 47 syl SSubMndGASubMndGASASubMndHABaseH0HAH𝑠AMnd
49 36 40 44 48 mpbir3and SSubMndGASubMndGASASubMndH
50 33 49 impbida SSubMndGASubMndHASubMndGAS