Step | Hyp | Ref
| Expression |
1 | | basfn 12473 |
. . . . 5
⊢ Base Fn
V |
2 | | vex 2733 |
. . . . 5
⊢ 𝑔 ∈ V |
3 | | funfvex 5513 |
. . . . . 6
⊢ ((Fun
Base ∧ 𝑔 ∈ dom
Base) → (Base‘𝑔)
∈ V) |
4 | 3 | funfni 5298 |
. . . . 5
⊢ ((Base Fn
V ∧ 𝑔 ∈ V) →
(Base‘𝑔) ∈
V) |
5 | 1, 2, 4 | mp2an 424 |
. . . 4
⊢
(Base‘𝑔)
∈ V |
6 | 5 | a1i 9 |
. . 3
⊢ (𝑔 = 𝑀 → (Base‘𝑔) ∈ V) |
7 | | fveq2 5496 |
. . . 4
⊢ (𝑔 = 𝑀 → (Base‘𝑔) = (Base‘𝑀)) |
8 | | issgrp.b |
. . . 4
⊢ 𝐵 = (Base‘𝑀) |
9 | 7, 8 | eqtr4di 2221 |
. . 3
⊢ (𝑔 = 𝑀 → (Base‘𝑔) = 𝐵) |
10 | | plusgslid 12513 |
. . . . . . 7
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
11 | 10 | slotex 12443 |
. . . . . 6
⊢ (𝑔 ∈ V →
(+g‘𝑔)
∈ V) |
12 | 11 | elv 2734 |
. . . . 5
⊢
(+g‘𝑔) ∈ V |
13 | 12 | a1i 9 |
. . . 4
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) ∈ V) |
14 | | fveq2 5496 |
. . . . . 6
⊢ (𝑔 = 𝑀 → (+g‘𝑔) = (+g‘𝑀)) |
15 | 14 | adantr 274 |
. . . . 5
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = (+g‘𝑀)) |
16 | | issgrp.o |
. . . . 5
⊢ ⚬ =
(+g‘𝑀) |
17 | 15, 16 | eqtr4di 2221 |
. . . 4
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → (+g‘𝑔) = ⚬ ) |
18 | | simplr 525 |
. . . . 5
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵) |
19 | | id 19 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑜 = ⚬ ) |
20 | | oveq 5859 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → (𝑥𝑜𝑦) = (𝑥 ⚬ 𝑦)) |
21 | | eqidd 2171 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑧 = 𝑧) |
22 | 19, 20, 21 | oveq123d 5874 |
. . . . . . . . 9
⊢ (𝑜 = ⚬ → ((𝑥𝑜𝑦)𝑜𝑧) = ((𝑥 ⚬ 𝑦) ⚬ 𝑧)) |
23 | | eqidd 2171 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → 𝑥 = 𝑥) |
24 | | oveq 5859 |
. . . . . . . . . 10
⊢ (𝑜 = ⚬ → (𝑦𝑜𝑧) = (𝑦 ⚬ 𝑧)) |
25 | 19, 23, 24 | oveq123d 5874 |
. . . . . . . . 9
⊢ (𝑜 = ⚬ → (𝑥𝑜(𝑦𝑜𝑧)) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) |
26 | 22, 25 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑜 = ⚬ → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
27 | 26 | adantl 275 |
. . . . . . 7
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) → (((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
28 | 18, 27 | raleqbidv 2677 |
. . . . . 6
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
29 | 18, 28 | raleqbidv 2677 |
. . . . 5
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
30 | 18, 29 | raleqbidv 2677 |
. . . 4
⊢ (((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) ∧ 𝑜 = ⚬ ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
31 | 13, 17, 30 | sbcied2 2992 |
. . 3
⊢ ((𝑔 = 𝑀 ∧ 𝑏 = 𝐵) → ([(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
32 | 6, 9, 31 | sbcied2 2992 |
. 2
⊢ (𝑔 = 𝑀 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |
33 | | df-sgrp 12643 |
. 2
⊢ Smgrp =
{𝑔 ∈ Mgm ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} |
34 | 32, 33 | elrab2 2889 |
1
⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) |