Metamath Proof Explorer

Theorem subsubmgm

Description: A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis subsubmgm.h ⊢ H = G ↾ 𝑠 S
Assertion subsubmgm ⊢ S ∈ SubMgm ⁡ G → A ∈ SubMgm ⁡ H ↔ A ∈ SubMgm ⁡ G ∧ A ⊆ S

Proof

Step Hyp Ref Expression
1 subsubmgm.h ⊢ H = G ↾ 𝑠 S
2 eqid ⊢ Base H = Base H
3 2 submgmss ⊢ A ∈ SubMgm ⁡ H → A ⊆ Base H
4 3 adantl ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → A ⊆ Base H
5 1 submgmbas ⊢ S ∈ SubMgm ⁡ G → S = Base H
6 5 adantr ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → S = Base H
7 4 6 sseqtrrd ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → A ⊆ S
8 eqid ⊢ Base G = Base G
9 8 submgmss ⊢ S ∈ SubMgm ⁡ G → S ⊆ Base G
10 9 adantr ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → S ⊆ Base G
11 7 10 sstrd ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → A ⊆ Base G
12 1 oveq1i ⊢ H ↾ 𝑠 A = G ↾ 𝑠 S ↾ 𝑠 A
13 ressabs ⊢ S ∈ SubMgm ⁡ G ∧ A ⊆ S → G ↾ 𝑠 S ↾ 𝑠 A = G ↾ 𝑠 A
14 12 13 syl5eq ⊢ S ∈ SubMgm ⁡ G ∧ A ⊆ S → H ↾ 𝑠 A = G ↾ 𝑠 A
15 7 14 syldan ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → H ↾ 𝑠 A = G ↾ 𝑠 A
16 eqid ⊢ H ↾ 𝑠 A = H ↾ 𝑠 A
17 16 submgmmgm ⊢ A ∈ SubMgm ⁡ H → H ↾ 𝑠 A ∈ Mgm
18 17 adantl ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → H ↾ 𝑠 A ∈ Mgm
19 15 18 eqeltrrd ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → G ↾ 𝑠 A ∈ Mgm
20 submgmrcl ⊢ S ∈ SubMgm ⁡ G → G ∈ Mgm
21 20 adantr ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → G ∈ Mgm
22 eqid ⊢ G ↾ 𝑠 A = G ↾ 𝑠 A
23 8 22 issubmgm2 ⊢ G ∈ Mgm → A ∈ SubMgm ⁡ G ↔ A ⊆ Base G ∧ G ↾ 𝑠 A ∈ Mgm
24 21 23 syl ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → A ∈ SubMgm ⁡ G ↔ A ⊆ Base G ∧ G ↾ 𝑠 A ∈ Mgm
25 11 19 24 mpbir2and ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → A ∈ SubMgm ⁡ G
26 25 7 jca ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ H → A ∈ SubMgm ⁡ G ∧ A ⊆ S
27 simprr ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → A ⊆ S
28 5 adantr ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → S = Base H
29 27 28 sseqtrd ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → A ⊆ Base H
30 14 adantrl ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → H ↾ 𝑠 A = G ↾ 𝑠 A
31 22 submgmmgm ⊢ A ∈ SubMgm ⁡ G → G ↾ 𝑠 A ∈ Mgm
32 31 ad2antrl ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → G ↾ 𝑠 A ∈ Mgm
33 30 32 eqeltrd ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → H ↾ 𝑠 A ∈ Mgm
34 1 submgmmgm ⊢ S ∈ SubMgm ⁡ G → H ∈ Mgm
35 34 adantr ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → H ∈ Mgm
36 2 16 issubmgm2 ⊢ H ∈ Mgm → A ∈ SubMgm ⁡ H ↔ A ⊆ Base H ∧ H ↾ 𝑠 A ∈ Mgm
37 35 36 syl ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → A ∈ SubMgm ⁡ H ↔ A ⊆ Base H ∧ H ↾ 𝑠 A ∈ Mgm
38 29 33 37 mpbir2and ⊢ S ∈ SubMgm ⁡ G ∧ A ∈ SubMgm ⁡ G ∧ A ⊆ S → A ∈ SubMgm ⁡ H
39 26 38 impbida ⊢ S ∈ SubMgm ⁡ G → A ∈ SubMgm ⁡ H ↔ A ∈ SubMgm ⁡ G ∧ A ⊆ S