Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
2 | 1 | dprdssv 18415 |
. . 3
⊢ (𝐺 DProd 𝑆) ⊆ (Base‘𝐺) |
3 | 2 | a1i 11 |
. 2
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ⊆ (Base‘𝐺)) |
4 | | eqid 2622 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | | eqid 2622 |
. . . 4
⊢ {ℎ ∈ X𝑖 ∈
dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} = {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} |
6 | | id 22 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → 𝐺dom DProd 𝑆) |
7 | | eqidd 2623 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → dom 𝑆 = dom 𝑆) |
8 | | fvex 6201 |
. . . . . 6
⊢
(0g‘𝐺) ∈ V |
9 | | fnconstg 6093 |
. . . . . 6
⊢
((0g‘𝐺) ∈ V → (dom 𝑆 × {(0g‘𝐺)}) Fn dom 𝑆) |
10 | 8, 9 | mp1i 13 |
. . . . 5
⊢ (𝐺dom DProd 𝑆 → (dom 𝑆 × {(0g‘𝐺)}) Fn dom 𝑆) |
11 | 8 | fvconst2 6469 |
. . . . . . . 8
⊢ (𝑘 ∈ dom 𝑆 → ((dom 𝑆 × {(0g‘𝐺)})‘𝑘) = (0g‘𝐺)) |
12 | 11 | adantl 482 |
. . . . . . 7
⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → ((dom 𝑆 × {(0g‘𝐺)})‘𝑘) = (0g‘𝐺)) |
13 | | dprdf 18405 |
. . . . . . . . 9
⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) |
14 | 13 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → (𝑆‘𝑘) ∈ (SubGrp‘𝐺)) |
15 | 4 | subg0cl 17602 |
. . . . . . . 8
⊢ ((𝑆‘𝑘) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑆‘𝑘)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → (0g‘𝐺) ∈ (𝑆‘𝑘)) |
17 | 12, 16 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝐺dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆) → ((dom 𝑆 × {(0g‘𝐺)})‘𝑘) ∈ (𝑆‘𝑘)) |
18 | 17 | ralrimiva 2966 |
. . . . 5
⊢ (𝐺dom DProd 𝑆 → ∀𝑘 ∈ dom 𝑆((dom 𝑆 × {(0g‘𝐺)})‘𝑘) ∈ (𝑆‘𝑘)) |
19 | | df-nel 2898 |
. . . . . . . 8
⊢ (dom
𝑆 ∉ V ↔ ¬
dom 𝑆 ∈
V) |
20 | | dprddomprc 18399 |
. . . . . . . 8
⊢ (dom
𝑆 ∉ V → ¬
𝐺dom DProd 𝑆) |
21 | 19, 20 | sylbir 225 |
. . . . . . 7
⊢ (¬
dom 𝑆 ∈ V → ¬
𝐺dom DProd 𝑆) |
22 | 21 | con4i 113 |
. . . . . 6
⊢ (𝐺dom DProd 𝑆 → dom 𝑆 ∈ V) |
23 | 8 | a1i 11 |
. . . . . 6
⊢ (𝐺dom DProd 𝑆 → (0g‘𝐺) ∈ V) |
24 | 22, 23 | fczfsuppd 8293 |
. . . . 5
⊢ (𝐺dom DProd 𝑆 → (dom 𝑆 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)) |
25 | 5, 6, 7 | dprdw 18409 |
. . . . 5
⊢ (𝐺dom DProd 𝑆 → ((dom 𝑆 × {(0g‘𝐺)}) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↔ ((dom 𝑆 ×
{(0g‘𝐺)})
Fn dom 𝑆 ∧
∀𝑘 ∈ dom 𝑆((dom 𝑆 × {(0g‘𝐺)})‘𝑘) ∈ (𝑆‘𝑘) ∧ (dom 𝑆 × {(0g‘𝐺)}) finSupp
(0g‘𝐺)))) |
26 | 10, 18, 24, 25 | mpbir3and 1245 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → (dom 𝑆 × {(0g‘𝐺)}) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) |
27 | 4, 5, 6, 7, 26 | eldprdi 18417 |
. . 3
⊢ (𝐺dom DProd 𝑆 → (𝐺 Σg (dom 𝑆 ×
{(0g‘𝐺)}))
∈ (𝐺 DProd 𝑆)) |
28 | | ne0i 3921 |
. . 3
⊢ ((𝐺 Σg (dom
𝑆 ×
{(0g‘𝐺)}))
∈ (𝐺 DProd 𝑆) → (𝐺 DProd 𝑆) ≠ ∅) |
29 | 27, 28 | syl 17 |
. 2
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ≠ ∅) |
30 | | eqid 2622 |
. . . . 5
⊢ dom 𝑆 = dom 𝑆 |
31 | 4, 5 | eldprd 18403 |
. . . . . . 7
⊢ (dom
𝑆 = dom 𝑆 → (𝑥 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑥 = (𝐺 Σg 𝑓)))) |
32 | 31 | baibd 948 |
. . . . . 6
⊢ ((dom
𝑆 = dom 𝑆 ∧ 𝐺dom DProd 𝑆) → (𝑥 ∈ (𝐺 DProd 𝑆) ↔ ∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑥 = (𝐺 Σg 𝑓))) |
33 | 4, 5 | eldprd 18403 |
. . . . . . 7
⊢ (dom
𝑆 = dom 𝑆 → (𝑦 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑦 = (𝐺 Σg 𝑔)))) |
34 | 33 | baibd 948 |
. . . . . 6
⊢ ((dom
𝑆 = dom 𝑆 ∧ 𝐺dom DProd 𝑆) → (𝑦 ∈ (𝐺 DProd 𝑆) ↔ ∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑦 = (𝐺 Σg 𝑔))) |
35 | 32, 34 | anbi12d 747 |
. . . . 5
⊢ ((dom
𝑆 = dom 𝑆 ∧ 𝐺dom DProd 𝑆) → ((𝑥 ∈ (𝐺 DProd 𝑆) ∧ 𝑦 ∈ (𝐺 DProd 𝑆)) ↔ (∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑥 = (𝐺 Σg 𝑓) ∧ ∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑦 = (𝐺 Σg 𝑔)))) |
36 | 30, 35 | mpan 706 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → ((𝑥 ∈ (𝐺 DProd 𝑆) ∧ 𝑦 ∈ (𝐺 DProd 𝑆)) ↔ (∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑥 = (𝐺 Σg 𝑓) ∧ ∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑦 = (𝐺 Σg 𝑔)))) |
37 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑓 ∈
{ℎ ∈ X𝑖 ∈
dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} (𝑥 = (𝐺 Σg 𝑓) ∧ 𝑦 = (𝐺 Σg 𝑔)) ↔ (∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑥 = (𝐺 Σg 𝑓) ∧ ∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑦 = (𝐺 Σg 𝑔))) |
38 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → 𝐺dom DProd 𝑆) |
39 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → dom 𝑆 = dom 𝑆) |
40 | | simprl 794 |
. . . . . . . . . 10
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → 𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) |
41 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) |
42 | | eqid 2622 |
. . . . . . . . . 10
⊢
(-g‘𝐺) = (-g‘𝐺) |
43 | 4, 5, 38, 39, 40, 41, 42 | dprdfsub 18420 |
. . . . . . . . 9
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → ((𝑓 ∘𝑓
(-g‘𝐺)𝑔) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ (𝐺 Σg (𝑓 ∘𝑓
(-g‘𝐺)𝑔)) = ((𝐺 Σg 𝑓)(-g‘𝐺)(𝐺 Σg 𝑔)))) |
44 | 43 | simprd 479 |
. . . . . . . 8
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → (𝐺 Σg (𝑓 ∘𝑓
(-g‘𝐺)𝑔)) = ((𝐺 Σg 𝑓)(-g‘𝐺)(𝐺 Σg 𝑔))) |
45 | 43 | simpld 475 |
. . . . . . . . 9
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → (𝑓 ∘𝑓
(-g‘𝐺)𝑔) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) |
46 | 4, 5, 38, 39, 45 | eldprdi 18417 |
. . . . . . . 8
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → (𝐺 Σg (𝑓 ∘𝑓
(-g‘𝐺)𝑔)) ∈ (𝐺 DProd 𝑆)) |
47 | 44, 46 | eqeltrrd 2702 |
. . . . . . 7
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → ((𝐺 Σg 𝑓)(-g‘𝐺)(𝐺 Σg 𝑔)) ∈ (𝐺 DProd 𝑆)) |
48 | | oveq12 6659 |
. . . . . . . 8
⊢ ((𝑥 = (𝐺 Σg 𝑓) ∧ 𝑦 = (𝐺 Σg 𝑔)) → (𝑥(-g‘𝐺)𝑦) = ((𝐺 Σg 𝑓)(-g‘𝐺)(𝐺 Σg 𝑔))) |
49 | 48 | eleq1d 2686 |
. . . . . . 7
⊢ ((𝑥 = (𝐺 Σg 𝑓) ∧ 𝑦 = (𝐺 Σg 𝑔)) → ((𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆) ↔ ((𝐺 Σg 𝑓)(-g‘𝐺)(𝐺 Σg 𝑔)) ∈ (𝐺 DProd 𝑆))) |
50 | 47, 49 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝐺dom DProd 𝑆 ∧ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ∧ 𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)})) → ((𝑥 = (𝐺 Σg 𝑓) ∧ 𝑦 = (𝐺 Σg 𝑔)) → (𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆))) |
51 | 50 | rexlimdvva 3038 |
. . . . 5
⊢ (𝐺dom DProd 𝑆 → (∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} (𝑥 = (𝐺 Σg 𝑓) ∧ 𝑦 = (𝐺 Σg 𝑔)) → (𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆))) |
52 | 37, 51 | syl5bir 233 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → ((∃𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑥 = (𝐺 Σg 𝑓) ∧ ∃𝑔 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑆(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}𝑦 = (𝐺 Σg 𝑔)) → (𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆))) |
53 | 36, 52 | sylbid 230 |
. . 3
⊢ (𝐺dom DProd 𝑆 → ((𝑥 ∈ (𝐺 DProd 𝑆) ∧ 𝑦 ∈ (𝐺 DProd 𝑆)) → (𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆))) |
54 | 53 | ralrimivv 2970 |
. 2
⊢ (𝐺dom DProd 𝑆 → ∀𝑥 ∈ (𝐺 DProd 𝑆)∀𝑦 ∈ (𝐺 DProd 𝑆)(𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆)) |
55 | | dprdgrp 18404 |
. . 3
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
56 | 1, 42 | issubg4 17613 |
. . 3
⊢ (𝐺 ∈ Grp → ((𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺) ↔ ((𝐺 DProd 𝑆) ⊆ (Base‘𝐺) ∧ (𝐺 DProd 𝑆) ≠ ∅ ∧ ∀𝑥 ∈ (𝐺 DProd 𝑆)∀𝑦 ∈ (𝐺 DProd 𝑆)(𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆)))) |
57 | 55, 56 | syl 17 |
. 2
⊢ (𝐺dom DProd 𝑆 → ((𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺) ↔ ((𝐺 DProd 𝑆) ⊆ (Base‘𝐺) ∧ (𝐺 DProd 𝑆) ≠ ∅ ∧ ∀𝑥 ∈ (𝐺 DProd 𝑆)∀𝑦 ∈ (𝐺 DProd 𝑆)(𝑥(-g‘𝐺)𝑦) ∈ (𝐺 DProd 𝑆)))) |
58 | 3, 29, 54, 57 | mpbir3and 1245 |
1
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) |