Metamath Proof Explorer

Theorem dprdfadd

Description: Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 ⊢ 0 = ( 0g ‘ 𝐺 )
eldprdi.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
eldprdi.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
eldprdi.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
eldprdi.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
dprdfadd.4 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
dprdfadd.b ⊢ + = ( +g ‘ 𝐺 )
Assertion dprdfadd ( 𝜑 → ( ( 𝐹 ∘f + 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 ⊢ 0 = ( 0g ‘ 𝐺 )
2 eldprdi.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
3 eldprdi.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
4 eldprdi.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
5 eldprdi.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
6 dprdfadd.4 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
7 dprdfadd.b ⊢ + = ( +g ‘ 𝐺 )
8 3 4 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
9 2 3 4 5 dprdfcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
10 2 3 4 6 dprdfcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 2 3 4 5 11 dprdff ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
13 12 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
14 2 3 4 6 11 dprdff ⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
15 14 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐻 ‘ 𝑥 ) ) )
16 8 9 10 13 15 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐻 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) )
17 3 4 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
18 17 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
19 7 subgcl ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ∈ ( 𝑆 ‘ 𝑥 ) )
20 18 9 10 19 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ∈ ( 𝑆 ‘ 𝑥 ) )
21 2 3 4 5 dprdffsupp ⊢ ( 𝜑 → 𝐹 finSupp 0 )
22 2 3 4 6 dprdffsupp ⊢ ( 𝜑 → 𝐻 finSupp 0 )
23 21 22 fsuppunfi ⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) ∈ Fin )
24 ssun1 ⊢ ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) )
25 24 a1i ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) )
26 1 fvexi ⊢ 0 ∈ V
27 26 a1i ⊢ ( 𝜑 → 0 ∈ V )
28 12 25 8 27 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
29 ssun2 ⊢ ( 𝐻 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) )
30 29 a1i ⊢ ( 𝜑 → ( 𝐻 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) )
31 14 30 8 27 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) ) ) → ( 𝐻 ‘ 𝑥 ) = 0 )
32 28 31 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) = ( 0 + 0 ) )
33 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
34 3 33 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
35 11 1 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
36 11 7 1 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( 0 + 0 ) = 0 )
37 34 35 36 syl2anc2 ⊢ ( 𝜑 → ( 0 + 0 ) = 0 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) ) ) → ( 0 + 0 ) = 0 )
39 32 38 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) = 0 )
40 39 8 suppss2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐻 supp 0 ) ) )
41 23 40 ssfid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) supp 0 ) ∈ Fin )
42 funmpt ⊢ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) )
43 42 a1i ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) )
44 8 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) ∈ V )
45 funisfsupp ⊢ ( ( Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) supp 0 ) ∈ Fin ) )
46 43 44 27 45 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) supp 0 ) ∈ Fin ) )
47 41 46 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) finSupp 0 )
48 2 3 4 20 47 dprdwd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) ) ∈ 𝑊 )
49 16 48 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐻 ) ∈ 𝑊 )
50 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
51 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
52 34 51 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
53 eqid ⊢ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) = ( ( 𝐹 ∪ 𝐻 ) supp 0 )
54 2 3 4 5 50 dprdfcntz ⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
55 2 3 4 6 50 dprdfcntz ⊢ ( 𝜑 → ran 𝐻 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐻 ) )
56 2 3 4 49 50 dprdfcntz ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐹 ∘f + 𝐻 ) ) )
57 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝐺 ∈ Mnd )
58 vex ⊢ 𝑥 ∈ V
59 58 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝑥 ∈ V )
60 eldifi ⊢ ( 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) → 𝑘 ∈ 𝐼 )
61 60 adantl ⊢ ( ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) → 𝑘 ∈ 𝐼 )
62 ffvelrn ⊢ ( ( 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
63 12 61 62 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
64 63 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐹 ‘ 𝑘 ) } ⊆ ( Base ‘ 𝐺 ) )
65 11 50 cntzsubm ⊢ ( ( 𝐺 ∈ Mnd ∧ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( Base ‘ 𝐺 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ∈ ( SubMnd ‘ 𝐺 ) )
66 57 64 65 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ∈ ( SubMnd ‘ 𝐺 ) )
67 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝐻 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
68 67 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝐻 Fn 𝐼 )
69 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝑥 ⊆ 𝐼 )
70 fnssres ⊢ ( ( 𝐻 Fn 𝐼 ∧ 𝑥 ⊆ 𝐼 ) → ( 𝐻 ↾ 𝑥 ) Fn 𝑥 )
71 68 69 70 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) Fn 𝑥 )
72 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
74 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐺 dom DProd 𝑆 )
75 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → dom 𝑆 = 𝐼 )
76 74 75 dprdf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
77 61 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑘 ∈ 𝐼 )
78 76 77 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑆 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) )
79 11 subgss ⊢ ( ( 𝑆 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( Base ‘ 𝐺 ) )
80 78 79 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( Base ‘ 𝐺 ) )
81 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 ∈ 𝑊 )
82 2 74 75 81 dprdfcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
83 77 82 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
84 83 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → { ( 𝐹 ‘ 𝑘 ) } ⊆ ( 𝑆 ‘ 𝑘 ) )
85 11 50 cntz2ss ⊢ ( ( ( 𝑆 ‘ 𝑘 ) ⊆ ( Base ‘ 𝐺 ) ∧ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( 𝑆 ‘ 𝑘 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
86 80 84 85 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
87 69 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐼 )
88 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
89 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) )
90 89 eldifbd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑘 ∈ 𝑥 )
91 nelne2 ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑘 ∈ 𝑥 ) → 𝑦 ≠ 𝑘 )
92 88 90 91 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≠ 𝑘 )
93 74 75 87 77 92 50 dprdcntz ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑆 ‘ 𝑦 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) )
94 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐻 ∈ 𝑊 )
95 2 74 75 94 dprdfcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( 𝑆 ‘ 𝑦 ) )
96 87 95 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( 𝑆 ‘ 𝑦 ) )
97 93 96 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) )
98 86 97 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
99 73 98 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
100 99 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
101 ffnfv ⊢ ( ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ↔ ( ( 𝐻 ↾ 𝑥 ) Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ) )
102 71 100 101 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
103 resss ⊢ ( 𝐻 ↾ 𝑥 ) ⊆ 𝐻
104 103 rnssi ⊢ ran ( 𝐻 ↾ 𝑥 ) ⊆ ran 𝐻
105 50 cntzidss ⊢ ( ( ran 𝐻 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐻 ) ∧ ran ( 𝐻 ↾ 𝑥 ) ⊆ ran 𝐻 ) → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐻 ↾ 𝑥 ) ) )
106 55 104 105 sylancl ⊢ ( 𝜑 → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐻 ↾ 𝑥 ) ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐻 ↾ 𝑥 ) ) )
108 22 27 fsuppres ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑥 ) finSupp 0 )
109 108 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) finSupp 0 )
110 1 50 57 59 66 102 107 109 gsumzsubmcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
111 110 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
112 67 69 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( Base ‘ 𝐺 ) )
113 11 1 50 57 59 112 107 109 gsumzcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) ∈ ( Base ‘ 𝐺 ) )
114 113 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( Base ‘ 𝐺 ) )
115 11 50 cntzrec ⊢ ( ( { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( Base ‘ 𝐺 ) ∧ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( Base ‘ 𝐺 ) ) → ( { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ↔ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
116 114 64 115 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ↔ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
117 111 116 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
118 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
119 118 snss ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ↔ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
120 117 119 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
121 11 1 7 50 52 8 21 22 53 12 14 54 55 56 120 gsumzaddlem ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )
122 49 121 jca ⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )