Step | Hyp | Ref
| Expression |
1 | | grpsubval.m |
. . 3
⊢ − =
(-g‘𝐺) |
2 | | fveq2 6545 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
3 | | grpsubval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
4 | 2, 3 | syl6eqr 2851 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
5 | | fveq2 6545 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺)) |
6 | | grpsubval.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
7 | 5, 6 | syl6eqr 2851 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + ) |
8 | | eqidd 2798 |
. . . . . 6
⊢ (𝑔 = 𝐺 → 𝑥 = 𝑥) |
9 | | fveq2 6545 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (invg‘𝑔) = (invg‘𝐺)) |
10 | | grpsubval.i |
. . . . . . . 8
⊢ 𝐼 = (invg‘𝐺) |
11 | 9, 10 | syl6eqr 2851 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (invg‘𝑔) = 𝐼) |
12 | 11 | fveq1d 6547 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((invg‘𝑔)‘𝑦) = (𝐼‘𝑦)) |
13 | 7, 8, 12 | oveq123d 7044 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)) = (𝑥 + (𝐼‘𝑦))) |
14 | 4, 4, 13 | mpoeq123dv 7094 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))) |
15 | | df-sbg 17870 |
. . . 4
⊢
-g = (𝑔
∈ V ↦ (𝑥 ∈
(Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))) |
16 | 3 | fvexi 6559 |
. . . . 5
⊢ 𝐵 ∈ V |
17 | 6 | fvexi 6559 |
. . . . . . 7
⊢ + ∈
V |
18 | 17 | rnex 7480 |
. . . . . 6
⊢ ran + ∈
V |
19 | | p0ex 5182 |
. . . . . 6
⊢ {∅}
∈ V |
20 | 18, 19 | unex 7333 |
. . . . 5
⊢ (ran
+ ∪
{∅}) ∈ V |
21 | | df-ov 7026 |
. . . . . . 7
⊢ (𝑥 + (𝐼‘𝑦)) = ( + ‘〈𝑥, (𝐼‘𝑦)〉) |
22 | | fvrn0 6573 |
. . . . . . 7
⊢ ( +
‘〈𝑥, (𝐼‘𝑦)〉) ∈ (ran + ∪
{∅}) |
23 | 21, 22 | eqeltri 2881 |
. . . . . 6
⊢ (𝑥 + (𝐼‘𝑦)) ∈ (ran + ∪
{∅}) |
24 | 23 | rgen2w 3120 |
. . . . 5
⊢
∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + (𝐼‘𝑦)) ∈ (ran + ∪
{∅}) |
25 | 16, 16, 20, 24 | mpoexw 7639 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) ∈ V |
26 | 14, 15, 25 | fvmpt 6642 |
. . 3
⊢ (𝐺 ∈ V →
(-g‘𝐺) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))) |
27 | 1, 26 | syl5eq 2845 |
. 2
⊢ (𝐺 ∈ V → − =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))) |
28 | | fvprc 6538 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(-g‘𝐺) =
∅) |
29 | 1, 28 | syl5eq 2845 |
. . 3
⊢ (¬
𝐺 ∈ V → − =
∅) |
30 | | fvprc 6538 |
. . . . . 6
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
31 | 3, 30 | syl5eq 2845 |
. . . . 5
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
32 | | mpoeq12 7092 |
. . . . 5
⊢ ((𝐵 = ∅ ∧ 𝐵 = ∅) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + (𝐼‘𝑦)))) |
33 | 31, 31, 32 | syl2anc 584 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + (𝐼‘𝑦)))) |
34 | | mpo0 7102 |
. . . 4
⊢ (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 + (𝐼‘𝑦))) = ∅ |
35 | 33, 34 | syl6eq 2849 |
. . 3
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) = ∅) |
36 | 29, 35 | eqtr4d 2836 |
. 2
⊢ (¬
𝐺 ∈ V → − =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))) |
37 | 27, 36 | pm2.61i 183 |
1
⊢ − =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) |