Step | Hyp | Ref
| Expression |
1 | | dprdlub.1 |
. . 3
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
2 | | dprdlub.2 |
. . 3
⊢ (𝜑 → dom 𝑆 = 𝐼) |
3 | | eqid 2610 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
4 | | eqid 2610 |
. . . 4
⊢ {ℎ ∈ X𝑖 ∈
𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} |
5 | 3, 4 | dprdval 18225 |
. . 3
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → (𝐺 DProd 𝑆) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓))) |
6 | 1, 2, 5 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑆) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓))) |
7 | | eqid 2610 |
. . . . 5
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
8 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝐺dom DProd 𝑆) |
9 | | dprdgrp 18227 |
. . . . . 6
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
10 | | grpmnd 17252 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
11 | 8, 9, 10 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝐺 ∈ Mnd) |
12 | 1, 2 | dprddomcld 18223 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ V) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝐼 ∈ V) |
14 | | dprdlub.3 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑇 ∈ (SubGrp‘𝐺)) |
16 | | subgsubm 17439 |
. . . . . 6
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝑇 ∈ (SubMnd‘𝐺)) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑇 ∈ (SubMnd‘𝐺)) |
18 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → dom 𝑆 = 𝐼) |
19 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) |
20 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
21 | 4, 8, 18, 19, 20 | dprdff 18234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑓:𝐼⟶(Base‘𝐺)) |
22 | | ffn 5958 |
. . . . . . 7
⊢ (𝑓:𝐼⟶(Base‘𝐺) → 𝑓 Fn 𝐼) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑓 Fn 𝐼) |
24 | | dprdlub.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ 𝑇) |
25 | 24 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ 𝑇) |
26 | 4, 8, 18, 19 | dprdfcl 18235 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) ∧ 𝑘 ∈ 𝐼) → (𝑓‘𝑘) ∈ (𝑆‘𝑘)) |
27 | 25, 26 | sseldd 3569 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) ∧ 𝑘 ∈ 𝐼) → (𝑓‘𝑘) ∈ 𝑇) |
28 | 27 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → ∀𝑘 ∈ 𝐼 (𝑓‘𝑘) ∈ 𝑇) |
29 | | ffnfv 6295 |
. . . . . 6
⊢ (𝑓:𝐼⟶𝑇 ↔ (𝑓 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑓‘𝑘) ∈ 𝑇)) |
30 | 23, 28, 29 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑓:𝐼⟶𝑇) |
31 | 4, 8, 18, 19, 7 | dprdfcntz 18237 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → ran 𝑓 ⊆ ((Cntz‘𝐺)‘ran 𝑓)) |
32 | 4, 8, 18, 19 | dprdffsupp 18236 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → 𝑓 finSupp (0g‘𝐺)) |
33 | 3, 7, 11, 13, 17, 30, 31, 32 | gsumzsubmcl 18141 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}) → (𝐺 Σg 𝑓) ∈ 𝑇) |
34 | | eqid 2610 |
. . . 4
⊢ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓)) = (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓)) |
35 | 33, 34 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓)):{ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}⟶𝑇) |
36 | | frn 5966 |
. . 3
⊢ ((𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓)):{ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)}⟶𝑇 → ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓)) ⊆ 𝑇) |
37 | 35, 36 | syl 17 |
. 2
⊢ (𝜑 → ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐺)} ↦ (𝐺 Σg 𝑓)) ⊆ 𝑇) |
38 | 6, 37 | eqsstrd 3602 |
1
⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ 𝑇) |