Proof of Theorem issstrmgm
Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . 5
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐻 ∈ Mgm) |
2 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑆 ⊆ 𝐵) |
3 | | issstrmgm.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
4 | | issstrmgm.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐺) |
5 | 3, 4 | ressbas2 15758 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
6 | 2, 5 | syl 17 |
. . . . . . . . 9
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑆 = (Base‘𝐻)) |
7 | 6 | eleq2d 2673 |
. . . . . . . 8
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ (Base‘𝐻))) |
8 | 7 | biimpcd 238 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑆 → (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑥 ∈ (Base‘𝐻))) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑥 ∈ (Base‘𝐻))) |
10 | 9 | impcom 445 |
. . . . 5
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐻)) |
11 | 6 | eleq2d 2673 |
. . . . . . . 8
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ (Base‘𝐻))) |
12 | 11 | biimpcd 238 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑆 → (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑦 ∈ (Base‘𝐻))) |
13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → 𝑦 ∈ (Base‘𝐻))) |
14 | 13 | impcom 445 |
. . . . 5
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐻)) |
15 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) |
16 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝐻) = (+g‘𝐻) |
17 | 15, 16 | mgmcl 17068 |
. . . . 5
⊢ ((𝐻 ∈ Mgm ∧ 𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
18 | 1, 10, 14, 17 | syl3anc 1318 |
. . . 4
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
19 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝐺)
∈ V |
20 | 4, 19 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
21 | 20 | ssex 4730 |
. . . . . . . 8
⊢ (𝑆 ⊆ 𝐵 → 𝑆 ∈ V) |
22 | 21 | adantl 481 |
. . . . . . 7
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ V) |
23 | | issstrmgm.p |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
24 | 3, 23 | ressplusg 15818 |
. . . . . . 7
⊢ (𝑆 ∈ V → + =
(+g‘𝐻)) |
25 | 22, 24 | syl 17 |
. . . . . 6
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → + =
(+g‘𝐻)) |
26 | 25 | adantr 480 |
. . . . 5
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → + =
(+g‘𝐻)) |
27 | 26 | oveqdr 6573 |
. . . 4
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑥(+g‘𝐻)𝑦)) |
28 | 6 | adantr 480 |
. . . 4
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑆 = (Base‘𝐻)) |
29 | 18, 27, 28 | 3eltr4d 2703 |
. . 3
⊢ ((((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
30 | 29 | ralrimivva 2954 |
. 2
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ 𝐻 ∈ Mgm) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
31 | 5 | adantl 481 |
. . . . 5
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → 𝑆 = (Base‘𝐻)) |
32 | 25 | oveqd 6566 |
. . . . . . 7
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → (𝑥 + 𝑦) = (𝑥(+g‘𝐻)𝑦)) |
33 | 32, 31 | eleq12d 2682 |
. . . . . 6
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻))) |
34 | 31, 33 | raleqbidv 3129 |
. . . . 5
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ↔ ∀𝑦 ∈ (Base‘𝐻)(𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻))) |
35 | 31, 34 | raleqbidv 3129 |
. . . 4
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ↔ ∀𝑥 ∈ (Base‘𝐻)∀𝑦 ∈ (Base‘𝐻)(𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻))) |
36 | 35 | biimpa 500 |
. . 3
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ∀𝑥 ∈ (Base‘𝐻)∀𝑦 ∈ (Base‘𝐻)(𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
37 | 15, 16 | ismgm 17066 |
. . . 4
⊢ (𝐻 ∈ 𝑉 → (𝐻 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐻)∀𝑦 ∈ (Base‘𝐻)(𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻))) |
38 | 37 | ad2antrr 758 |
. . 3
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → (𝐻 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐻)∀𝑦 ∈ (Base‘𝐻)(𝑥(+g‘𝐻)𝑦) ∈ (Base‘𝐻))) |
39 | 36, 38 | mpbird 246 |
. 2
⊢ (((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → 𝐻 ∈ Mgm) |
40 | 30, 39 | impbida 873 |
1
⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → (𝐻 ∈ Mgm ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) |