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

Theorem gsumzaddlem 18707
Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
Hypotheses
Ref Expression
gsumzadd.b 𝐵 = (Base‘𝐺)
gsumzadd.0 0 = (0g𝐺)
gsumzadd.p + = (+g𝐺)
gsumzadd.z 𝑍 = (Cntz‘𝐺)
gsumzadd.g (𝜑𝐺 ∈ Mnd)
gsumzadd.a (𝜑𝐴𝑉)
gsumzadd.fn (𝜑𝐹 finSupp 0 )
gsumzadd.hn (𝜑𝐻 finSupp 0 )
gsumzaddlem.w 𝑊 = ((𝐹𝐻) supp 0 )
gsumzaddlem.f (𝜑𝐹:𝐴𝐵)
gsumzaddlem.h (𝜑𝐻:𝐴𝐵)
gsumzaddlem.1 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
gsumzaddlem.2 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
gsumzaddlem.3 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
gsumzaddlem.4 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
Assertion
Ref Expression
gsumzaddlem (𝜑 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Distinct variable groups:   𝑥,𝑘, +   0 ,𝑘,𝑥   𝑘,𝐹,𝑥   𝑘,𝐺,𝑥   𝐴,𝑘,𝑥   𝐵,𝑘,𝑥   𝑘,𝐻,𝑥   𝜑,𝑘,𝑥   𝑥,𝑉   𝑘,𝑊,𝑥   𝑘,𝑍,𝑥
Allowed substitution hint:   𝑉(𝑘)

Proof of Theorem gsumzaddlem
Dummy variables 𝑓 𝑛 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumzadd.g . . . . . 6 (𝜑𝐺 ∈ Mnd)
2 gsumzadd.b . . . . . . . 8 𝐵 = (Base‘𝐺)
3 gsumzadd.0 . . . . . . . 8 0 = (0g𝐺)
42, 3mndidcl 17694 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 . . . . . 6 (𝜑0𝐵)
6 gsumzadd.p . . . . . . 7 + = (+g𝐺)
72, 6, 3mndlid 17697 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
81, 5, 7syl2anc 579 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
98adantr 474 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
10 gsumzaddlem.f . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
11 gsumzadd.a . . . . . . . 8 (𝜑𝐴𝑉)
123fvexi 6460 . . . . . . . . 9 0 ∈ V
1312a1i 11 . . . . . . . 8 (𝜑0 ∈ V)
14 gsumzaddlem.h . . . . . . . . . . 11 (𝜑𝐻:𝐴𝐵)
15 fex 6761 . . . . . . . . . . 11 ((𝐻:𝐴𝐵𝐴𝑉) → 𝐻 ∈ V)
1614, 11, 15syl2anc 579 . . . . . . . . . 10 (𝜑𝐻 ∈ V)
1716suppun 7596 . . . . . . . . 9 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
18 gsumzaddlem.w . . . . . . . . 9 𝑊 = ((𝐹𝐻) supp 0 )
1917, 18syl6sseqr 3871 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
2010, 11, 13, 19gsumcllem 18695 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
2120oveq2d 6938 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
223gsumz 17760 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
231, 11, 22syl2anc 579 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2423adantr 474 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2521, 24eqtrd 2814 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
26 fex 6761 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
2710, 11, 26syl2anc 579 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
2827suppun 7596 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
29 uncom 3980 . . . . . . . . . . 11 (𝐹𝐻) = (𝐻𝐹)
3029oveq1i 6932 . . . . . . . . . 10 ((𝐹𝐻) supp 0 ) = ((𝐻𝐹) supp 0 )
3128, 30syl6sseqr 3871 . . . . . . . . 9 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
3231, 18syl6sseqr 3871 . . . . . . . 8 (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
3314, 11, 13, 32gsumcllem 18695 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐻 = (𝑥𝐴0 ))
3433oveq2d 6938 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥𝐴0 )))
3534, 24eqtrd 2814 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
3625, 35oveq12d 6940 . . . 4 ((𝜑𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
3711adantr 474 . . . . . . . 8 ((𝜑𝑊 = ∅) → 𝐴𝑉)
385ad2antrr 716 . . . . . . . 8 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → 0𝐵)
3937, 38, 38, 20, 33offval2 7191 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴 ↦ ( 0 + 0 )))
409mpteq2dv 4980 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ ( 0 + 0 )) = (𝑥𝐴0 ))
4139, 40eqtrd 2814 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴0 ))
4241oveq2d 6938 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (𝐺 Σg (𝑥𝐴0 )))
4342, 24eqtrd 2814 . . . 4 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = 0 )
449, 36, 433eqtr4rd 2825 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
4544ex 403 . 2 (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
461adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
472, 6mndcl 17687 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧𝐵𝑤𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
48473expb 1110 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
4946, 48sylan 575 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5049caovclg 7103 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
51 simprl 761 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (♯‘𝑊) ∈ ℕ)
52 nnuz 12029 . . . . . . . 8 ℕ = (ℤ‘1)
5351, 52syl6eleq 2869 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (♯‘𝑊) ∈ (ℤ‘1))
5410adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
55 f1of1 6390 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))–1-1𝑊)
5655ad2antll 719 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1𝑊)
57 suppssdm 7589 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
5857a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻))
5918a1i 11 . . . . . . . . . . . . 13 (𝜑𝑊 = ((𝐹𝐻) supp 0 ))
60 dmun 5576 . . . . . . . . . . . . . 14 dom (𝐹𝐻) = (dom 𝐹 ∪ dom 𝐻)
6110fdmd 6300 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
6214fdmd 6300 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = 𝐴)
6361, 62uneq12d 3991 . . . . . . . . . . . . . . 15 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴𝐴))
64 unidm 3979 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
6563, 64syl6eq 2830 . . . . . . . . . . . . . 14 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
6660, 65syl5req 2827 . . . . . . . . . . . . 13 (𝜑𝐴 = dom (𝐹𝐻))
6758, 59, 663sstr4d 3867 . . . . . . . . . . . 12 (𝜑𝑊𝐴)
6867adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
69 f1ss 6356 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝑊))–1-1𝑊𝑊𝐴) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
7056, 68, 69syl2anc 579 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
71 f1f 6351 . . . . . . . . . 10 (𝑓:(1...(♯‘𝑊))–1-1𝐴𝑓:(1...(♯‘𝑊))⟶𝐴)
7270, 71syl 17 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
73 fco 6308 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹𝑓):(1...(♯‘𝑊))⟶𝐵)
7454, 72, 73syl2anc 579 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓):(1...(♯‘𝑊))⟶𝐵)
7574ffvelrnda 6623 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
7614adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐻:𝐴𝐵)
77 fco 6308 . . . . . . . . 9 ((𝐻:𝐴𝐵𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻𝑓):(1...(♯‘𝑊))⟶𝐵)
7876, 72, 77syl2anc 579 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓):(1...(♯‘𝑊))⟶𝐵)
7978ffvelrnda 6623 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
8054ffnd 6292 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
8176ffnd 6292 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐻 Fn 𝐴)
8211adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐴𝑉)
83 ovexd 6956 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (1...(♯‘𝑊)) ∈ V)
84 inidm 4043 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
8580, 81, 72, 82, 82, 83, 84ofco 7194 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) ∘ 𝑓) = ((𝐹𝑓) ∘𝑓 + (𝐻𝑓)))
8685fveq1d 6448 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
8786adantr 474 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
88 fnfco 6319 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹𝑓) Fn (1...(♯‘𝑊)))
8980, 72, 88syl2anc 579 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓) Fn (1...(♯‘𝑊)))
90 fnfco 6319 . . . . . . . . . 10 ((𝐻 Fn 𝐴𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻𝑓) Fn (1...(♯‘𝑊)))
9181, 72, 90syl2anc 579 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓) Fn (1...(♯‘𝑊)))
92 inidm 4043 . . . . . . . . 9 ((1...(♯‘𝑊)) ∩ (1...(♯‘𝑊))) = (1...(♯‘𝑊))
93 eqidd 2779 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑓)‘𝑘))
94 eqidd 2779 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) = ((𝐻𝑓)‘𝑘))
9589, 91, 83, 83, 92, 93, 94ofval 7183 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
9687, 95eqtrd 2814 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
971ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐺 ∈ Mnd)
98 elfzouz 12793 . . . . . . . . . 10 (𝑛 ∈ (1..^(♯‘𝑊)) → 𝑛 ∈ (ℤ‘1))
9998adantl 475 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ (ℤ‘1))
100 elfzouz2 12803 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ𝑛))
101100adantl 475 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ𝑛))
102 fzss2 12698 . . . . . . . . . . . 12 ((♯‘𝑊) ∈ (ℤ𝑛) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
103101, 102syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
104103sselda 3821 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(♯‘𝑊)))
10575adantlr 705 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
106104, 105syldan 585 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
1072, 6mndcl 17687 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑘𝐵𝑥𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
1081073expb 1110 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
10997, 108sylan 575 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
11099, 106, 109seqcl 13139 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐹𝑓))‘𝑛) ∈ 𝐵)
11179adantlr 705 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
112104, 111syldan 585 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
11399, 112, 109seqcl 13139 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ 𝐵)
114 fzofzp1 12884 . . . . . . . . 9 (𝑛 ∈ (1..^(♯‘𝑊)) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
115 ffvelrn 6621 . . . . . . . . 9 (((𝐹𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11674, 114, 115syl2an 589 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
117 ffvelrn 6621 . . . . . . . . 9 (((𝐻𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11878, 114, 117syl2an 589 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
119 fvco3 6535 . . . . . . . . . . . 12 ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
12072, 114, 119syl2an 589 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
121 fveq2 6446 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
122121eleq1d 2844 . . . . . . . . . . . 12 (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
123 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
124123expr 450 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐴𝑥) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
125124ralrimiv 3147 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
126125ex 403 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
127126alrimiv 1970 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
128127ad2antrr 716 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
129 imassrn 5731 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
13072adantr 474 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
131130frnd 6298 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝑓𝐴)
132129, 131syl5ss 3832 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
133 vex 3401 . . . . . . . . . . . . . . 15 𝑓 ∈ V
134133imaex 7383 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ∈ V
135 sseq1 3845 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
136 difeq2 3945 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
137 reseq2 5637 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
138137oveq2d 6938 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
139138sneqd 4410 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
140139fveq2d 6450 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
141140eleq2d 2845 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
142136, 141raleqbidv 3326 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
143135, 142imbi12d 336 . . . . . . . . . . . . . 14 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
144134, 143spcv 3501 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
145128, 132, 144sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
146 ffvelrn 6621 . . . . . . . . . . . . . 14 ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
14772, 114, 146syl2an 589 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
148 fzp1nel 12742 . . . . . . . . . . . . . 14 ¬ (𝑛 + 1) ∈ (1...𝑛)
14970adantr 474 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
150114adantl 475 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
151 f1elima 6792 . . . . . . . . . . . . . . 15 ((𝑓:(1...(♯‘𝑊))–1-1𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊)) ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
152149, 150, 103, 151syl3anc 1439 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
153148, 152mtbiri 319 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
154147, 153eldifd 3803 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
155122, 145, 154rspcdva 3517 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
156120, 155eqeltrd 2859 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
157 gsumzadd.z . . . . . . . . . . . . 13 𝑍 = (Cntz‘𝐺)
158134a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V)
15914ad2antrr 716 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐻:𝐴𝐵)
160159, 132fssresd 6321 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
161 gsumzaddlem.2 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
162161ad2antrr 716 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
163 resss 5671 . . . . . . . . . . . . . . 15 (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
164 rnss 5599 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻)
165163, 164ax-mp 5 . . . . . . . . . . . . . 14 ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
166157cntzidss 18153 . . . . . . . . . . . . . 14 ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
167162, 165, 166sylancl 580 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
16899, 52syl6eleqr 2870 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ ℕ)
169 f1ores 6405 . . . . . . . . . . . . . . 15 ((𝑓:(1...(♯‘𝑊))–1-1𝐴 ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
170149, 103, 169syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
171 f1of1 6390 . . . . . . . . . . . . . 14 ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
172170, 171syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
173 suppssdm 7589 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
174 dmres 5668 . . . . . . . . . . . . . . . 16 dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
175174a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
176173, 175syl5sseq 3872 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
177 inss1 4053 . . . . . . . . . . . . . . 15 ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
178 df-ima 5368 . . . . . . . . . . . . . . . 16 (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
179178a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
180177, 179syl5sseq 3872 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
181176, 180sstrd 3831 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
182 eqid 2778 . . . . . . . . . . . . 13 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
1832, 3, 6, 157, 97, 158, 160, 167, 168, 172, 181, 182gsumval3 18694 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
184178eqimss2i 3879 . . . . . . . . . . . . . . . . . 18 ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
185 cores 5892 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
186184, 185ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
187 resco 5893 . . . . . . . . . . . . . . . . 17 ((𝐻𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
188186, 187eqtr4i 2805 . . . . . . . . . . . . . . . 16 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻𝑓) ↾ (1...𝑛))
189188fveq1i 6447 . . . . . . . . . . . . . . 15 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻𝑓) ↾ (1...𝑛))‘𝑘)
190 fvres 6465 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → (((𝐻𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻𝑓)‘𝑘))
191189, 190syl5eq 2826 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
192191adantl 475 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
19399, 192seqfveq 13143 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻𝑓))‘𝑛))
194183, 193eqtr2d 2815 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
195 fvex 6459 . . . . . . . . . . . 12 (seq1( + , (𝐻𝑓))‘𝑛) ∈ V
196195elsn 4413 . . . . . . . . . . 11 ((seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
197194, 196sylibr 226 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
1986, 157cntzi 18145 . . . . . . . . . 10 ((((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
199156, 197, 198syl2anc 579 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
200199eqcomd 2784 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) = (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)))
2012, 6, 97, 110, 113, 116, 118, 200mnd4g 17693 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((seq1( + , (𝐹𝑓))‘𝑛) + (seq1( + , (𝐻𝑓))‘𝑛)) + (((𝐹𝑓)‘(𝑛 + 1)) + ((𝐻𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐻𝑓)‘(𝑛 + 1)))))
20250, 50, 53, 75, 79, 96, 201seqcaopr3 13154 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(♯‘𝑊)) = ((seq1( + , (𝐹𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻𝑓))‘(♯‘𝑊))))
20349, 54, 76, 82, 82, 84off 7189 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
204 gsumzaddlem.3 . . . . . . . 8 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
205204adantr 474 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
20646, 108sylan 575 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
207206, 54, 76, 82, 82, 84off 7189 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
208 eldifi 3955 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥𝐴)
209 eqidd 2779 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
210 eqidd 2779 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐻𝑥) = (𝐻𝑥))
21180, 81, 82, 82, 84, 209, 210ofval 7183 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
212208, 211sylan2 586 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
21317adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
214 f1ofo 6398 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))–onto𝑊)
215 forn 6369 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝑊))–onto𝑊 → ran 𝑓 = 𝑊)
216214, 215syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ran 𝑓 = 𝑊)
217216, 18syl6eq 2830 . . . . . . . . . . . . . 14 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ran 𝑓 = ((𝐹𝐻) supp 0 ))
218217sseq2d 3852 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
219218ad2antll 719 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
220213, 219mpbird 249 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
22112a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 0 ∈ V)
22254, 220, 82, 221suppssr 7608 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹𝑥) = 0 )
22328adantr 474 . . . . . . . . . . . . 13 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
224223, 30syl6sseqr 3871 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
225217sseq2d 3852 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
226225ad2antll 719 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
227224, 226mpbird 249 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
22876, 227, 82, 221suppssr 7608 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻𝑥) = 0 )
229222, 228oveq12d 6940 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
2308ad2antrr 716 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
231212, 229, 2303eqtrd 2818 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = 0 )
232207, 231suppss 7607 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓)
233 ovex 6954 . . . . . . . . 9 (𝐹𝑓 + 𝐻) ∈ V
234233, 133coex 7397 . . . . . . . 8 ((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V
235 suppimacnv 7587 . . . . . . . . 9 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
236235eqcomd 2784 . . . . . . . 8 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ))
237234, 12, 236mp2an 682 . . . . . . 7 (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 )
2382, 3, 6, 157, 46, 82, 203, 205, 51, 70, 232, 237gsumval3 18694 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(♯‘𝑊)))
239 gsumzaddlem.1 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
240239adantr 474 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
241 eqid 2778 . . . . . . . 8 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
2422, 3, 6, 157, 46, 82, 54, 240, 51, 70, 220, 241gsumval3 18694 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))
243161adantr 474 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
244 eqid 2778 . . . . . . . 8 ((𝐻𝑓) supp 0 ) = ((𝐻𝑓) supp 0 )
2452, 3, 6, 157, 46, 82, 76, 243, 51, 70, 227, 244gsumval3 18694 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻𝑓))‘(♯‘𝑊)))
246242, 245oveq12d 6940 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻𝑓))‘(♯‘𝑊))))
247202, 238, 2463eqtr4d 2824 . . . . 5 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
248247expr 450 . . . 4 ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
249248exlimdv 1976 . . 3 ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
250249expimpd 447 . 2 (𝜑 → (((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
251 gsumzadd.fn . . . . 5 (𝜑𝐹 finSupp 0 )
252 gsumzadd.hn . . . . 5 (𝜑𝐻 finSupp 0 )
253251, 252fsuppun 8582 . . . 4 (𝜑 → ((𝐹𝐻) supp 0 ) ∈ Fin)
25418, 253syl5eqel 2863 . . 3 (𝜑𝑊 ∈ Fin)
255 fz1f1o 14848 . . 3 (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)))
256254, 255syl 17 . 2 (𝜑 → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)))
25745, 250, 256mpjaod 849 1 (𝜑 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wo 836  wal 1599   = wceq 1601  wex 1823  wcel 2107  wral 3090  Vcvv 3398  cdif 3789  cun 3790  cin 3791  wss 3792  c0 4141  {csn 4398   class class class wbr 4886  cmpt 4965  ccnv 5354  dom cdm 5355  ran crn 5356  cres 5357  cima 5358  ccom 5359   Fn wfn 6130  wf 6131  1-1wf1 6132  ontowfo 6133  1-1-ontowf1o 6134  cfv 6135  (class class class)co 6922  𝑓 cof 7172   supp csupp 7576  Fincfn 8241   finSupp cfsupp 8563  1c1 10273   + caddc 10275  cn 11374  cuz 11992  ...cfz 12643  ..^cfzo 12784  seqcseq 13119  chash 13435  Basecbs 16255  +gcplusg 16338  0gc0g 16486   Σg cgsu 16487  Mndcmnd 17680  Cntzccntz 18131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-oi 8704  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-n0 11643  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-seq 13120  df-hash 13436  df-0g 16488  df-gsum 16489  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-cntz 18133
This theorem is referenced by:  gsumzadd  18708  dprdfadd  18806
  Copyright terms: Public domain W3C validator