Step | Hyp | Ref
| Expression |
1 | | issubmgm2.b |
. . 3
⊢ 𝐵 = (Base‘𝑀) |
2 | | eqid 2610 |
. . 3
⊢
(+g‘𝑀) = (+g‘𝑀) |
3 | 1, 2 | issubmgm 41579 |
. 2
⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆))) |
4 | | issubmgm2.h |
. . . . . . 7
⊢ 𝐻 = (𝑀 ↾s 𝑆) |
5 | 4, 1 | ressbas2 15758 |
. . . . . 6
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
6 | 5 | ad2antlr 759 |
. . . . 5
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝑆 = (Base‘𝐻)) |
7 | | ovex 6577 |
. . . . . . 7
⊢ (𝑀 ↾s 𝑆) ∈ V |
8 | 4, 7 | eqeltri 2684 |
. . . . . 6
⊢ 𝐻 ∈ V |
9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝐻 ∈ V) |
10 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑀)
∈ V |
11 | 1, 10 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
12 | 11 | ssex 4730 |
. . . . . . 7
⊢ (𝑆 ⊆ 𝐵 → 𝑆 ∈ V) |
13 | 12 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝑆 ∈ V) |
14 | 4, 2 | ressplusg 15818 |
. . . . . 6
⊢ (𝑆 ∈ V →
(+g‘𝑀) =
(+g‘𝐻)) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → (+g‘𝑀) = (+g‘𝐻)) |
16 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑥(+g‘𝑀)𝑦) = (𝑎(+g‘𝑀)𝑦)) |
17 | 16 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝑥(+g‘𝑀)𝑦) ∈ 𝑆 ↔ (𝑎(+g‘𝑀)𝑦) ∈ 𝑆)) |
18 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → (𝑎(+g‘𝑀)𝑦) = (𝑎(+g‘𝑀)𝑏)) |
19 | 18 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → ((𝑎(+g‘𝑀)𝑦) ∈ 𝑆 ↔ (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
20 | 17, 19 | rspc2v 3293 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆 → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
21 | 20 | com12 32 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆 → ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆)) |
23 | 22 | 3impib 1254 |
. . . . 5
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎(+g‘𝑀)𝑏) ∈ 𝑆) |
24 | 6, 9, 15, 23 | ismgmd 41566 |
. . . 4
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) → 𝐻 ∈ Mgm) |
25 | | simplr 788 |
. . . . . . 7
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐻 ∈ Mgm) |
26 | | simprl 790 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
27 | 5 | ad3antlr 763 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑆 = (Base‘𝐻)) |
28 | 26, 27 | eleqtrd 2690 |
. . . . . . 7
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐻)) |
29 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
30 | 29 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
31 | 30, 27 | eleqtrd 2690 |
. . . . . . 7
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐻)) |
32 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) |
33 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐻) = (+g‘𝐻) |
34 | 32, 33 | mgmcl 17068 |
. . . . . . 7
⊢ ((𝐻 ∈ Mgm ∧ 𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
35 | 25, 28, 31, 34 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
36 | 12 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑆 ∈ V) |
37 | 36, 14 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) →
(+g‘𝑀) =
(+g‘𝐻)) |
38 | 37 | oveqdr 6573 |
. . . . . 6
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
39 | 35, 38, 27 | 3eltr4d 2703 |
. . . . 5
⊢ ((((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
40 | 39 | ralrimivva 2954 |
. . . 4
⊢ (((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
41 | 24, 40 | impbida 873 |
. . 3
⊢ ((𝑀 ∈ Mgm ∧ 𝑆 ⊆ 𝐵) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆 ↔ 𝐻 ∈ Mgm)) |
42 | 41 | pm5.32da 671 |
. 2
⊢ (𝑀 ∈ Mgm → ((𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm))) |
43 | 3, 42 | bitrd 267 |
1
⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm))) |