Step | Hyp | Ref
| Expression |
1 | | eldprdi.w |
. . . . 5
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
2 | | eldprdi.1 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
3 | | eldprdi.2 |
. . . . 5
⊢ (𝜑 → dom 𝑆 = 𝐼) |
4 | | eldprdi.3 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
5 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 2, 3, 4, 5 | dprdff 18234 |
. . . 4
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
7 | | ffn 5958 |
. . . 4
⊢ (𝐹:𝐼⟶(Base‘𝐺) → 𝐹 Fn 𝐼) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐼) |
9 | | dprdf11.4 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
10 | 1, 2, 3, 9, 5 | dprdff 18234 |
. . . 4
⊢ (𝜑 → 𝐻:𝐼⟶(Base‘𝐺)) |
11 | | ffn 5958 |
. . . 4
⊢ (𝐻:𝐼⟶(Base‘𝐺) → 𝐻 Fn 𝐼) |
12 | 10, 11 | syl 17 |
. . 3
⊢ (𝜑 → 𝐻 Fn 𝐼) |
13 | | eqfnfv 6219 |
. . 3
⊢ ((𝐹 Fn 𝐼 ∧ 𝐻 Fn 𝐼) → (𝐹 = 𝐻 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) = (𝐻‘𝑥))) |
14 | 8, 12, 13 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐹 = 𝐻 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) = (𝐻‘𝑥))) |
15 | | eldprdi.0 |
. . . 4
⊢ 0 =
(0g‘𝐺) |
16 | | eqid 2610 |
. . . . . 6
⊢
(-g‘𝐺) = (-g‘𝐺) |
17 | 15, 1, 2, 3, 4, 9, 16 | dprdfsub 18243 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∘𝑓
(-g‘𝐺)𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘𝑓
(-g‘𝐺)𝐻)) = ((𝐺 Σg 𝐹)(-g‘𝐺)(𝐺 Σg 𝐻)))) |
18 | 17 | simpld 474 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓
(-g‘𝐺)𝐻) ∈ 𝑊) |
19 | 15, 1, 2, 3, 18 | dprdfeq0 18244 |
. . 3
⊢ (𝜑 → ((𝐺 Σg (𝐹 ∘𝑓
(-g‘𝐺)𝐻)) = 0 ↔ (𝐹 ∘𝑓
(-g‘𝐺)𝐻) = (𝑥 ∈ 𝐼 ↦ 0 ))) |
20 | 17 | simprd 478 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
(-g‘𝐺)𝐻)) = ((𝐺 Σg 𝐹)(-g‘𝐺)(𝐺 Σg 𝐻))) |
21 | 20 | eqeq1d 2612 |
. . 3
⊢ (𝜑 → ((𝐺 Σg (𝐹 ∘𝑓
(-g‘𝐺)𝐻)) = 0 ↔ ((𝐺 Σg 𝐹)(-g‘𝐺)(𝐺 Σg 𝐻)) = 0 )) |
22 | 2, 3 | dprddomcld 18223 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
23 | | fvex 6113 |
. . . . . . 7
⊢ (𝐹‘𝑥) ∈ V |
24 | 23 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ V) |
25 | | fvex 6113 |
. . . . . . 7
⊢ (𝐻‘𝑥) ∈ V |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐻‘𝑥) ∈ V) |
27 | 6 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
28 | 10 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐼 ↦ (𝐻‘𝑥))) |
29 | 22, 24, 26, 27, 28 | offval2 6812 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘𝑓
(-g‘𝐺)𝐻) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)))) |
30 | 29 | eqeq1d 2612 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘𝑓
(-g‘𝐺)𝐻) = (𝑥 ∈ 𝐼 ↦ 0 ) ↔ (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥))) = (𝑥 ∈ 𝐼 ↦ 0 ))) |
31 | | ovex 6577 |
. . . . . . 7
⊢ ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) ∈ V |
32 | 31 | rgenw 2908 |
. . . . . 6
⊢
∀𝑥 ∈
𝐼 ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) ∈ V |
33 | | mpteqb 6207 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐼 ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) ∈ V → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥))) = (𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀𝑥 ∈ 𝐼 ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) = 0 )) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥))) = (𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀𝑥 ∈ 𝐼 ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) = 0 ) |
35 | | dprdgrp 18227 |
. . . . . . . . 9
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
36 | 2, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Grp) |
37 | 36 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ Grp) |
38 | 6 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (Base‘𝐺)) |
39 | 10 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐻‘𝑥) ∈ (Base‘𝐺)) |
40 | 5, 15, 16 | grpsubeq0 17324 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝐹‘𝑥) ∈ (Base‘𝐺) ∧ (𝐻‘𝑥) ∈ (Base‘𝐺)) → (((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) = 0 ↔ (𝐹‘𝑥) = (𝐻‘𝑥))) |
41 | 37, 38, 39, 40 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) = 0 ↔ (𝐹‘𝑥) = (𝐻‘𝑥))) |
42 | 41 | ralbidva 2968 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐼 ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥)) = 0 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) = (𝐻‘𝑥))) |
43 | 34, 42 | syl5bb 271 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(-g‘𝐺)(𝐻‘𝑥))) = (𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) = (𝐻‘𝑥))) |
44 | 30, 43 | bitrd 267 |
. . 3
⊢ (𝜑 → ((𝐹 ∘𝑓
(-g‘𝐺)𝐻) = (𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) = (𝐻‘𝑥))) |
45 | 19, 21, 44 | 3bitr3d 297 |
. 2
⊢ (𝜑 → (((𝐺 Σg 𝐹)(-g‘𝐺)(𝐺 Σg 𝐻)) = 0 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) = (𝐻‘𝑥))) |
46 | 5 | dprdssv 18238 |
. . . 4
⊢ (𝐺 DProd 𝑆) ⊆ (Base‘𝐺) |
47 | 15, 1, 2, 3, 4 | eldprdi 18240 |
. . . 4
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd 𝑆)) |
48 | 46, 47 | sseldi 3566 |
. . 3
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (Base‘𝐺)) |
49 | 15, 1, 2, 3, 9 | eldprdi 18240 |
. . . 4
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ (𝐺 DProd 𝑆)) |
50 | 46, 49 | sseldi 3566 |
. . 3
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ (Base‘𝐺)) |
51 | 5, 15, 16 | grpsubeq0 17324 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝐺 Σg
𝐹) ∈ (Base‘𝐺) ∧ (𝐺 Σg 𝐻) ∈ (Base‘𝐺)) → (((𝐺 Σg 𝐹)(-g‘𝐺)(𝐺 Σg 𝐻)) = 0 ↔ (𝐺 Σg 𝐹) = (𝐺 Σg 𝐻))) |
52 | 36, 48, 50, 51 | syl3anc 1318 |
. 2
⊢ (𝜑 → (((𝐺 Σg 𝐹)(-g‘𝐺)(𝐺 Σg 𝐻)) = 0 ↔ (𝐺 Σg 𝐹) = (𝐺 Σg 𝐻))) |
53 | 14, 45, 52 | 3bitr2rd 296 |
1
⊢ (𝜑 → ((𝐺 Σg 𝐹) = (𝐺 Σg 𝐻) ↔ 𝐹 = 𝐻)) |