Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐻 ∈ Mnd) |
2 | | simprl 790 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
3 | | simpll2 1094 |
. . . . . . 7
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑆 ⊆ 𝐵) |
4 | | issubmnd.h |
. . . . . . . 8
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
5 | | issubmnd.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | ressbas2 15758 |
. . . . . . 7
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
7 | 3, 6 | syl 17 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑆 = (Base‘𝐻)) |
8 | 2, 7 | eleqtrd 2690 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐻)) |
9 | | simprr 792 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
10 | 9, 7 | eleqtrd 2690 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐻)) |
11 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) |
12 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝐻) = (+g‘𝐻) |
13 | 11, 12 | mndcl 17124 |
. . . . 5
⊢ ((𝐻 ∈ Mnd ∧ 𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
14 | 1, 8, 10, 13 | syl3anc 1318 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
15 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝐺)
∈ V |
16 | 5, 15 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
17 | 16 | ssex 4730 |
. . . . . . . 8
⊢ (𝑆 ⊆ 𝐵 → 𝑆 ∈ V) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → 𝑆 ∈ V) |
19 | | issubmnd.p |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
20 | 4, 19 | ressplusg 15818 |
. . . . . . 7
⊢ (𝑆 ∈ V → + =
(+g‘𝐻)) |
21 | 18, 20 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → + =
(+g‘𝐻)) |
22 | 21 | ad2antrr 758 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → + =
(+g‘𝐻)) |
23 | 22 | oveqd 6566 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑥(+g‘𝐻)𝑦)) |
24 | 14, 23, 7 | 3eltr4d 2703 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
25 | 24 | ralrimivva 2954 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ 𝐻 ∈ Mnd) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
26 | | simpl2 1058 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝑆 ⊆ 𝐵) |
27 | 26, 6 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝑆 = (Base‘𝐻)) |
28 | 21 | adantr 480 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → + =
(+g‘𝐻)) |
29 | | ovrspc2v 6571 |
. . . . . 6
⊢ (((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆) |
30 | 29 | ancoms 468 |
. . . . 5
⊢
((∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 + 𝑣) ∈ 𝑆) |
31 | 30 | 3impb 1252 |
. . . 4
⊢
((∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆) |
32 | 31 | 3adant1l 1310 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆) |
33 | 26 | sseld 3567 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑢 ∈ 𝑆 → 𝑢 ∈ 𝐵)) |
34 | 26 | sseld 3567 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑣 ∈ 𝑆 → 𝑣 ∈ 𝐵)) |
35 | 26 | sseld 3567 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝑤 ∈ 𝑆 → 𝑤 ∈ 𝐵)) |
36 | 33, 34, 35 | 3anim123d 1398 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) |
37 | 36 | imp 444 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) |
38 | | simpl1 1057 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝐺 ∈ Mnd) |
39 | 5, 19 | mndass 17125 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
40 | 38, 39 | sylan 487 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
41 | 37, 40 | syldan 486 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
42 | | simpl3 1059 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 0 ∈ 𝑆) |
43 | 26 | sselda 3568 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝐵) |
44 | | issubmnd.z |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
45 | 5, 19, 44 | mndlid 17134 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑢 ∈ 𝐵) → ( 0 + 𝑢) = 𝑢) |
46 | 38, 45 | sylan 487 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢 ∈ 𝐵) → ( 0 + 𝑢) = 𝑢) |
47 | 43, 46 | syldan 486 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢 ∈ 𝑆) → ( 0 + 𝑢) = 𝑢) |
48 | 5, 19, 44 | mndrid 17135 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑢 ∈ 𝐵) → (𝑢 + 0 ) = 𝑢) |
49 | 38, 48 | sylan 487 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢 ∈ 𝐵) → (𝑢 + 0 ) = 𝑢) |
50 | 43, 49 | syldan 486 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ∧ 𝑢 ∈ 𝑆) → (𝑢 + 0 ) = 𝑢) |
51 | 27, 28, 32, 41, 42, 47, 50 | ismndd 17136 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝐻 ∈ Mnd) |
52 | 25, 51 | impbida 873 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) |