Step | Hyp | Ref
| Expression |
1 | | grpinvval.n |
. 2
⊢ 𝑁 = (invg‘𝐺) |
2 | | fveq2 6717 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
3 | | grpinvval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
4 | 2, 3 | eqtr4di 2796 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
5 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺)) |
6 | | grpinvval.p |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
7 | 5, 6 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + ) |
8 | 7 | oveqd 7230 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑦(+g‘𝑔)𝑥) = (𝑦 + 𝑥)) |
9 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = (0g‘𝐺)) |
10 | | grpinvval.o |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
11 | 9, 10 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = 0 ) |
12 | 8, 11 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑦(+g‘𝑔)𝑥) = (0g‘𝑔) ↔ (𝑦 + 𝑥) = 0 )) |
13 | 4, 12 | riotaeqbidv 7173 |
. . . . 5
⊢ (𝑔 = 𝐺 → (℩𝑦 ∈ (Base‘𝑔)(𝑦(+g‘𝑔)𝑥) = (0g‘𝑔)) = (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) |
14 | 4, 13 | mpteq12dv 5140 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑦 ∈ (Base‘𝑔)(𝑦(+g‘𝑔)𝑥) = (0g‘𝑔))) = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
15 | | df-minusg 18369 |
. . . 4
⊢
invg = (𝑔
∈ V ↦ (𝑥 ∈
(Base‘𝑔) ↦
(℩𝑦 ∈
(Base‘𝑔)(𝑦(+g‘𝑔)𝑥) = (0g‘𝑔)))) |
16 | 3 | fvexi 6731 |
. . . . 5
⊢ 𝐵 ∈ V |
17 | | p0ex 5277 |
. . . . . 6
⊢ {∅}
∈ V |
18 | 17, 16 | unex 7531 |
. . . . 5
⊢
({∅} ∪ 𝐵)
∈ V |
19 | | ssun2 4087 |
. . . . . . . 8
⊢ 𝐵 ⊆ ({∅} ∪ 𝐵) |
20 | | riotacl 7188 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈ 𝐵) |
21 | 19, 20 | sseldi 3899 |
. . . . . . 7
⊢
(∃!𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵)) |
22 | | ssun1 4086 |
. . . . . . . 8
⊢ {∅}
⊆ ({∅} ∪ 𝐵) |
23 | | riotaund 7210 |
. . . . . . . . 9
⊢ (¬
∃!𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) =
∅) |
24 | | riotaex 7174 |
. . . . . . . . . 10
⊢
(℩𝑦
∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈
V |
25 | 24 | elsn 4556 |
. . . . . . . . 9
⊢
((℩𝑦
∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈ {∅} ↔
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) =
∅) |
26 | 23, 25 | sylibr 237 |
. . . . . . . 8
⊢ (¬
∃!𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈
{∅}) |
27 | 22, 26 | sseldi 3899 |
. . . . . . 7
⊢ (¬
∃!𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 →
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵)) |
28 | 21, 27 | pm2.61i 185 |
. . . . . 6
⊢
(℩𝑦
∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵) |
29 | 28 | rgenw 3073 |
. . . . 5
⊢
∀𝑥 ∈
𝐵 (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ) ∈ ({∅} ∪
𝐵) |
30 | 16, 18, 29 | mptexw 7726 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) ∈
V |
31 | 14, 15, 30 | fvmpt 6818 |
. . 3
⊢ (𝐺 ∈ V →
(invg‘𝐺) =
(𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
32 | | fvprc 6709 |
. . . . 5
⊢ (¬
𝐺 ∈ V →
(invg‘𝐺) =
∅) |
33 | | mpt0 6520 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 )) =
∅ |
34 | 32, 33 | eqtr4di 2796 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(invg‘𝐺) =
(𝑥 ∈ ∅ ↦
(℩𝑦 ∈
𝐵 (𝑦 + 𝑥) = 0 ))) |
35 | | fvprc 6709 |
. . . . . 6
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
36 | 3, 35 | syl5eq 2790 |
. . . . 5
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
37 | 36 | mpteq1d 5144 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) = (𝑥 ∈ ∅ ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
38 | 34, 37 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐺 ∈ V →
(invg‘𝐺) =
(𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))) |
39 | 31, 38 | pm2.61i 185 |
. 2
⊢
(invg‘𝐺) = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) |
40 | 1, 39 | eqtri 2765 |
1
⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) |