Step | Hyp | Ref
| Expression |
1 | | issubmgm2.b |
. . 3
⊢ 𝐵 = (Base‘𝑀) |
2 | | eqid 2748 |
. . 3
⊢
(+g‘𝑀) = (+g‘𝑀) |
3 | 1, 2 | issubmgm 42268 |
. 2
⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆))) |
4 | | issubmgm2.h |
. . . . . . 7
⊢ 𝐻 = (𝑀 ↾s 𝑆) |
5 | 4, 1 | ressbas2 16104 |
. . . . . 6
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
6 | 5 | ad2antlr 765 |
. . . . 5
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝑆 = (Base‘𝐻)) |
7 | | ovex 6829 |
. . . . . . 7
⊢ (𝑀 ↾s 𝑆) ∈ V |
8 | 4, 7 | eqeltri 2823 |
. . . . . 6
⊢ 𝐻 ∈ V |
9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝐻 ∈ V) |
10 | | fvex 6350 |
. . . . . . . . 9
⊢
(Base‘𝑀)
∈ V |
11 | 1, 10 | eqeltri 2823 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
12 | 11 | ssex 4942 |
. . . . . . 7
⊢ (𝑆 ⊆ 𝐵 → 𝑆 ∈ V) |
13 | 12 | ad2antlr 765 |
. . . . . 6
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝑆 ∈ V) |
14 | 4, 2 | ressplusg 16166 |
. . . . . 6
⊢ (𝑆 ∈ V →
(+g‘𝑀) =
(+g‘𝐻)) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → (+g‘𝑀) = (+g‘𝐻)) |
16 | | oveq1 6808 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑥(+g‘𝑀)𝑦) = (𝑎(+g‘𝑀)𝑦)) |
17 | 16 | eleq1d 2812 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝑥(+g‘𝑀)𝑦) ∈ 𝑆 ↔ (𝑎(+g‘𝑀)𝑦) ∈ 𝑆)) |
18 | | oveq2 6809 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → (𝑎(+g‘𝑀)𝑦) = (𝑎(+g‘𝑀)𝑏)) |
19 | 18 | eleq1d 2812 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → ((𝑎(+g‘𝑀)𝑦) ∈ 𝑆 ↔ (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
20 | 17, 19 | rspc2v 3449 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆 → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
21 | 20 | com12 32 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆 → ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
22 | 21 | adantl 473 |
. . . . . 6
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
23 | 22 | 3impib 1108 |
. . . . 5
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆) |
24 | 6, 9, 15, 23 | ismgmd 42255 |
. . . 4
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝐻 ∈ Mgm) |
25 | | simplr 809 |
. . . . . . 7
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐻 ∈ Mgm) |
26 | | simprl 811 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
27 | 5 | ad3antlr 769 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑆 = (Base‘𝐻)) |
28 | 26, 27 | eleqtrd 2829 |
. . . . . . 7
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐻)) |
29 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
30 | 29 | adantl 473 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
31 | 30, 27 | eleqtrd 2829 |
. . . . . . 7
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐻)) |
32 | | eqid 2748 |
. . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) |
33 | | eqid 2748 |
. . . . . . . 8
⊢
(+g‘𝐻) = (+g‘𝐻) |
34 | 32, 33 | mgmcl 17417 |
. . . . . . 7
⊢ ((𝐻 ∈ Mgm ∧ 𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
35 | 25, 28, 31, 34 | syl3anc 1463 |
. . . . . 6
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
36 | 12 | ad2antlr 765 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑆 ∈ V) |
37 | 36, 14 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) →
(+g‘𝑀) =
(+g‘𝐻)) |
38 | 37 | oveqdr 6825 |
. . . . . 6
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
39 | 35, 38, 27 | 3eltr4d 2842 |
. . . . 5
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
40 | 39 | ralrimivva 3097 |
. . . 4
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
41 | 24, 40 | impbida 913 |
. . 3
⊢ ((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆 ↔ 𝐻 ∈ Mgm)) |
42 | 41 | pm5.32da 676 |
. 2
⊢ (𝑀 ∈ Mgm → ((𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm))) |
43 | 3, 42 | bitrd 268 |
1
⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm))) |