Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dprdfadd Structured version   Visualization version   GIF version

Theorem dprdfadd 18242
 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.)
Hypotheses
Ref Expression
eldprdi.0 0 = (0g𝐺)
eldprdi.w 𝑊 = {X𝑖𝐼 (𝑆𝑖) ∣ finSupp 0 }
eldprdi.1 (𝜑𝐺dom DProd 𝑆)
eldprdi.2 (𝜑 → dom 𝑆 = 𝐼)
eldprdi.3 (𝜑𝐹𝑊)
dprdfadd.4 (𝜑𝐻𝑊)
dprdfadd.b + = (+g𝐺)
Assertion
Ref Expression
dprdfadd (𝜑 → ((𝐹𝑓 + 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
Distinct variable groups:   + ,   ,𝐹   ,𝐻   ,𝑖,𝐺   ,𝐼,𝑖   0 ,   𝑆,,𝑖
Allowed substitution hints:   𝜑(,𝑖)   + (𝑖)   𝐹(𝑖)   𝐻(𝑖)   𝑊(,𝑖)   0 (𝑖)

Proof of Theorem dprdfadd
Dummy variables 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldprdi.1 . . . . 5 (𝜑𝐺dom DProd 𝑆)
2 eldprdi.2 . . . . 5 (𝜑 → dom 𝑆 = 𝐼)
31, 2dprddomcld 18223 . . . 4 (𝜑𝐼 ∈ V)
4 eldprdi.w . . . . 5 𝑊 = {X𝑖𝐼 (𝑆𝑖) ∣ finSupp 0 }
5 eldprdi.3 . . . . 5 (𝜑𝐹𝑊)
64, 1, 2, 5dprdfcl 18235 . . . 4 ((𝜑𝑥𝐼) → (𝐹𝑥) ∈ (𝑆𝑥))
7 dprdfadd.4 . . . . 5 (𝜑𝐻𝑊)
84, 1, 2, 7dprdfcl 18235 . . . 4 ((𝜑𝑥𝐼) → (𝐻𝑥) ∈ (𝑆𝑥))
9 eqid 2610 . . . . . 6 (Base‘𝐺) = (Base‘𝐺)
104, 1, 2, 5, 9dprdff 18234 . . . . 5 (𝜑𝐹:𝐼⟶(Base‘𝐺))
1110feqmptd 6159 . . . 4 (𝜑𝐹 = (𝑥𝐼 ↦ (𝐹𝑥)))
124, 1, 2, 7, 9dprdff 18234 . . . . 5 (𝜑𝐻:𝐼⟶(Base‘𝐺))
1312feqmptd 6159 . . . 4 (𝜑𝐻 = (𝑥𝐼 ↦ (𝐻𝑥)))
143, 6, 8, 11, 13offval2 6812 . . 3 (𝜑 → (𝐹𝑓 + 𝐻) = (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))))
151, 2dprdf2 18229 . . . . . 6 (𝜑𝑆:𝐼⟶(SubGrp‘𝐺))
1615ffvelrnda 6267 . . . . 5 ((𝜑𝑥𝐼) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
17 dprdfadd.b . . . . . 6 + = (+g𝐺)
1817subgcl 17427 . . . . 5 (((𝑆𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐹𝑥) ∈ (𝑆𝑥) ∧ (𝐻𝑥) ∈ (𝑆𝑥)) → ((𝐹𝑥) + (𝐻𝑥)) ∈ (𝑆𝑥))
1916, 6, 8, 18syl3anc 1318 . . . 4 ((𝜑𝑥𝐼) → ((𝐹𝑥) + (𝐻𝑥)) ∈ (𝑆𝑥))
204, 1, 2, 5dprdffsupp 18236 . . . . . . 7 (𝜑𝐹 finSupp 0 )
214, 1, 2, 7dprdffsupp 18236 . . . . . . 7 (𝜑𝐻 finSupp 0 )
2220, 21fsuppunfi 8178 . . . . . 6 (𝜑 → ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) ∈ Fin)
23 ssun1 3738 . . . . . . . . . . 11 (𝐹 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))
2423a1i 11 . . . . . . . . . 10 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))
25 eldprdi.0 . . . . . . . . . . . 12 0 = (0g𝐺)
26 fvex 6113 . . . . . . . . . . . 12 (0g𝐺) ∈ V
2725, 26eqeltri 2684 . . . . . . . . . . 11 0 ∈ V
2827a1i 11 . . . . . . . . . 10 (𝜑0 ∈ V)
2910, 24, 3, 28suppssr 7213 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → (𝐹𝑥) = 0 )
30 ssun2 3739 . . . . . . . . . . 11 (𝐻 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))
3130a1i 11 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))
3212, 31, 3, 28suppssr 7213 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → (𝐻𝑥) = 0 )
3329, 32oveq12d 6567 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
34 dprdgrp 18227 . . . . . . . . . . 11 (𝐺dom DProd 𝑆𝐺 ∈ Grp)
351, 34syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
369, 25grpidcl 17273 . . . . . . . . . . 11 (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
3735, 36syl 17 . . . . . . . . . 10 (𝜑0 ∈ (Base‘𝐺))
389, 17, 25grplid 17275 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 0 ∈ (Base‘𝐺)) → ( 0 + 0 ) = 0 )
3935, 37, 38syl2anc 691 . . . . . . . . 9 (𝜑 → ( 0 + 0 ) = 0 )
4039adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ( 0 + 0 ) = 0 )
4133, 40eqtrd 2644 . . . . . . 7 ((𝜑𝑥 ∈ (𝐼 ∖ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))) → ((𝐹𝑥) + (𝐻𝑥)) = 0 )
4241, 3suppss2 7216 . . . . . 6 (𝜑 → ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 )))
43 ssfi 8065 . . . . . 6 ((((𝐹 supp 0 ) ∪ (𝐻 supp 0 )) ∈ Fin ∧ ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) supp 0 ) ⊆ ((𝐹 supp 0 ) ∪ (𝐻 supp 0 ))) → ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) supp 0 ) ∈ Fin)
4422, 42, 43syl2anc 691 . . . . 5 (𝜑 → ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) supp 0 ) ∈ Fin)
45 funmpt 5840 . . . . . . 7 Fun (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥)))
4645a1i 11 . . . . . 6 (𝜑 → Fun (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))))
47 mptexg 6389 . . . . . . 7 (𝐼 ∈ V → (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) ∈ V)
483, 47syl 17 . . . . . 6 (𝜑 → (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) ∈ V)
49 funisfsupp 8163 . . . . . 6 ((Fun (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) ∧ (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) ∈ V ∧ 0 ∈ V) → ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) finSupp 0 ↔ ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) supp 0 ) ∈ Fin))
5046, 48, 28, 49syl3anc 1318 . . . . 5 (𝜑 → ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) finSupp 0 ↔ ((𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) supp 0 ) ∈ Fin))
5144, 50mpbird 246 . . . 4 (𝜑 → (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) finSupp 0 )
524, 1, 2, 19, 51dprdwd 18233 . . 3 (𝜑 → (𝑥𝐼 ↦ ((𝐹𝑥) + (𝐻𝑥))) ∈ 𝑊)
5314, 52eqeltrd 2688 . 2 (𝜑 → (𝐹𝑓 + 𝐻) ∈ 𝑊)
54 eqid 2610 . . 3 (Cntz‘𝐺) = (Cntz‘𝐺)
55 grpmnd 17252 . . . 4 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
5635, 55syl 17 . . 3 (𝜑𝐺 ∈ Mnd)
57 eqid 2610 . . 3 ((𝐹𝐻) supp 0 ) = ((𝐹𝐻) supp 0 )
584, 1, 2, 5, 54dprdfcntz 18237 . . 3 (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹))
594, 1, 2, 7, 54dprdfcntz 18237 . . 3 (𝜑 → ran 𝐻 ⊆ ((Cntz‘𝐺)‘ran 𝐻))
604, 1, 2, 53, 54dprdfcntz 18237 . . 3 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ ((Cntz‘𝐺)‘ran (𝐹𝑓 + 𝐻)))
6156adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → 𝐺 ∈ Mnd)
62 vex 3176 . . . . . . . 8 𝑥 ∈ V
6362a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → 𝑥 ∈ V)
64 eldifi 3694 . . . . . . . . . . 11 (𝑘 ∈ (𝐼𝑥) → 𝑘𝐼)
6564adantl 481 . . . . . . . . . 10 ((𝑥𝐼𝑘 ∈ (𝐼𝑥)) → 𝑘𝐼)
66 ffvelrn 6265 . . . . . . . . . 10 ((𝐹:𝐼⟶(Base‘𝐺) ∧ 𝑘𝐼) → (𝐹𝑘) ∈ (Base‘𝐺))
6710, 65, 66syl2an 493 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐹𝑘) ∈ (Base‘𝐺))
6867snssd 4281 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → {(𝐹𝑘)} ⊆ (Base‘𝐺))
699, 54cntzsubm 17591 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ {(𝐹𝑘)} ⊆ (Base‘𝐺)) → ((Cntz‘𝐺)‘{(𝐹𝑘)}) ∈ (SubMnd‘𝐺))
7061, 68, 69syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → ((Cntz‘𝐺)‘{(𝐹𝑘)}) ∈ (SubMnd‘𝐺))
7112adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → 𝐻:𝐼⟶(Base‘𝐺))
72 ffn 5958 . . . . . . . . . 10 (𝐻:𝐼⟶(Base‘𝐺) → 𝐻 Fn 𝐼)
7371, 72syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → 𝐻 Fn 𝐼)
74 simprl 790 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → 𝑥𝐼)
75 fnssres 5918 . . . . . . . . 9 ((𝐻 Fn 𝐼𝑥𝐼) → (𝐻𝑥) Fn 𝑥)
7673, 74, 75syl2anc 691 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐻𝑥) Fn 𝑥)
77 fvres 6117 . . . . . . . . . . 11 (𝑦𝑥 → ((𝐻𝑥)‘𝑦) = (𝐻𝑦))
7877adantl 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → ((𝐻𝑥)‘𝑦) = (𝐻𝑦))
791ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝐺dom DProd 𝑆)
802ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → dom 𝑆 = 𝐼)
8179, 80dprdf2 18229 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝑆:𝐼⟶(SubGrp‘𝐺))
8265ad2antlr 759 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝑘𝐼)
8381, 82ffvelrnd 6268 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝑆𝑘) ∈ (SubGrp‘𝐺))
849subgss 17418 . . . . . . . . . . . . 13 ((𝑆𝑘) ∈ (SubGrp‘𝐺) → (𝑆𝑘) ⊆ (Base‘𝐺))
8583, 84syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝑆𝑘) ⊆ (Base‘𝐺))
865ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝐹𝑊)
874, 79, 80, 86dprdfcl 18235 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) ∧ 𝑘𝐼) → (𝐹𝑘) ∈ (𝑆𝑘))
8882, 87mpdan 699 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝐹𝑘) ∈ (𝑆𝑘))
8988snssd 4281 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → {(𝐹𝑘)} ⊆ (𝑆𝑘))
909, 54cntz2ss 17588 . . . . . . . . . . . 12 (((𝑆𝑘) ⊆ (Base‘𝐺) ∧ {(𝐹𝑘)} ⊆ (𝑆𝑘)) → ((Cntz‘𝐺)‘(𝑆𝑘)) ⊆ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
9185, 89, 90syl2anc 691 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → ((Cntz‘𝐺)‘(𝑆𝑘)) ⊆ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
9274sselda 3568 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝑦𝐼)
93 simpr 476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝑦𝑥)
94 simplrr 797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝑘 ∈ (𝐼𝑥))
9594eldifbd 3553 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → ¬ 𝑘𝑥)
96 nelne2 2879 . . . . . . . . . . . . . 14 ((𝑦𝑥 ∧ ¬ 𝑘𝑥) → 𝑦𝑘)
9793, 95, 96syl2anc 691 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝑦𝑘)
9879, 80, 92, 82, 97, 54dprdcntz 18230 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝑆𝑦) ⊆ ((Cntz‘𝐺)‘(𝑆𝑘)))
997ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → 𝐻𝑊)
1004, 79, 80, 99dprdfcl 18235 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) ∧ 𝑦𝐼) → (𝐻𝑦) ∈ (𝑆𝑦))
10192, 100mpdan 699 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝐻𝑦) ∈ (𝑆𝑦))
10298, 101sseldd 3569 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝐻𝑦) ∈ ((Cntz‘𝐺)‘(𝑆𝑘)))
10391, 102sseldd 3569 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → (𝐻𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
10478, 103eqeltrd 2688 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) ∧ 𝑦𝑥) → ((𝐻𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
105104ralrimiva 2949 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → ∀𝑦𝑥 ((𝐻𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
106 ffnfv 6295 . . . . . . . 8 ((𝐻𝑥):𝑥⟶((Cntz‘𝐺)‘{(𝐹𝑘)}) ↔ ((𝐻𝑥) Fn 𝑥 ∧ ∀𝑦𝑥 ((𝐻𝑥)‘𝑦) ∈ ((Cntz‘𝐺)‘{(𝐹𝑘)})))
10776, 105, 106sylanbrc 695 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐻𝑥):𝑥⟶((Cntz‘𝐺)‘{(𝐹𝑘)}))
108 resss 5342 . . . . . . . . . 10 (𝐻𝑥) ⊆ 𝐻
109 rnss 5275 . . . . . . . . . 10 ((𝐻𝑥) ⊆ 𝐻 → ran (𝐻𝑥) ⊆ ran 𝐻)
110108, 109ax-mp 5 . . . . . . . . 9 ran (𝐻𝑥) ⊆ ran 𝐻
11154cntzidss 17593 . . . . . . . . 9 ((ran 𝐻 ⊆ ((Cntz‘𝐺)‘ran 𝐻) ∧ ran (𝐻𝑥) ⊆ ran 𝐻) → ran (𝐻𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻𝑥)))
11259, 110, 111sylancl 693 . . . . . . . 8 (𝜑 → ran (𝐻𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻𝑥)))
113112adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → ran (𝐻𝑥) ⊆ ((Cntz‘𝐺)‘ran (𝐻𝑥)))
11421, 28fsuppres 8183 . . . . . . . 8 (𝜑 → (𝐻𝑥) finSupp 0 )
115114adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐻𝑥) finSupp 0 )
11625, 54, 61, 63, 70, 107, 113, 115gsumzsubmcl 18141 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐺 Σg (𝐻𝑥)) ∈ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
117116snssd 4281 . . . . 5 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → {(𝐺 Σg (𝐻𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹𝑘)}))
11871, 74fssresd 5984 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐻𝑥):𝑥⟶(Base‘𝐺))
1199, 25, 54, 61, 63, 118, 113, 115gsumzcl 18135 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐺 Σg (𝐻𝑥)) ∈ (Base‘𝐺))
120119snssd 4281 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → {(𝐺 Σg (𝐻𝑥))} ⊆ (Base‘𝐺))
1219, 54cntzrec 17589 . . . . . 6 (({(𝐺 Σg (𝐻𝑥))} ⊆ (Base‘𝐺) ∧ {(𝐹𝑘)} ⊆ (Base‘𝐺)) → ({(𝐺 Σg (𝐻𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹𝑘)}) ↔ {(𝐹𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻𝑥))})))
122120, 68, 121syl2anc 691 . . . . 5 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → ({(𝐺 Σg (𝐻𝑥))} ⊆ ((Cntz‘𝐺)‘{(𝐹𝑘)}) ↔ {(𝐹𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻𝑥))})))
123117, 122mpbid 221 . . . 4 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → {(𝐹𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻𝑥))}))
124 fvex 6113 . . . . 5 (𝐹𝑘) ∈ V
125124snss 4259 . . . 4 ((𝐹𝑘) ∈ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻𝑥))}) ↔ {(𝐹𝑘)} ⊆ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻𝑥))}))
126123, 125sylibr 223 . . 3 ((𝜑 ∧ (𝑥𝐼𝑘 ∈ (𝐼𝑥))) → (𝐹𝑘) ∈ ((Cntz‘𝐺)‘{(𝐺 Σg (𝐻𝑥))}))
1279, 25, 17, 54, 56, 3, 20, 21, 57, 10, 12, 58, 59, 60, 126gsumzaddlem 18144 . 2 (𝜑 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
12853, 127jca 553 1 (𝜑 → ((𝐹𝑓 + 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  {csn 4125   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ran crn 5039   ↾ cres 5040  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793   supp csupp 7182  Xcixp 7794  Fincfn 7841   finSupp cfsupp 8158  Basecbs 15695  +gcplusg 15768  0gc0g 15923   Σg cgsu 15924  Mndcmnd 17117  SubMndcsubmnd 17157  Grpcgrp 17245  SubGrpcsubg 17411  Cntzccntz 17571   DProd cdprd 18215 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-subg 17414  df-cntz 17573  df-dprd 18217 This theorem is referenced by:  dprdfsub  18243
 Copyright terms: Public domain W3C validator