Step | Hyp | Ref
| Expression |
1 | | eldprdi.1 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
2 | | eldprdi.2 |
. . . . 5
⊢ (𝜑 → dom 𝑆 = 𝐼) |
3 | 1, 2 | dprddomcld 19125 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
4 | | eldprdi.w |
. . . . 5
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
5 | | eldprdi.3 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
6 | 4, 1, 2, 5 | dprdfcl 19137 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (𝑆‘𝑥)) |
7 | | dprdfadd.4 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
8 | 4, 1, 2, 7 | dprdfcl 19137 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐻‘𝑥) ∈ (𝑆‘𝑥)) |
9 | | eqid 2823 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
10 | 4, 1, 2, 5, 9 | dprdff 19136 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
11 | 10 | feqmptd 6735 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
12 | 4, 1, 2, 7, 9 | dprdff 19136 |
. . . . 5
⊢ (𝜑 → 𝐻:𝐼⟶(Base‘𝐺)) |
13 | 12 | feqmptd 6735 |
. . . 4
⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐼 ↦ (𝐻‘𝑥))) |
14 | 3, 6, 8, 11, 13 | offval2 7428 |
. . 3
⊢ (𝜑 → (𝐹 ∘f + 𝐻) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥)))) |
15 | 1, 2 | dprdf2 19131 |
. . . . . 6
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
16 | 15 | ffvelrnda 6853 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
17 | | dprdfadd.b |
. . . . . 6
⊢ + =
(+g‘𝐺) |
18 | 17 | subgcl 18291 |
. . . . 5
⊢ (((𝑆‘𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐹‘𝑥) ∈ (𝑆‘𝑥) ∧ (𝐻‘𝑥) ∈ (𝑆‘𝑥)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) ∈ (𝑆‘𝑥)) |
19 | 16, 6, 8, 18 | syl3anc 1367 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥) + (𝐻‘𝑥)) ∈ (𝑆‘𝑥)) |
20 | 4, 1, 2, 5 | dprdffsupp 19138 |
. . . . . . 7
⊢ (𝜑 → 𝐹 finSupp 0 ) |
21 | 4, 1, 2, 7 | dprdffsupp 19138 |
. . . . . . 7
⊢ (𝜑 → 𝐻 finSupp 0 ) |
22 | 20, 21 | fsuppunfi 8855 |
. . . . . 6
⊢ (𝜑 → ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) ∈
Fin) |
23 | | ssun1 4150 |
. . . . . . . . . . 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 6686 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ V) |
28 | 10, 24, 3, 27 | suppssr 7863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → (𝐹‘𝑥) = 0 ) |
29 | | ssun2 4151 |
. . . . . . . . . . 11
⊢ (𝐻 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))) |
31 | 12, 30, 3, 27 | suppssr 7863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → (𝐻‘𝑥) = 0 ) |
32 | 28, 31 | oveq12d 7176 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 )) |
33 | | dprdgrp 19129 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
34 | 1, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ Grp) |
35 | 9, 25 | grpidcl 18133 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
36 | 9, 17, 25 | grplid 18135 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 0 ∈
(Base‘𝐺)) → (
0 + 0 ) = 0
) |
37 | 34, 35, 36 | syl2anc2 587 |
. . . . . . . . 9
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
38 | 37 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ( 0 + 0 ) = 0
) |
39 | 32, 38 | eqtrd 2858 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = 0 ) |
40 | 39, 3 | suppss2 7866 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))) |
41 | 22, 40 | ssfid 8743 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ∈
Fin) |
42 | | funmpt 6395 |
. . . . . . 7
⊢ Fun
(𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) |
43 | 42 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Fun (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥)))) |
44 | 3 | mptexd 6989 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∈ V) |
45 | | funisfsupp 8840 |
. . . . . 6
⊢ ((Fun
(𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∧ (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ∈
Fin)) |
46 | 43, 44, 27, 45 | syl3anc 1367 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) supp 0 ) ∈
Fin)) |
47 | 41, 46 | mpbird 259 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) finSupp 0 ) |
48 | 4, 1, 2, 19, 47 | dprdwd 19135 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥) + (𝐻‘𝑥))) ∈ 𝑊) |
49 | 14, 48 | eqeltrd 2915 |
. 2
⊢ (𝜑 → (𝐹 ∘f + 𝐻) ∈ 𝑊) |
50 | | eqid 2823 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
51 | | grpmnd 18112 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
52 | 34, 51 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
53 | | eqid 2823 |
. . 3
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐹 ∪ 𝐻) supp 0 ) |
54 | 4, 1, 2, 5, 50 | dprdfcntz 19139 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
55 | 4, 1, 2, 7, 50 | dprdfcntz 19139 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ ((Cntz‘𝐺)‘ran 𝐻)) |
56 | 4, 1, 2, 49, 50 | dprdfcntz 19139 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘f + 𝐻) ⊆ ((Cntz‘𝐺)‘ran (𝐹 ∘f + 𝐻))) |
57 | 52 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝐺 ∈ Mnd) |
58 | | vex 3499 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝑥 ∈ V) |
60 | | eldifi 4105 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝐼 ∖ 𝑥) → 𝑘 ∈ 𝐼) |
61 | 60 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥)) → 𝑘 ∈ 𝐼) |
62 | | ffvelrn 6851 |
. . . . . . . . . 10
⊢ ((𝐹:𝐼⟶(Base‘𝐺) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (Base‘𝐺)) |
63 | 10, 61, 62 | syl2an 597 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (Base‘𝐺)) |
64 | 63 | snssd 4744 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐹‘𝑘)} ⊆ (Base‘𝐺)) |
65 | 9, 50 | cntzsubm 18468 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ {(𝐹‘𝑘)} ⊆ (Base‘𝐺)) → ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ∈ (SubMnd‘𝐺)) |
66 | 57, 64, 65 | syl2anc 586 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ∈ (SubMnd‘𝐺)) |
67 | 12 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝐻:𝐼⟶(Base‘𝐺)) |
68 | 67 | ffnd 6517 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝐻 Fn 𝐼) |
69 | | simprl 769 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → 𝑥 ⊆ 𝐼) |
70 | | fnssres 6472 |
. . . . . . . . 9
⊢ ((𝐻 Fn 𝐼 ∧ 𝑥 ⊆ 𝐼) → (𝐻 ↾ 𝑥) Fn 𝑥) |
71 | 68, 69, 70 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥) Fn 𝑥) |
72 | | fvres 6691 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 → ((𝐻 ↾ 𝑥)‘𝑦) = (𝐻‘𝑦)) |
73 | 72 | adantl 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ((𝐻 ↾ 𝑥)‘𝑦) = (𝐻‘𝑦)) |
74 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝐺dom DProd 𝑆) |
75 | 2 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → dom 𝑆 = 𝐼) |
76 | 74, 75 | dprdf2 19131 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
77 | 61 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑘 ∈ 𝐼) |
78 | 76, 77 | ffvelrnd 6854 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝑆‘𝑘) ∈ (SubGrp‘𝐺)) |
79 | 9 | subgss 18282 |
. . . . . . . . . . . . 13
⊢ ((𝑆‘𝑘) ∈ (SubGrp‘𝐺) → (𝑆‘𝑘) ⊆ (Base‘𝐺)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝑆‘𝑘) ⊆ (Base‘𝐺)) |
81 | 5 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝐹 ∈ 𝑊) |
82 | 4, 74, 75, 81 | dprdfcl 19137 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) |
83 | 77, 82 | mpdan 685 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) |
84 | 83 | snssd 4744 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → {(𝐹‘𝑘)} ⊆ (𝑆‘𝑘)) |
85 | 9, 50 | cntz2ss 18465 |
. . . . . . . . . . . 12
⊢ (((𝑆‘𝑘) ⊆ (Base‘𝐺) ∧ {(𝐹‘𝑘)} ⊆ (𝑆‘𝑘)) → ((Cntz‘𝐺)‘(𝑆‘𝑘)) ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
86 | 80, 84, 85 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ((Cntz‘𝐺)‘(𝑆‘𝑘)) ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
87 | 69 | sselda 3969 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐼) |
88 | | simpr 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
89 | | simplrr 776 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑘 ∈ (𝐼 ∖ 𝑥)) |
90 | 89 | eldifbd 3951 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ¬ 𝑘 ∈ 𝑥) |
91 | | nelne2 3117 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑥 ∧ ¬ 𝑘 ∈ 𝑥) → 𝑦 ≠ 𝑘) |
92 | 88, 90, 91 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ≠ 𝑘) |
93 | 74, 75, 87, 77, 92, 50 | dprdcntz 19132 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝑆‘𝑦) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑘))) |
94 | 7 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → 𝐻 ∈ 𝑊) |
95 | 4, 74, 75, 94 | dprdfcl 19137 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ 𝐼) → (𝐻‘𝑦) ∈ (𝑆‘𝑦)) |
96 | 87, 95 | mpdan 685 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ (𝑆‘𝑦)) |
97 | 93, 96 | sseldd 3970 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ ((Cntz‘𝐺)‘(𝑆‘𝑘))) |
98 | 86, 97 | sseldd 3970 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → (𝐻‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
99 | 73, 98 | eqeltrd 2915 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) ∧ 𝑦 ∈ 𝑥) → ((𝐻 ↾ 𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
100 | 99 | ralrimiva 3184 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ∀𝑦 ∈ 𝑥 ((𝐻 ↾ 𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
101 | | ffnfv 6884 |
. . . . . . . 8
⊢ ((𝐻 ↾ 𝑥):𝑥⟶((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ↔ ((𝐻 ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝐻 ↾ 𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)}))) |
102 | 71, 100, 101 | sylanbrc 585 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
103 | | resss 5880 |
. . . . . . . . . 10
⊢ (𝐻 ↾ 𝑥) ⊆ 𝐻 |
104 | 103 | rnssi 5812 |
. . . . . . . . 9
⊢ ran
(𝐻 ↾ 𝑥) ⊆ ran 𝐻 |
105 | 50 | cntzidss 18470 |
. . . . . . . . 9
⊢ ((ran
𝐻 ⊆
((Cntz‘𝐺)‘ran
𝐻) ∧ ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) → ran (𝐻 ↾ 𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻 ↾ 𝑥))) |
106 | 55, 104, 105 | sylancl 588 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐻 ↾ 𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻 ↾ 𝑥))) |
107 | 106 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ran (𝐻 ↾ 𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻 ↾ 𝑥))) |
108 | 21, 27 | fsuppres 8860 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ↾ 𝑥) finSupp 0 ) |
109 | 108 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥) finSupp 0 ) |
110 | 25, 50, 57, 59, 66, 102, 107, 109 | gsumzsubmcl 19040 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
111 | 110 | snssd 4744 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)})) |
112 | 67, 69 | fssresd 6547 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶(Base‘𝐺)) |
113 | 9, 25, 50, 57, 59, 112, 107, 109 | gsumzcl 19033 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ (Base‘𝐺)) |
114 | 113 | snssd 4744 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ (Base‘𝐺)) |
115 | 9, 50 | cntzrec 18466 |
. . . . . 6
⊢ (({(𝐺 Σg
(𝐻 ↾ 𝑥))} ⊆ (Base‘𝐺) ∧ {(𝐹‘𝑘)} ⊆ (Base‘𝐺)) → ({(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ↔ {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
116 | 114, 64, 115 | syl2anc 586 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → ({(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑘)}) ↔ {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
117 | 111, 116 | mpbid 234 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
118 | | fvex 6685 |
. . . . 5
⊢ (𝐹‘𝑘) ∈ V |
119 | 118 | snss 4720 |
. . . 4
⊢ ((𝐹‘𝑘) ∈ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ {(𝐹‘𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
120 | 117, 119 | sylibr 236 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ (𝐼 ∖ 𝑥))) → (𝐹‘𝑘) ∈ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
121 | 9, 25, 17, 50, 52, 3, 20, 21, 53, 10, 12, 54, 55, 56, 120 | gsumzaddlem 19043 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
122 | 49, 121 | jca 514 |
1
⊢ (𝜑 → ((𝐹 ∘f + 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |