| Step | Hyp | Ref
| Expression |
| 1 | | grpinvval.n |
. 2
⊢ 𝑁 = (invg‘𝐺) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
| 3 | | grpinvval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
| 5 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺)) |
| 6 | | grpinvval.p |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + ) |
| 8 | 7 | oveqd 7448 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑦(+g‘𝑔)𝑥) = (𝑦 + 𝑥)) |
| 9 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = (0g‘𝐺)) |
| 10 | | grpinvval.o |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = 0 ) |
| 12 | 8, 11 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑦(+g‘𝑔)𝑥) = (0g‘𝑔) ↔ (𝑦 + 𝑥) = 0 )) |
| 13 | 4, 12 | riotaeqbidv 7391 |
. . . . 5
⊢ (𝑔 = 𝐺 → (℩𝑦 ∈ (Base‘𝑔)(𝑦(+g‘𝑔)𝑥) = (0g‘𝑔)) = (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) |
| 14 | 4, 13 | mpteq12dv 5233 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑦 ∈ (Base‘𝑔)(𝑦(+g‘𝑔)𝑥) = (0g‘𝑔))) = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
| 15 | | df-minusg 18955 |
. . . 4
⊢
invg = (𝑔
∈ V ↦ (𝑥 ∈
(Base‘𝑔) ↦
(℩𝑦 ∈
(Base‘𝑔)(𝑦(+g‘𝑔)𝑥) = (0g‘𝑔)))) |
| 16 | 3 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 17 | | p0ex 5384 |
. . . . . 6
⊢ {∅}
∈ V |
| 18 | 17, 16 | unex 7764 |
. . . . 5
⊢
({∅} ∪ 𝐵)
∈ V |
| 19 | | ssun2 4179 |
. . . . . . . 8
⊢ 𝐵 ⊆ ({∅} ∪ 𝐵) |
| 20 | | riotacl 7405 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈ 𝐵) |
| 21 | 19, 20 | sselid 3981 |
. . . . . . 7
⊢
(∃!𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵)) |
| 22 | | ssun1 4178 |
. . . . . . . 8
⊢ {∅}
⊆ ({∅} ∪ 𝐵) |
| 23 | | riotaund 7427 |
. . . . . . . . 9
⊢ (¬
∃!𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) =
∅) |
| 24 | | riotaex 7392 |
. . . . . . . . . 10
⊢
(℩𝑦
∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈
V |
| 25 | 24 | elsn 4641 |
. . . . . . . . 9
⊢
((℩𝑦
∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈ {∅} ↔
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) =
∅) |
| 26 | 23, 25 | sylibr 234 |
. . . . . . . 8
⊢ (¬
∃!𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈
{∅}) |
| 27 | 22, 26 | sselid 3981 |
. . . . . . 7
⊢ (¬
∃!𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵)) |
| 28 | 21, 27 | pm2.61i 182 |
. . . . . 6
⊢
(℩𝑦
∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵) |
| 29 | 28 | rgenw 3065 |
. . . . 5
⊢
∀𝑥 ∈
𝐵 (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵) |
| 30 | 16, 18, 29 | mptexw 7977 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) ∈
V |
| 31 | 14, 15, 30 | fvmpt 7016 |
. . 3
⊢ (𝐺 ∈ V →
(invg‘𝐺) =
(𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
| 32 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝐺 ∈ V →
(invg‘𝐺) =
∅) |
| 33 | | mpt0 6710 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 )) =
∅ |
| 34 | 32, 33 | eqtr4di 2795 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(invg‘𝐺) =
(𝑥 ∈ ∅ ↦
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ))) |
| 35 | | fvprc 6898 |
. . . . . 6
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
| 36 | 3, 35 | eqtrid 2789 |
. . . . 5
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
| 37 | 36 | mpteq1d 5237 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) = (𝑥 ∈ ∅ ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
| 38 | 34, 37 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐺 ∈ V →
(invg‘𝐺) =
(𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
| 39 | 31, 38 | pm2.61i 182 |
. 2
⊢
(invg‘𝐺) = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) |
| 40 | 1, 39 | eqtri 2765 |
1
⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) |