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

Theorem gsumzaddlem 18527
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 17515 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 . . . . . 6 (𝜑0𝐵)
6 gsumzadd.p . . . . . . 7 + = (+g𝐺)
72, 6, 3mndlid 17518 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
81, 5, 7syl2anc 573 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
98adantr 466 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
10 gsumzaddlem.f . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
11 gsumzadd.a . . . . . . . 8 (𝜑𝐴𝑉)
123fvexi 6345 . . . . . . . . 9 0 ∈ V
1312a1i 11 . . . . . . . 8 (𝜑0 ∈ V)
14 gsumzaddlem.h . . . . . . . . . . 11 (𝜑𝐻:𝐴𝐵)
15 fex 6635 . . . . . . . . . . 11 ((𝐻:𝐴𝐵𝐴𝑉) → 𝐻 ∈ V)
1614, 11, 15syl2anc 573 . . . . . . . . . 10 (𝜑𝐻 ∈ V)
1716suppun 7469 . . . . . . . . 9 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
18 gsumzaddlem.w . . . . . . . . 9 𝑊 = ((𝐹𝐻) supp 0 )
1917, 18syl6sseqr 3801 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
2010, 11, 13, 19gsumcllem 18515 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
2120oveq2d 6811 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
223gsumz 17581 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
231, 11, 22syl2anc 573 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2423adantr 466 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2521, 24eqtrd 2805 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
26 fex 6635 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
2710, 11, 26syl2anc 573 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
2827suppun 7469 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
29 uncom 3908 . . . . . . . . . . 11 (𝐹𝐻) = (𝐻𝐹)
3029oveq1i 6805 . . . . . . . . . 10 ((𝐹𝐻) supp 0 ) = ((𝐻𝐹) supp 0 )
3128, 30syl6sseqr 3801 . . . . . . . . 9 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
3231, 18syl6sseqr 3801 . . . . . . . 8 (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
3314, 11, 13, 32gsumcllem 18515 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐻 = (𝑥𝐴0 ))
3433oveq2d 6811 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥𝐴0 )))
3534, 24eqtrd 2805 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
3625, 35oveq12d 6813 . . . 4 ((𝜑𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
3711adantr 466 . . . . . . . 8 ((𝜑𝑊 = ∅) → 𝐴𝑉)
385ad2antrr 705 . . . . . . . 8 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → 0𝐵)
3937, 38, 38, 20, 33offval2 7064 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴 ↦ ( 0 + 0 )))
409mpteq2dv 4880 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ ( 0 + 0 )) = (𝑥𝐴0 ))
4139, 40eqtrd 2805 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴0 ))
4241oveq2d 6811 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (𝐺 Σg (𝑥𝐴0 )))
4342, 24eqtrd 2805 . . . 4 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = 0 )
449, 36, 433eqtr4rd 2816 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
4544ex 397 . 2 (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
461adantr 466 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
472, 6mndcl 17508 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧𝐵𝑤𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
48473expb 1113 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
4946, 48sylan 569 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5049caovclg 6976 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
51 simprl 754 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (♯‘𝑊) ∈ ℕ)
52 nnuz 11929 . . . . . . . 8 ℕ = (ℤ‘1)
5351, 52syl6eleq 2860 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (♯‘𝑊) ∈ (ℤ‘1))
5410adantr 466 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
55 f1of1 6278 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))–1-1𝑊)
5655ad2antll 708 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1𝑊)
57 suppssdm 7462 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
5857a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻))
5918a1i 11 . . . . . . . . . . . . 13 (𝜑𝑊 = ((𝐹𝐻) supp 0 ))
60 dmun 5468 . . . . . . . . . . . . . 14 dom (𝐹𝐻) = (dom 𝐹 ∪ dom 𝐻)
6110fdmd 6193 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
6214fdmd 6193 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = 𝐴)
6361, 62uneq12d 3919 . . . . . . . . . . . . . . 15 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴𝐴))
64 unidm 3907 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
6563, 64syl6eq 2821 . . . . . . . . . . . . . 14 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
6660, 65syl5req 2818 . . . . . . . . . . . . 13 (𝜑𝐴 = dom (𝐹𝐻))
6758, 59, 663sstr4d 3797 . . . . . . . . . . . 12 (𝜑𝑊𝐴)
6867adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
69 f1ss 6247 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝑊))–1-1𝑊𝑊𝐴) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
7056, 68, 69syl2anc 573 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
71 f1f 6242 . . . . . . . . . 10 (𝑓:(1...(♯‘𝑊))–1-1𝐴𝑓:(1...(♯‘𝑊))⟶𝐴)
7270, 71syl 17 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
73 fco 6199 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹𝑓):(1...(♯‘𝑊))⟶𝐵)
7454, 72, 73syl2anc 573 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓):(1...(♯‘𝑊))⟶𝐵)
7574ffvelrnda 6504 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
7614adantr 466 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐻:𝐴𝐵)
77 fco 6199 . . . . . . . . 9 ((𝐻:𝐴𝐵𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻𝑓):(1...(♯‘𝑊))⟶𝐵)
7876, 72, 77syl2anc 573 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓):(1...(♯‘𝑊))⟶𝐵)
7978ffvelrnda 6504 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
8054ffnd 6185 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
8176ffnd 6185 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐻 Fn 𝐴)
8211adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐴𝑉)
83 ovexd 6828 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (1...(♯‘𝑊)) ∈ V)
84 inidm 3971 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
8580, 81, 72, 82, 82, 83, 84ofco 7067 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) ∘ 𝑓) = ((𝐹𝑓) ∘𝑓 + (𝐻𝑓)))
8685fveq1d 6335 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
8786adantr 466 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
88 fnfco 6210 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹𝑓) Fn (1...(♯‘𝑊)))
8980, 72, 88syl2anc 573 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓) Fn (1...(♯‘𝑊)))
90 fnfco 6210 . . . . . . . . . 10 ((𝐻 Fn 𝐴𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻𝑓) Fn (1...(♯‘𝑊)))
9181, 72, 90syl2anc 573 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓) Fn (1...(♯‘𝑊)))
92 inidm 3971 . . . . . . . . 9 ((1...(♯‘𝑊)) ∩ (1...(♯‘𝑊))) = (1...(♯‘𝑊))
93 eqidd 2772 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑓)‘𝑘))
94 eqidd 2772 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) = ((𝐻𝑓)‘𝑘))
9589, 91, 83, 83, 92, 93, 94ofval 7056 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
9687, 95eqtrd 2805 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
971ad2antrr 705 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐺 ∈ Mnd)
98 elfzouz 12681 . . . . . . . . . 10 (𝑛 ∈ (1..^(♯‘𝑊)) → 𝑛 ∈ (ℤ‘1))
9998adantl 467 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ (ℤ‘1))
100 elfzouz2 12691 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ𝑛))
101100adantl 467 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ𝑛))
102 fzss2 12587 . . . . . . . . . . . 12 ((♯‘𝑊) ∈ (ℤ𝑛) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
103101, 102syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
104103sselda 3752 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(♯‘𝑊)))
10575adantlr 694 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
106104, 105syldan 579 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
1072, 6mndcl 17508 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑘𝐵𝑥𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
1081073expb 1113 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
10997, 108sylan 569 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
11099, 106, 109seqcl 13027 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐹𝑓))‘𝑛) ∈ 𝐵)
11179adantlr 694 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
112104, 111syldan 579 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
11399, 112, 109seqcl 13027 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ 𝐵)
114 fzofzp1 12772 . . . . . . . . 9 (𝑛 ∈ (1..^(♯‘𝑊)) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
115 ffvelrn 6502 . . . . . . . . 9 (((𝐹𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11674, 114, 115syl2an 583 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
117 ffvelrn 6502 . . . . . . . . 9 (((𝐻𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11878, 114, 117syl2an 583 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
119 fvco3 6419 . . . . . . . . . . . 12 ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
12072, 114, 119syl2an 583 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
121 fveq2 6333 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
122121eleq1d 2835 . . . . . . . . . . . 12 (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
123 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
124123expr 444 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐴𝑥) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
125124ralrimiv 3114 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
126125ex 397 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
127126alrimiv 2007 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
128127ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
129 imassrn 5617 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
13072adantr 466 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
131130frnd 6191 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝑓𝐴)
132129, 131syl5ss 3763 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
133 vex 3354 . . . . . . . . . . . . . . 15 𝑓 ∈ V
134133imaex 7254 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ∈ V
135 sseq1 3775 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
136 difeq2 3873 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
137 reseq2 5528 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
138137oveq2d 6811 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
139138sneqd 4329 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
140139fveq2d 6337 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
141140eleq2d 2836 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
142136, 141raleqbidv 3301 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
143135, 142imbi12d 333 . . . . . . . . . . . . . 14 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
144134, 143spcv 3450 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
145128, 132, 144sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
146 ffvelrn 6502 . . . . . . . . . . . . . 14 ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
14772, 114, 146syl2an 583 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
148 fzp1nel 12630 . . . . . . . . . . . . . 14 ¬ (𝑛 + 1) ∈ (1...𝑛)
14970adantr 466 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
150114adantl 467 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
151 f1elima 6665 . . . . . . . . . . . . . . 15 ((𝑓:(1...(♯‘𝑊))–1-1𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊)) ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
152149, 150, 103, 151syl3anc 1476 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
153148, 152mtbiri 316 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
154147, 153eldifd 3734 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
155122, 145, 154rspcdva 3466 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
156120, 155eqeltrd 2850 . . . . . . . . . 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 705 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐻:𝐴𝐵)
160159, 132fssresd 6212 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
161 gsumzaddlem.2 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
162161ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
163 resss 5562 . . . . . . . . . . . . . . 15 (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
164 rnss 5491 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻)
165163, 164ax-mp 5 . . . . . . . . . . . . . 14 ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
166157cntzidss 17976 . . . . . . . . . . . . . 14 ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
167162, 165, 166sylancl 574 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
16899, 52syl6eleqr 2861 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ ℕ)
169 f1ores 6293 . . . . . . . . . . . . . . 15 ((𝑓:(1...(♯‘𝑊))–1-1𝐴 ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
170149, 103, 169syl2anc 573 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
171 f1of1 6278 . . . . . . . . . . . . . 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 7462 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
174 dmres 5559 . . . . . . . . . . . . . . . 16 dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
175174a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
176173, 175syl5sseq 3802 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
177 inss1 3981 . . . . . . . . . . . . . . 15 ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
178 df-ima 5263 . . . . . . . . . . . . . . . 16 (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
179178a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
180177, 179syl5sseq 3802 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
181176, 180sstrd 3762 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
182 eqid 2771 . . . . . . . . . . . . 13 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
1832, 3, 6, 157, 97, 158, 160, 167, 168, 172, 181, 182gsumval3 18514 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
184178eqimss2i 3809 . . . . . . . . . . . . . . . . . 18 ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
185 cores 5781 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
186184, 185ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
187 resco 5782 . . . . . . . . . . . . . . . . 17 ((𝐻𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
188186, 187eqtr4i 2796 . . . . . . . . . . . . . . . 16 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻𝑓) ↾ (1...𝑛))
189188fveq1i 6334 . . . . . . . . . . . . . . 15 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻𝑓) ↾ (1...𝑛))‘𝑘)
190 fvres 6350 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → (((𝐻𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻𝑓)‘𝑘))
191189, 190syl5eq 2817 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
192191adantl 467 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
19399, 192seqfveq 13031 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻𝑓))‘𝑛))
194183, 193eqtr2d 2806 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
195 fvex 6344 . . . . . . . . . . . 12 (seq1( + , (𝐻𝑓))‘𝑛) ∈ V
196195elsn 4332 . . . . . . . . . . 11 ((seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
197194, 196sylibr 224 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
1986, 157cntzi 17968 . . . . . . . . . 10 ((((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
199156, 197, 198syl2anc 573 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
200199eqcomd 2777 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) = (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)))
2012, 6, 97, 110, 113, 116, 118, 200mnd4g 17514 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((seq1( + , (𝐹𝑓))‘𝑛) + (seq1( + , (𝐻𝑓))‘𝑛)) + (((𝐹𝑓)‘(𝑛 + 1)) + ((𝐻𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐻𝑓)‘(𝑛 + 1)))))
20250, 50, 53, 75, 79, 96, 201seqcaopr3 13042 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(♯‘𝑊)) = ((seq1( + , (𝐹𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻𝑓))‘(♯‘𝑊))))
20349, 54, 76, 82, 82, 84off 7062 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
204 gsumzaddlem.3 . . . . . . . 8 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
205204adantr 466 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
20646, 108sylan 569 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
207206, 54, 76, 82, 82, 84off 7062 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
208 eldifi 3883 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥𝐴)
209 eqidd 2772 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
210 eqidd 2772 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐻𝑥) = (𝐻𝑥))
21180, 81, 82, 82, 84, 209, 210ofval 7056 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
212208, 211sylan2 580 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
21317adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
214 f1ofo 6286 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))–onto𝑊)
215 forn 6260 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝑊))–onto𝑊 → ran 𝑓 = 𝑊)
216214, 215syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ran 𝑓 = 𝑊)
217216, 18syl6eq 2821 . . . . . . . . . . . . . 14 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ran 𝑓 = ((𝐹𝐻) supp 0 ))
218217sseq2d 3782 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
219218ad2antll 708 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
220213, 219mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
22112a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 0 ∈ V)
22254, 220, 82, 221suppssr 7481 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹𝑥) = 0 )
22328adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
224223, 30syl6sseqr 3801 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
225217sseq2d 3782 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
226225ad2antll 708 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
227224, 226mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
22876, 227, 82, 221suppssr 7481 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻𝑥) = 0 )
229222, 228oveq12d 6813 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
2308ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
231212, 229, 2303eqtrd 2809 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = 0 )
232207, 231suppss 7480 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓)
233 ovex 6826 . . . . . . . . 9 (𝐹𝑓 + 𝐻) ∈ V
234233, 133coex 7268 . . . . . . . 8 ((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V
235 suppimacnv 7460 . . . . . . . . 9 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
236235eqcomd 2777 . . . . . . . 8 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ))
237234, 12, 236mp2an 672 . . . . . . 7 (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 )
2382, 3, 6, 157, 46, 82, 203, 205, 51, 70, 232, 237gsumval3 18514 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(♯‘𝑊)))
239 gsumzaddlem.1 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
240239adantr 466 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
241 eqid 2771 . . . . . . . 8 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
2422, 3, 6, 157, 46, 82, 54, 240, 51, 70, 220, 241gsumval3 18514 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))
243161adantr 466 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
244 eqid 2771 . . . . . . . 8 ((𝐻𝑓) supp 0 ) = ((𝐻𝑓) supp 0 )
2452, 3, 6, 157, 46, 82, 76, 243, 51, 70, 227, 244gsumval3 18514 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻𝑓))‘(♯‘𝑊)))
246242, 245oveq12d 6813 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻𝑓))‘(♯‘𝑊))))
247202, 238, 2463eqtr4d 2815 . . . . 5 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
248247expr 444 . . . 4 ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
249248exlimdv 2013 . . 3 ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
250249expimpd 441 . 2 (𝜑 → (((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
251 gsumzadd.fn . . . . 5 (𝜑𝐹 finSupp 0 )
252 gsumzadd.hn . . . . 5 (𝜑𝐻 finSupp 0 )
253251, 252fsuppun 8453 . . . 4 (𝜑 → ((𝐹𝐻) supp 0 ) ∈ Fin)
25418, 253syl5eqel 2854 . . 3 (𝜑𝑊 ∈ Fin)
255 fz1f1o 14648 . . 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 196  wa 382  wo 836  wal 1629   = wceq 1631  wex 1852  wcel 2145  wral 3061  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  {csn 4317   class class class wbr 4787  cmpt 4864  ccnv 5249  dom cdm 5250  ran crn 5251  cres 5252  cima 5253  ccom 5254   Fn wfn 6025  wf 6026  1-1wf1 6027  ontowfo 6028  1-1-ontowf1o 6029  cfv 6030  (class class class)co 6795  𝑓 cof 7045   supp csupp 7449  Fincfn 8112   finSupp cfsupp 8434  1c1 10142   + caddc 10144  cn 11225  cuz 11892  ...cfz 12532  ..^cfzo 12672  seqcseq 13007  chash 13320  Basecbs 16063  +gcplusg 16148  0gc0g 16307   Σg cgsu 16308  Mndcmnd 17501  Cntzccntz 17954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-of 7047  df-om 7216  df-1st 7318  df-2nd 7319  df-supp 7450  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-oadd 7720  df-er 7899  df-en 8113  df-dom 8114  df-sdom 8115  df-fin 8116  df-fsupp 8435  df-oi 8574  df-card 8968  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-nn 11226  df-n0 11499  df-z 11584  df-uz 11893  df-fz 12533  df-fzo 12673  df-seq 13008  df-hash 13321  df-0g 16309  df-gsum 16310  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-cntz 17956
This theorem is referenced by:  gsumzadd  18528  dprdfadd  18626
  Copyright terms: Public domain W3C validator