| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
| 2 | 1 | pweqd 4617 |
. . . . 5
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) |
| 3 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀)) |
| 4 | 3 | oveqd 7448 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑥(+g‘𝑚)𝑦) = (𝑥(+g‘𝑀)𝑦)) |
| 5 | 4 | eleq1d 2826 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑥(+g‘𝑚)𝑦) ∈ 𝑡 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)) |
| 6 | 5 | 2ralbidv 3221 |
. . . . 5
⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)) |
| 7 | 2, 6 | rabeqbidv 3455 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑡 ∈ 𝒫 (Base‘𝑚) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡} = {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡}) |
| 8 | | df-submgm 18706 |
. . . 4
⊢ SubMgm =
(𝑚 ∈ Mgm ↦
{𝑡 ∈ 𝒫
(Base‘𝑚) ∣
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡}) |
| 9 | | fvex 6919 |
. . . . . 6
⊢
(Base‘𝑀)
∈ V |
| 10 | 9 | pwex 5380 |
. . . . 5
⊢ 𝒫
(Base‘𝑀) ∈
V |
| 11 | 10 | rabex 5339 |
. . . 4
⊢ {𝑡 ∈ 𝒫
(Base‘𝑀) ∣
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡} ∈ V |
| 12 | 7, 8, 11 | fvmpt 7016 |
. . 3
⊢ (𝑀 ∈ Mgm →
(SubMgm‘𝑀) = {𝑡 ∈ 𝒫
(Base‘𝑀) ∣
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡}) |
| 13 | 12 | eleq2d 2827 |
. 2
⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ 𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡})) |
| 14 | 9 | elpw2 5334 |
. . . 4
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)) |
| 15 | 14 | anbi1i 624 |
. . 3
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) ↔ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 16 | | eleq2 2830 |
. . . . . 6
⊢ (𝑡 = 𝑆 → ((𝑥(+g‘𝑀)𝑦) ∈ 𝑡 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 17 | 16 | raleqbi1dv 3338 |
. . . . 5
⊢ (𝑡 = 𝑆 → (∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡 ↔ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 18 | 17 | raleqbi1dv 3338 |
. . . 4
⊢ (𝑡 = 𝑆 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 19 | 18 | elrab 3692 |
. . 3
⊢ (𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡} ↔ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 20 | | issubmgm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
| 21 | 20 | sseq2i 4013 |
. . . 4
⊢ (𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ (Base‘𝑀)) |
| 22 | | issubmgm.p |
. . . . . . 7
⊢ + =
(+g‘𝑀) |
| 23 | 22 | oveqi 7444 |
. . . . . 6
⊢ (𝑥 + 𝑦) = (𝑥(+g‘𝑀)𝑦) |
| 24 | 23 | eleq1i 2832 |
. . . . 5
⊢ ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
| 25 | 24 | 2ralbii 3128 |
. . . 4
⊢
(∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
| 26 | 21, 25 | anbi12i 628 |
. . 3
⊢ ((𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ↔ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 27 | 15, 19, 26 | 3bitr4i 303 |
. 2
⊢ (𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡} ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) |
| 28 | 13, 27 | bitrdi 287 |
1
⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) |