| Step | Hyp | Ref
| Expression |
| 1 | | fvexd 6921 |
. . 3
⊢ (𝑔 = 𝑀 → (Base‘𝑔) ∈ V) |
| 2 | | fveq2 6906 |
. . . 4
⊢ (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀)) |
| 3 | | issgrp.b |
. . . 4
⊢ 𝐵 = (Base‘𝑀) |
| 4 | 2, 3 | eqtr4di 2795 |
. . 3
⊢ (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵) |
| 5 | | fvexd 6921 |
. . . 4
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) ∈ V) |
| 6 | | fveq2 6906 |
. . . . . 6
⊢ (𝑔 = 𝑀 → (+g‘𝑔) = (+g‘𝑀)) |
| 7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = (+g‘𝑀)) |
| 8 | | issgrp.o |
. . . . 5
⊢ ⚬ =
(+g‘𝑀) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . 4
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = ⚬ ) |
| 10 | | simplr 769 |
. . . . 5
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵) |
| 11 | | id 22 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑜 = ⚬ ) |
| 12 | | oveq 7437 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦)) |
| 13 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑧 = 𝑧) |
| 14 | 11, 12, 13 | oveq123d 7452 |
. . . . . . . . 9
⊢ (𝑜 = ⚬ → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 ⚬ 𝑦) ⚬ 𝑧)) |
| 15 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑥 = 𝑥) |
| 16 | | oveq 7437 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → (𝑦𝑜𝑧) = (𝑦 ⚬ 𝑧)) |
| 17 | 11, 15, 16 | oveq123d 7452 |
. . . . . . . . 9
⊢ (𝑜 = ⚬ → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) |
| 18 | 14, 17 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑜 = ⚬ → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 19 | 18 | adantl 481 |
. . . . . . 7
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 20 | 10, 19 | raleqbidv 3346 |
. . . . . 6
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 21 | 10, 20 | raleqbidv 3346 |
. . . . 5
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 22 | 10, 21 | raleqbidv 3346 |
. . . 4
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 23 | 5, 9, 22 | sbcied2 3833 |
. . 3
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → ([(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 24 | 1, 4, 23 | sbcied2 3833 |
. 2
⊢ (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
| 25 | | df-sgrp 18732 |
. 2
⊢ Smgrp =
{𝑔 ∈ Mgm ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} |
| 26 | 24, 25 | elrab2 3695 |
1
⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |