Step | Hyp | Ref
| Expression |
1 | | fvex 6730 |
. . 3
⊢
(Base‘𝑔)
∈ V |
2 | | fvex 6730 |
. . 3
⊢
(+g‘𝑔) ∈ V |
3 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
4 | | ismnddef.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
5 | 3, 4 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
6 | 5 | eqeq2d 2748 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑏 = (Base‘𝑔) ↔ 𝑏 = 𝐵)) |
7 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺)) |
8 | | ismnddef.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
9 | 7, 8 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + ) |
10 | 9 | eqeq2d 2748 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑝 = (+g‘𝑔) ↔ 𝑝 = + )) |
11 | 6, 10 | anbi12d 634 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝑏 = (Base‘𝑔) ∧ 𝑝 = (+g‘𝑔)) ↔ (𝑏 = 𝐵 ∧ 𝑝 = + ))) |
12 | | simpl 486 |
. . . . 5
⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → 𝑏 = 𝐵) |
13 | | oveq 7219 |
. . . . . . . . 9
⊢ (𝑝 = + → (𝑒𝑝𝑎) = (𝑒 + 𝑎)) |
14 | 13 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑝 = + → ((𝑒𝑝𝑎) = 𝑎 ↔ (𝑒 + 𝑎) = 𝑎)) |
15 | | oveq 7219 |
. . . . . . . . 9
⊢ (𝑝 = + → (𝑎𝑝𝑒) = (𝑎 + 𝑒)) |
16 | 15 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑝 = + → ((𝑎𝑝𝑒) = 𝑎 ↔ (𝑎 + 𝑒) = 𝑎)) |
17 | 14, 16 | anbi12d 634 |
. . . . . . 7
⊢ (𝑝 = + → (((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) |
18 | 17 | adantl 485 |
. . . . . 6
⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → (((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) |
19 | 12, 18 | raleqbidv 3313 |
. . . . 5
⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → (∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) |
20 | 12, 19 | rexeqbidv 3314 |
. . . 4
⊢ ((𝑏 = 𝐵 ∧ 𝑝 = + ) → (∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) |
21 | 11, 20 | syl6bi 256 |
. . 3
⊢ (𝑔 = 𝐺 → ((𝑏 = (Base‘𝑔) ∧ 𝑝 = (+g‘𝑔)) → (∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))) |
22 | 1, 2, 21 | sbc2iedv 3780 |
. 2
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎) ↔ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) |
23 | | df-mnd 18174 |
. 2
⊢ Mnd =
{𝑔 ∈ Smgrp ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑎 ∈ 𝑏 ((𝑒𝑝𝑎) = 𝑎 ∧ (𝑎𝑝𝑒) = 𝑎)} |
24 | 22, 23 | elrab2 3605 |
1
⊢ (𝐺 ∈ Mnd ↔ (𝐺 ∈ Smgrp ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) |