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 ⊢ S ∈ SubMnd ⁡ G → A ∈ SubMnd ⁡ H ↔ A ∈ SubMnd ⁡ G ∧ A ⊆ S

Proof

Step Hyp Ref Expression
1 subsubm.h ⊢ H = G ↾ 𝑠 S
2 eqid ⊢ Base H = Base H
3 2 submss ⊢ A ∈ SubMnd ⁡ H → A ⊆ Base H
4 3 adantl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → A ⊆ Base H
5 1 submbas ⊢ S ∈ SubMnd ⁡ G → S = Base H
6 5 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → S = Base H
7 4 6 sseqtrrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → A ⊆ S
8 eqid ⊢ Base G = Base G
9 8 submss ⊢ S ∈ SubMnd ⁡ G → S ⊆ Base G
10 9 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → S ⊆ Base G
11 7 10 sstrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → A ⊆ Base G
12 eqid ⊢ 0 G = 0 G
13 1 12 subm0 ⊢ S ∈ SubMnd ⁡ G → 0 G = 0 H
14 13 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → 0 G = 0 H
15 eqid ⊢ 0 H = 0 H
16 15 subm0cl ⊢ A ∈ SubMnd ⁡ H → 0 H ∈ A
17 16 adantl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → 0 H ∈ A
18 14 17 eqeltrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → 0 G ∈ A
19 1 oveq1i ⊢ H ↾ 𝑠 A = G ↾ 𝑠 S ↾ 𝑠 A
20 ressabs ⊢ S ∈ SubMnd ⁡ G ∧ A ⊆ S → G ↾ 𝑠 S ↾ 𝑠 A = G ↾ 𝑠 A
21 19 20 syl5eq ⊢ S ∈ SubMnd ⁡ G ∧ A ⊆ S → H ↾ 𝑠 A = G ↾ 𝑠 A
22 7 21 syldan ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → H ↾ 𝑠 A = G ↾ 𝑠 A
23 eqid ⊢ H ↾ 𝑠 A = H ↾ 𝑠 A
24 23 submmnd ⊢ A ∈ SubMnd ⁡ H → H ↾ 𝑠 A ∈ Mnd
25 24 adantl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → H ↾ 𝑠 A ∈ Mnd
26 22 25 eqeltrrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → G ↾ 𝑠 A ∈ Mnd
27 submrcl ⊢ S ∈ SubMnd ⁡ G → G ∈ Mnd
28 27 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → G ∈ Mnd
29 eqid ⊢ G ↾ 𝑠 A = G ↾ 𝑠 A
30 8 12 29 issubm2 ⊢ G ∈ Mnd → A ∈ SubMnd ⁡ G ↔ A ⊆ Base G ∧ 0 G ∈ A ∧ G ↾ 𝑠 A ∈ Mnd
31 28 30 syl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → A ∈ SubMnd ⁡ G ↔ A ⊆ Base G ∧ 0 G ∈ A ∧ G ↾ 𝑠 A ∈ Mnd
32 11 18 26 31 mpbir3and ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → A ∈ SubMnd ⁡ G
33 32 7 jca ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ H → A ∈ SubMnd ⁡ G ∧ A ⊆ S
34 simprr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → A ⊆ S
35 5 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → S = Base H
36 34 35 sseqtrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → A ⊆ Base H
37 13 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → 0 G = 0 H
38 12 subm0cl ⊢ A ∈ SubMnd ⁡ G → 0 G ∈ A
39 38 ad2antrl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → 0 G ∈ A
40 37 39 eqeltrrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → 0 H ∈ A
41 21 adantrl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → H ↾ 𝑠 A = G ↾ 𝑠 A
42 29 submmnd ⊢ A ∈ SubMnd ⁡ G → G ↾ 𝑠 A ∈ Mnd
43 42 ad2antrl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → G ↾ 𝑠 A ∈ Mnd
44 41 43 eqeltrd ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → H ↾ 𝑠 A ∈ Mnd
45 1 submmnd ⊢ S ∈ SubMnd ⁡ G → H ∈ Mnd
46 45 adantr ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → H ∈ Mnd
47 2 15 23 issubm2 ⊢ H ∈ Mnd → A ∈ SubMnd ⁡ H ↔ A ⊆ Base H ∧ 0 H ∈ A ∧ H ↾ 𝑠 A ∈ Mnd
48 46 47 syl ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → A ∈ SubMnd ⁡ H ↔ A ⊆ Base H ∧ 0 H ∈ A ∧ H ↾ 𝑠 A ∈ Mnd
49 36 40 44 48 mpbir3and ⊢ S ∈ SubMnd ⁡ G ∧ A ∈ SubMnd ⁡ G ∧ A ⊆ S → A ∈ SubMnd ⁡ H
50 33 49 impbida ⊢ S ∈ SubMnd ⁡ G → A ∈ SubMnd ⁡ H ↔ A ∈ SubMnd ⁡ G ∧ A ⊆ S