Step | Hyp | Ref
| Expression |
1 | | eldprdi.1 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
2 | | eldprdi.2 |
. . . . 5
⊢ (𝜑 → dom 𝑆 = 𝐼) |
3 | 1, 2 | dprddomcld 18798 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
4 | | eldprdi.w |
. . . . 5
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
5 | | eldprdi.3 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
6 | 4, 1, 2, 5 | dprdfcl 18810 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (𝑆‘𝑥)) |
7 | | dprdfadd.4 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
8 | 4, 1, 2, 7 | dprdfcl 18810 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐻‘𝑥) ∈ (𝑆‘𝑥)) |
9 | | eqid 2778 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
10 | 4, 1, 2, 5, 9 | dprdff 18809 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
11 | 10 | feqmptd 6511 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
12 | 4, 1, 2, 7, 9 | dprdff 18809 |
. . . . 5
⊢ (𝜑 → 𝐻:𝐼⟶(Base‘𝐺)) |
13 | 12 | feqmptd 6511 |
. . . 4
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐼 ↦ (𝐻‘𝑥))) |
14 | 3, 6, 8, 11, 13 | offval2 7193 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥)))) |
15 | 1, 2 | dprdf2 18804 |
. . . . . 6
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
16 | 15 | ffvelrnda 6625 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
17 | | dprdfadd.b |
. . . . . 6
⊢ + =
(+g‘𝐺) |
18 | 17 | subgcl 17999 |
. . . . 5
⊢ (((𝑆‘𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐹‘𝑥) ∈ (𝑆‘𝑥) ∧ (𝐻‘𝑥) ∈ (𝑆‘𝑥)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) ∈ (𝑆‘𝑥)) |
19 | 16, 6, 8, 18 | syl3anc 1439 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥) + (𝐻‘𝑥)) ∈ (𝑆‘𝑥)) |
20 | 4, 1, 2, 5 | dprdffsupp 18811 |
. . . . . . 7
⊢ (𝜑 → 𝐹 finSupp 0 ) |
21 | 4, 1, 2, 7 | dprdffsupp 18811 |
. . . . . . 7
⊢ (𝜑 → 𝐻 finSupp 0 ) |
22 | 20, 21 | fsuppunfi 8585 |
. . . . . 6
⊢ (𝜑 → ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) ∈
Fin) |
23 | | ssun1 3999 |
. . . . . . . . . . 11
⊢ (𝐹 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))) |
25 | | eldprdi.0 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐺) |
26 | 25 | fvexi 6462 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ V) |
28 | 10, 24, 3, 27 | suppssr 7610 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → (𝐹‘𝑥) = 0 ) |
29 | | ssun2 4000 |
. . . . . . . . . . 11
⊢ (𝐻 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))) |
31 | 12, 30, 3, 27 | suppssr 7610 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → (𝐻‘𝑥) = 0 ) |
32 | 28, 31 | oveq12d 6942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 )) |
33 | | dprdgrp 18802 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
34 | 1, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ Grp) |
35 | 9, 25 | grpidcl 17848 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (Base‘𝐺)) |
37 | 9, 17, 25 | grplid 17850 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 0 ∈
(Base‘𝐺)) → (
0 + 0 ) = 0
) |
38 | 34, 36, 37 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
39 | 38 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ( 0 + 0 ) = 0
) |
40 | 32, 39 | eqtrd 2814 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = 0 ) |
41 | 40, 3 | suppss2 7613 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))) |
42 | 22, 41 | ssfid 8473 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ∈
Fin) |
43 | | funmpt 6175 |
. . . . . . 7
⊢ Fun
(𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) |
44 | 43 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Fun (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥)))) |
45 | 3 | mptexd 6761 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∈ V) |
46 | | funisfsupp 8570 |
. . . . . 6
⊢ ((Fun
(𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∧ (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ∈
Fin)) |
47 | 44, 45, 27, 46 | syl3anc 1439 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ∈
Fin)) |
48 | 42, 47 | mpbird 249 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) finSupp 0 ) |
49 | 4, 1, 2, 19, 48 | dprdwd 18808 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∈ 𝑊) |
50 | 14, 49 | eqeltrd 2859 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐻) ∈ 𝑊) |
51 | | eqid 2778 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
52 | | grpmnd 17827 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
53 | 34, 52 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
54 | | eqid 2778 |
. . 3
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐹 ∪ 𝐻) supp 0 ) |
55 | 4, 1, 2, 5, 51 | dprdfcntz 18812 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
56 | 4, 1, 2, 7, 51 | dprdfcntz 18812 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ ((Cntz‘𝐺)‘ran 𝐻)) |
57 | 4, 1, 2, 50, 51 | dprdfcntz 18812 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ ((Cntz‘𝐺)‘ran (𝐹 ∘𝑓 + 𝐻))) |
58 | 53 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝐺 ∈ Mnd) |
59 | | vex 3401 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝑥 ∈ V) |
61 | | eldifi 3955 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝐼 ∖ 𝑥) → 𝑘 ∈ 𝐼) |
62 | 61 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥)) → 𝑘 ∈ 𝐼) |
63 | | ffvelrn 6623 |
. . . . . . . . . 10
⊢ ((𝐹:𝐼⟶(Base‘𝐺) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (Base‘𝐺)) |
64 | 10, 62, 63 | syl2an 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (Base‘𝐺)) |
65 | 64 | snssd 4573 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐹‘𝑘)} ⊆ (Base‘𝐺)) |
66 | 9, 51 | cntzsubm 18162 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ {(𝐹‘𝑘)} ⊆ (Base‘𝐺)) → ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ∈ (SubMnd‘𝐺)) |
67 | 58, 65, 66 | syl2anc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ∈ (SubMnd‘𝐺)) |
68 | 12 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝐻:𝐼⟶(Base‘𝐺)) |
69 | 68 | ffnd 6294 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝐻 Fn 𝐼) |
70 | | simprl 761 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝑥 ⊆ 𝐼) |
71 | | fnssres 6252 |
. . . . . . . . 9
⊢ ((𝐻 Fn 𝐼 ∧ 𝑥 ⊆ 𝐼) → (𝐻 ↾ 𝑥) Fn 𝑥) |
72 | 69, 70, 71 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥) Fn 𝑥) |
73 | | fvres 6467 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 → ((𝐻 ↾ 𝑥)‘𝑦) = (𝐻‘𝑦)) |
74 | 73 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ((𝐻 ↾ 𝑥)‘𝑦) = (𝐻‘𝑦)) |
75 | 1 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝐺dom DProd 𝑆) |
76 | 2 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → dom 𝑆 = 𝐼) |
77 | 75, 76 | dprdf2 18804 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
78 | 62 | ad2antlr 717 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑘 ∈ 𝐼) |
79 | 77, 78 | ffvelrnd 6626 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝑆‘𝑘) ∈ (SubGrp‘𝐺)) |
80 | 9 | subgss 17990 |
. . . . . . . . . . . . 13
⊢ ((𝑆‘𝑘) ∈ (SubGrp‘𝐺) → (𝑆‘𝑘) ⊆ (Base‘𝐺)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝑆‘𝑘) ⊆ (Base‘𝐺)) |
82 | 5 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝐹 ∈ 𝑊) |
83 | 4, 75, 76, 82 | dprdfcl 18810 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) |
84 | 78, 83 | mpdan 677 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) |
85 | 84 | snssd 4573 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → {(𝐹‘𝑘)} ⊆ (𝑆‘𝑘)) |
86 | 9, 51 | cntz2ss 18159 |
. . . . . . . . . . . 12
⊢ (((𝑆‘𝑘) ⊆ (Base‘𝐺) ∧ {(𝐹‘𝑘)} ⊆ (𝑆‘𝑘)) → ((Cntz‘𝐺)‘(𝑆‘𝑘)) ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
87 | 81, 85, 86 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ((Cntz‘𝐺)‘(𝑆‘𝑘)) ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
88 | 70 | sselda 3821 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐼) |
89 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
90 | | simplrr 768 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑘 ∈ (𝐼 ∖ 𝑥)) |
91 | 90 | eldifbd 3805 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ¬ 𝑘 ∈ 𝑥) |
92 | | nelne2 3068 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑥 ∧ ¬ 𝑘 ∈ 𝑥) → 𝑦 ≠ 𝑘) |
93 | 89, 91, 92 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ≠ 𝑘) |
94 | 75, 76, 88, 78, 93, 51 | dprdcntz 18805 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝑆‘𝑦) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑘))) |
95 | 7 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝐻 ∈ 𝑊) |
96 | 4, 75, 76, 95 | dprdfcl 18810 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ 𝐼) → (𝐻‘𝑦) ∈ (𝑆‘𝑦)) |
97 | 88, 96 | mpdan 677 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ (𝑆‘𝑦)) |
98 | 94, 97 | sseldd 3822 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ ((Cntz‘𝐺)‘(𝑆‘𝑘))) |
99 | 87, 98 | sseldd 3822 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
100 | 74, 99 | eqeltrd 2859 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ((𝐻 ↾ 𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
101 | 100 | ralrimiva 3148 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ∀𝑦 ∈ 𝑥 ((𝐻 ↾ 𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
102 | | ffnfv 6654 |
. . . . . . . 8
⊢ ((𝐻 ↾ 𝑥):𝑥⟶((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ↔ ((𝐻 ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝐻 ↾ 𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)}))) |
103 | 72, 101, 102 | sylanbrc 578 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
104 | | resss 5673 |
. . . . . . . . . 10
⊢ (𝐻 ↾ 𝑥) ⊆ 𝐻 |
105 | 104 | rnssi 5602 |
. . . . . . . . 9
⊢ ran
(𝐻 ↾ 𝑥) ⊆ ran 𝐻 |
106 | 51 | cntzidss 18164 |
. . . . . . . . 9
⊢ ((ran
𝐻 ⊆
((Cntz‘𝐺)‘ran
𝐻) ∧ ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) → ran (𝐻 ↾ 𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻 ↾ 𝑥))) |
107 | 56, 105, 106 | sylancl 580 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐻 ↾ 𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻 ↾ 𝑥))) |
108 | 107 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ran (𝐻 ↾ 𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻 ↾ 𝑥))) |
109 | 21, 27 | fsuppres 8590 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ↾ 𝑥) finSupp 0 ) |
110 | 109 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥) finSupp 0 ) |
111 | 25, 51, 58, 60, 67, 103, 108, 110 | gsumzsubmcl 18715 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
112 | 111 | snssd 4573 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
113 | 68, 70 | fssresd 6323 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶(Base‘𝐺)) |
114 | 9, 25, 51, 58, 60, 113, 108, 110 | gsumzcl 18709 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ (Base‘𝐺)) |
115 | 114 | snssd 4573 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ (Base‘𝐺)) |
116 | 9, 51 | cntzrec 18160 |
. . . . . 6
⊢ (({(𝐺 Σg
(𝐻 ↾ 𝑥))} ⊆ (Base‘𝐺) ∧ {(𝐹‘𝑘)} ⊆ (Base‘𝐺)) → ({(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ↔ {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
117 | 115, 65, 116 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ({(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ↔ {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
118 | 112, 117 | mpbid 224 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
119 | | fvex 6461 |
. . . . 5
⊢ (𝐹‘𝑘) ∈ V |
120 | 119 | snss 4549 |
. . . 4
⊢ ((𝐹‘𝑘) ∈ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
121 | 118, 120 | sylibr 226 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐹‘𝑘) ∈ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
122 | 9, 25, 17, 51, 53, 3, 20, 21, 54, 10, 12, 55, 56, 57, 121 | gsumzaddlem 18718 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
123 | 50, 122 | jca 507 |
1
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |