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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 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 34 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
52 eqid ⊢ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) = ( ( 𝐹 ∪ 𝐻 ) supp 0 )
53 2 3 4 5 50 dprdfcntz ⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
54 2 3 4 6 50 dprdfcntz ⊢ ( 𝜑 → ran 𝐻 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐻 ) )
55 2 3 4 49 50 dprdfcntz ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐹 ∘f + 𝐻 ) ) )
56 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝐺 ∈ Mnd )
57 vex ⊢ 𝑥 ∈ V
58 57 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝑥 ∈ V )
59 eldifi ⊢ ( 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) → 𝑘 ∈ 𝐼 )
60 59 adantl ⊢ ( ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) → 𝑘 ∈ 𝐼 )
61 ffvelcdm ⊢ ( ( 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
62 12 60 61 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
63 62 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐹 ‘ 𝑘 ) } ⊆ ( Base ‘ 𝐺 ) )
64 11 50 cntzsubm ⊢ ( ( 𝐺 ∈ Mnd ∧ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( Base ‘ 𝐺 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ∈ ( SubMnd ‘ 𝐺 ) )
65 56 63 64 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ∈ ( SubMnd ‘ 𝐺 ) )
66 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝐻 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
67 66 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝐻 Fn 𝐼 )
68 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → 𝑥 ⊆ 𝐼 )
69 fnssres ⊢ ( ( 𝐻 Fn 𝐼 ∧ 𝑥 ⊆ 𝐼 ) → ( 𝐻 ↾ 𝑥 ) Fn 𝑥 )
70 67 68 69 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) Fn 𝑥 )
71 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
73 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐺 dom DProd 𝑆 )
74 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → dom 𝑆 = 𝐼 )
75 73 74 dprdf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
76 60 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑘 ∈ 𝐼 )
77 75 76 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑆 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) )
78 11 subgss ⊢ ( ( 𝑆 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( Base ‘ 𝐺 ) )
79 77 78 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( Base ‘ 𝐺 ) )
80 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 ∈ 𝑊 )
81 2 73 74 80 dprdfcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
82 76 81 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
83 82 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → { ( 𝐹 ‘ 𝑘 ) } ⊆ ( 𝑆 ‘ 𝑘 ) )
84 11 50 cntz2ss ⊢ ( ( ( 𝑆 ‘ 𝑘 ) ⊆ ( Base ‘ 𝐺 ) ∧ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( 𝑆 ‘ 𝑘 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
85 79 83 84 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
86 68 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐼 )
87 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
88 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) )
89 88 eldifbd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑘 ∈ 𝑥 )
90 nelne2 ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑘 ∈ 𝑥 ) → 𝑦 ≠ 𝑘 )
91 87 89 90 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≠ 𝑘 )
92 73 74 86 76 91 50 dprdcntz ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑆 ‘ 𝑦 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) )
93 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐻 ∈ 𝑊 )
94 2 73 74 93 dprdfcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( 𝑆 ‘ 𝑦 ) )
95 86 94 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( 𝑆 ‘ 𝑦 ) )
96 92 95 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑘 ) ) )
97 85 96 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐻 ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
98 72 97 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
99 98 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
100 ffnfv ⊢ ( ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ↔ ( ( 𝐻 ↾ 𝑥 ) Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝐻 ↾ 𝑥 ) ‘ 𝑦 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ) )
101 70 99 100 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
102 resss ⊢ ( 𝐻 ↾ 𝑥 ) ⊆ 𝐻
103 102 rnssi ⊢ ran ( 𝐻 ↾ 𝑥 ) ⊆ ran 𝐻
104 50 cntzidss ⊢ ( ( ran 𝐻 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐻 ) ∧ ran ( 𝐻 ↾ 𝑥 ) ⊆ ran 𝐻 ) → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐻 ↾ 𝑥 ) ) )
105 54 103 104 sylancl ⊢ ( 𝜑 → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐻 ↾ 𝑥 ) ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝐻 ↾ 𝑥 ) ) )
107 22 27 fsuppres ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑥 ) finSupp 0 )
108 107 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) finSupp 0 )
109 1 50 56 58 65 101 106 108 gsumzsubmcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
110 109 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) )
111 66 68 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( Base ‘ 𝐺 ) )
112 11 1 50 56 58 111 106 108 gsumzcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) ∈ ( Base ‘ 𝐺 ) )
113 112 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( Base ‘ 𝐺 ) )
114 11 50 cntzrec ⊢ ( ( { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( Base ‘ 𝐺 ) ∧ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( Base ‘ 𝐺 ) ) → ( { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ↔ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
115 113 63 114 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐹 ‘ 𝑘 ) } ) ↔ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
116 110 115 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
117 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
118 117 snss ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ↔ { ( 𝐹 ‘ 𝑘 ) } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
119 116 118 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ( Cntz ‘ 𝐺 ) ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
120 11 1 7 50 51 8 21 22 52 12 14 53 54 55 119 gsumzaddlem ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )
121 49 120 jca ⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )