Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . 4
⊢
(Base‘𝑔)
∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑔 = 𝑀 → (Base‘𝑔) ∈ V) |
3 | | fveq2 6103 |
. . . 4
⊢ (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀)) |
4 | | issgrp.b |
. . . 4
⊢ 𝐵 = (Base‘𝑀) |
5 | 3, 4 | syl6eqr 2662 |
. . 3
⊢ (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵) |
6 | | fvex 6113 |
. . . . 5
⊢
(+g‘𝑔) ∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) ∈ V) |
8 | | fveq2 6103 |
. . . . . 6
⊢ (𝑔 = 𝑀 → (+g‘𝑔) = (+g‘𝑀)) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = (+g‘𝑀)) |
10 | | issgrp.o |
. . . . 5
⊢ ⚬ =
(+g‘𝑀) |
11 | 9, 10 | syl6eqr 2662 |
. . . 4
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = ⚬ ) |
12 | | simplr 788 |
. . . . 5
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵) |
13 | | id 22 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑜 = ⚬ ) |
14 | | oveq 6555 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦)) |
15 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑧 = 𝑧) |
16 | 13, 14, 15 | oveq123d 6570 |
. . . . . . . . 9
⊢ (𝑜 = ⚬ → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 ⚬ 𝑦) ⚬ 𝑧)) |
17 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑥 = 𝑥) |
18 | | oveq 6555 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → (𝑦𝑜𝑧) = (𝑦 ⚬ 𝑧)) |
19 | 13, 17, 18 | oveq123d 6570 |
. . . . . . . . 9
⊢ (𝑜 = ⚬ → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) |
20 | 16, 19 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑜 = ⚬ → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
22 | 12, 21 | raleqbidv 3129 |
. . . . . 6
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
23 | 12, 22 | raleqbidv 3129 |
. . . . 5
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
24 | 12, 23 | raleqbidv 3129 |
. . . 4
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
25 | 7, 11, 24 | sbcied2 3440 |
. . 3
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → ([(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
26 | 2, 5, 25 | sbcied2 3440 |
. 2
⊢ (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
27 | | df-sgrp 17107 |
. 2
⊢ SGrp =
{𝑔 ∈ Mgm ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} |
28 | 26, 27 | elrab2 3333 |
1
⊢ (𝑀 ∈ SGrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |