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

Theorem gsumzaddlem 18144
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 17131 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 . . . . . 6 (𝜑0𝐵)
6 gsumzadd.p . . . . . . 7 + = (+g𝐺)
72, 6, 3mndlid 17134 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
81, 5, 7syl2anc 691 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
98adantr 480 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
10 gsumzaddlem.f . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
11 gsumzadd.a . . . . . . . 8 (𝜑𝐴𝑉)
12 fvex 6113 . . . . . . . . . 10 (0g𝐺) ∈ V
133, 12eqeltri 2684 . . . . . . . . 9 0 ∈ V
1413a1i 11 . . . . . . . 8 (𝜑0 ∈ V)
15 gsumzaddlem.h . . . . . . . . . . 11 (𝜑𝐻:𝐴𝐵)
16 fex 6394 . . . . . . . . . . 11 ((𝐻:𝐴𝐵𝐴𝑉) → 𝐻 ∈ V)
1715, 11, 16syl2anc 691 . . . . . . . . . 10 (𝜑𝐻 ∈ V)
1817suppun 7202 . . . . . . . . 9 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
19 gsumzaddlem.w . . . . . . . . 9 𝑊 = ((𝐹𝐻) supp 0 )
2018, 19syl6sseqr 3615 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
2110, 11, 14, 20gsumcllem 18132 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
2221oveq2d 6565 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
233gsumz 17197 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
241, 11, 23syl2anc 691 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2524adantr 480 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2622, 25eqtrd 2644 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
27 fex 6394 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
2810, 11, 27syl2anc 691 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
2928suppun 7202 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
30 uncom 3719 . . . . . . . . . . 11 (𝐹𝐻) = (𝐻𝐹)
3130oveq1i 6559 . . . . . . . . . 10 ((𝐹𝐻) supp 0 ) = ((𝐻𝐹) supp 0 )
3229, 31syl6sseqr 3615 . . . . . . . . 9 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
3332, 19syl6sseqr 3615 . . . . . . . 8 (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
3415, 11, 14, 33gsumcllem 18132 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐻 = (𝑥𝐴0 ))
3534oveq2d 6565 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥𝐴0 )))
3635, 25eqtrd 2644 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
3726, 36oveq12d 6567 . . . 4 ((𝜑𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
3811adantr 480 . . . . . . . 8 ((𝜑𝑊 = ∅) → 𝐴𝑉)
395ad2antrr 758 . . . . . . . 8 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → 0𝐵)
4038, 39, 39, 21, 34offval2 6812 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴 ↦ ( 0 + 0 )))
419mpteq2dv 4673 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ ( 0 + 0 )) = (𝑥𝐴0 ))
4240, 41eqtrd 2644 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴0 ))
4342oveq2d 6565 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (𝐺 Σg (𝑥𝐴0 )))
4443, 25eqtrd 2644 . . . 4 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = 0 )
459, 37, 443eqtr4rd 2655 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
4645ex 449 . 2 (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
471adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
482, 6mndcl 17124 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧𝐵𝑤𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
49483expb 1258 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5047, 49sylan 487 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5150caovclg 6724 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
52 simprl 790 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ ℕ)
53 nnuz 11599 . . . . . . . 8 ℕ = (ℤ‘1)
5452, 53syl6eleq 2698 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ (ℤ‘1))
5510adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
56 f1of1 6049 . . . . . . . . . . . 12 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–1-1𝑊)
5756ad2antll 761 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1𝑊)
58 suppssdm 7195 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
5958a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻))
6019a1i 11 . . . . . . . . . . . . 13 (𝜑𝑊 = ((𝐹𝐻) supp 0 ))
61 dmun 5253 . . . . . . . . . . . . . 14 dom (𝐹𝐻) = (dom 𝐹 ∪ dom 𝐻)
62 fdm 5964 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
6310, 62syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
64 fdm 5964 . . . . . . . . . . . . . . . . 17 (𝐻:𝐴𝐵 → dom 𝐻 = 𝐴)
6515, 64syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = 𝐴)
6663, 65uneq12d 3730 . . . . . . . . . . . . . . 15 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴𝐴))
67 unidm 3718 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
6866, 67syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
6961, 68syl5req 2657 . . . . . . . . . . . . 13 (𝜑𝐴 = dom (𝐹𝐻))
7059, 60, 693sstr4d 3611 . . . . . . . . . . . 12 (𝜑𝑊𝐴)
7170adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
72 f1ss 6019 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝑊))–1-1𝑊𝑊𝐴) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
7357, 71, 72syl2anc 691 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
74 f1f 6014 . . . . . . . . . 10 (𝑓:(1...(#‘𝑊))–1-1𝐴𝑓:(1...(#‘𝑊))⟶𝐴)
7573, 74syl 17 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝐴)
76 fco 5971 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹𝑓):(1...(#‘𝑊))⟶𝐵)
7755, 75, 76syl2anc 691 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓):(1...(#‘𝑊))⟶𝐵)
7877ffvelrnda 6267 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
7915adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐻:𝐴𝐵)
80 fco 5971 . . . . . . . . 9 ((𝐻:𝐴𝐵𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻𝑓):(1...(#‘𝑊))⟶𝐵)
8179, 75, 80syl2anc 691 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓):(1...(#‘𝑊))⟶𝐵)
8281ffvelrnda 6267 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
8355ffnd 5959 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
8479ffnd 5959 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐻 Fn 𝐴)
8511adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐴𝑉)
86 ovex 6577 . . . . . . . . . . . 12 (1...(#‘𝑊)) ∈ V
8786a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (1...(#‘𝑊)) ∈ V)
88 inidm 3784 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
8983, 84, 75, 85, 85, 87, 88ofco 6815 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) ∘ 𝑓) = ((𝐹𝑓) ∘𝑓 + (𝐻𝑓)))
9089fveq1d 6105 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
9190adantr 480 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
92 fnfco 5982 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹𝑓) Fn (1...(#‘𝑊)))
9383, 75, 92syl2anc 691 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓) Fn (1...(#‘𝑊)))
94 fnfco 5982 . . . . . . . . . 10 ((𝐻 Fn 𝐴𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻𝑓) Fn (1...(#‘𝑊)))
9584, 75, 94syl2anc 691 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓) Fn (1...(#‘𝑊)))
96 inidm 3784 . . . . . . . . 9 ((1...(#‘𝑊)) ∩ (1...(#‘𝑊))) = (1...(#‘𝑊))
97 eqidd 2611 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑓)‘𝑘))
98 eqidd 2611 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) = ((𝐻𝑓)‘𝑘))
9993, 95, 87, 87, 96, 97, 98ofval 6804 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
10091, 99eqtrd 2644 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
1011ad2antrr 758 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐺 ∈ Mnd)
102 elfzouz 12343 . . . . . . . . . 10 (𝑛 ∈ (1..^(#‘𝑊)) → 𝑛 ∈ (ℤ‘1))
103102adantl 481 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ (ℤ‘1))
104 elfzouz2 12353 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈ (ℤ𝑛))
105104adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈ (ℤ𝑛))
106 fzss2 12252 . . . . . . . . . . . 12 ((#‘𝑊) ∈ (ℤ𝑛) → (1...𝑛) ⊆ (1...(#‘𝑊)))
107105, 106syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (1...𝑛) ⊆ (1...(#‘𝑊)))
108107sselda 3568 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(#‘𝑊)))
10978adantlr 747 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
110108, 109syldan 486 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
1112, 6mndcl 17124 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑘𝐵𝑥𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
1121113expb 1258 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
113101, 112sylan 487 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
114103, 110, 113seqcl 12683 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐹𝑓))‘𝑛) ∈ 𝐵)
11582adantlr 747 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
116108, 115syldan 486 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
117103, 116, 113seqcl 12683 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ 𝐵)
118 fzofzp1 12431 . . . . . . . . 9 (𝑛 ∈ (1..^(#‘𝑊)) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
119 ffvelrn 6265 . . . . . . . . 9 (((𝐹𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
12077, 118, 119syl2an 493 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
121 ffvelrn 6265 . . . . . . . . 9 (((𝐻𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
12281, 118, 121syl2an 493 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
123 fvco3 6185 . . . . . . . . . . . 12 ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
12475, 118, 123syl2an 493 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
125 fveq2 6103 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
126125eleq1d 2672 . . . . . . . . . . . 12 (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
127 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
128127expr 641 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐴𝑥) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
129128ralrimiv 2948 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
130129ex 449 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
131130alrimiv 1842 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
132131ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
133 imassrn 5396 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
13475adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝐴)
135 frn 5966 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))⟶𝐴 → ran 𝑓𝐴)
136134, 135syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝑓𝐴)
137133, 136syl5ss 3579 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
138 vex 3176 . . . . . . . . . . . . . . 15 𝑓 ∈ V
139138imaex 6996 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ∈ V
140 sseq1 3589 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
141 difeq2 3684 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
142 reseq2 5312 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
143142oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
144143sneqd 4137 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
145144fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
146145eleq2d 2673 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
147141, 146raleqbidv 3129 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
148140, 147imbi12d 333 . . . . . . . . . . . . . 14 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
149139, 148spcv 3272 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
150132, 137, 149sylc 63 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
151 ffvelrn 6265 . . . . . . . . . . . . . 14 ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
15275, 118, 151syl2an 493 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
153 fzp1nel 12293 . . . . . . . . . . . . . 14 ¬ (𝑛 + 1) ∈ (1...𝑛)
15473adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
155118adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
156 f1elima 6421 . . . . . . . . . . . . . . 15 ((𝑓:(1...(#‘𝑊))–1-1𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊)) ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
157154, 155, 107, 156syl3anc 1318 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
158153, 157mtbiri 316 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
159152, 158eldifd 3551 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
160126, 150, 159rspcdva 3288 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
161124, 160eqeltrd 2688 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
162 gsumzadd.z . . . . . . . . . . . . 13 𝑍 = (Cntz‘𝐺)
163139a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V)
16415ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐻:𝐴𝐵)
165164, 137fssresd 5984 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
166 gsumzaddlem.2 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
167166ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
168 resss 5342 . . . . . . . . . . . . . . 15 (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
169 rnss 5275 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻)
170168, 169ax-mp 5 . . . . . . . . . . . . . 14 ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
171162cntzidss 17593 . . . . . . . . . . . . . 14 ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
172167, 170, 171sylancl 693 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
173103, 53syl6eleqr 2699 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ ℕ)
174 f1ores 6064 . . . . . . . . . . . . . . 15 ((𝑓:(1...(#‘𝑊))–1-1𝐴 ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
175154, 107, 174syl2anc 691 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
176 f1of1 6049 . . . . . . . . . . . . . 14 ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
177175, 176syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
178 suppssdm 7195 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
179 dmres 5339 . . . . . . . . . . . . . . . 16 dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
180179a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
181178, 180syl5sseq 3616 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
182 inss1 3795 . . . . . . . . . . . . . . 15 ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
183 df-ima 5051 . . . . . . . . . . . . . . . 16 (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
184183a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
185182, 184syl5sseq 3616 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
186181, 185sstrd 3578 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
187 eqid 2610 . . . . . . . . . . . . 13 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
1882, 3, 6, 162, 101, 163, 165, 172, 173, 177, 186, 187gsumval3 18131 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
189183eqimss2i 3623 . . . . . . . . . . . . . . . . . 18 ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
190 cores 5555 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
191189, 190ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
192 resco 5556 . . . . . . . . . . . . . . . . 17 ((𝐻𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
193191, 192eqtr4i 2635 . . . . . . . . . . . . . . . 16 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻𝑓) ↾ (1...𝑛))
194193fveq1i 6104 . . . . . . . . . . . . . . 15 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻𝑓) ↾ (1...𝑛))‘𝑘)
195 fvres 6117 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → (((𝐻𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻𝑓)‘𝑘))
196194, 195syl5eq 2656 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
197196adantl 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
198103, 197seqfveq 12687 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻𝑓))‘𝑛))
199188, 198eqtr2d 2645 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
200 fvex 6113 . . . . . . . . . . . 12 (seq1( + , (𝐻𝑓))‘𝑛) ∈ V
201200elsn 4140 . . . . . . . . . . 11 ((seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
202199, 201sylibr 223 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
2036, 162cntzi 17585 . . . . . . . . . 10 ((((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
204161, 202, 203syl2anc 691 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
205204eqcomd 2616 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) = (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)))
2062, 6, 101, 114, 117, 120, 122, 205mnd4g 17130 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((seq1( + , (𝐹𝑓))‘𝑛) + (seq1( + , (𝐻𝑓))‘𝑛)) + (((𝐹𝑓)‘(𝑛 + 1)) + ((𝐻𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐻𝑓)‘(𝑛 + 1)))))
20751, 51, 54, 78, 82, 100, 206seqcaopr3 12698 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)) = ((seq1( + , (𝐹𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻𝑓))‘(#‘𝑊))))
20850, 55, 79, 85, 85, 88off 6810 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
209 gsumzaddlem.3 . . . . . . . 8 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
210209adantr 480 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
21147, 112sylan 487 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
212211, 55, 79, 85, 85, 88off 6810 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
213 eldifi 3694 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥𝐴)
214 eqidd 2611 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
215 eqidd 2611 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐻𝑥) = (𝐻𝑥))
21683, 84, 85, 85, 88, 214, 215ofval 6804 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
217213, 216sylan2 490 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
21818adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
219 f1ofo 6057 . . . . . . . . . . . . . . . 16 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–onto𝑊)
220 forn 6031 . . . . . . . . . . . . . . . 16 (𝑓:(1...(#‘𝑊))–onto𝑊 → ran 𝑓 = 𝑊)
221219, 220syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ran 𝑓 = 𝑊)
222221, 19syl6eq 2660 . . . . . . . . . . . . . 14 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ran 𝑓 = ((𝐹𝐻) supp 0 ))
223222sseq2d 3596 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
224223ad2antll 761 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
225218, 224mpbird 246 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
22613a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 0 ∈ V)
22755, 225, 85, 226suppssr 7213 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹𝑥) = 0 )
22829adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
229228, 31syl6sseqr 3615 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
230222sseq2d 3596 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
231230ad2antll 761 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
232229, 231mpbird 246 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
23379, 232, 85, 226suppssr 7213 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻𝑥) = 0 )
234227, 233oveq12d 6567 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
2358ad2antrr 758 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
236217, 234, 2353eqtrd 2648 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = 0 )
237212, 236suppss 7212 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓)
238 ovex 6577 . . . . . . . . 9 (𝐹𝑓 + 𝐻) ∈ V
239238, 138coex 7011 . . . . . . . 8 ((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V
240 suppimacnv 7193 . . . . . . . . 9 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
241240eqcomd 2616 . . . . . . . 8 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ))
242239, 13, 241mp2an 704 . . . . . . 7 (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 )
2432, 3, 6, 162, 47, 85, 208, 210, 52, 73, 237, 242gsumval3 18131 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)))
244 gsumzaddlem.1 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
245244adantr 480 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
246 eqid 2610 . . . . . . . 8 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
2472, 3, 6, 162, 47, 85, 55, 245, 52, 73, 225, 246gsumval3 18131 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))
248166adantr 480 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
249 eqid 2610 . . . . . . . 8 ((𝐻𝑓) supp 0 ) = ((𝐻𝑓) supp 0 )
2502, 3, 6, 162, 47, 85, 79, 248, 52, 73, 232, 249gsumval3 18131 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻𝑓))‘(#‘𝑊)))
251247, 250oveq12d 6567 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻𝑓))‘(#‘𝑊))))
252207, 243, 2513eqtr4d 2654 . . . . 5 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
253252expr 641 . . . 4 ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
254253exlimdv 1848 . . 3 ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
255254expimpd 627 . 2 (𝜑 → (((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
256 gsumzadd.fn . . . . 5 (𝜑𝐹 finSupp 0 )
257 gsumzadd.hn . . . . 5 (𝜑𝐻 finSupp 0 )
258256, 257fsuppun 8177 . . . 4 (𝜑 → ((𝐹𝐻) supp 0 ) ∈ Fin)
25919, 258syl5eqel 2692 . . 3 (𝜑𝑊 ∈ Fin)
260 fz1f1o 14288 . . 3 (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
261259, 260syl 17 . 2 (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
26246, 255, 261mpjaod 395 1 (𝜑 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wo 382  wa 383  wal 1473   = wceq 1475  wex 1695  wcel 1977  wral 2896  Vcvv 3173  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  {csn 4125   class class class wbr 4583  cmpt 4643  ccnv 5037  dom cdm 5038  ran crn 5039  cres 5040  cima 5041  ccom 5042   Fn wfn 5799  wf 5800  1-1wf1 5801  ontowfo 5802  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  𝑓 cof 6793   supp csupp 7182  Fincfn 7841   finSupp cfsupp 8158  1c1 9816   + caddc 9818  cn 10897  cuz 11563  ...cfz 12197  ..^cfzo 12334  seqcseq 12663  #chash 12979  Basecbs 15695  +gcplusg 15768  0gc0g 15923   Σg cgsu 15924  Mndcmnd 17117  Cntzccntz 17571
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-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-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-cntz 17573
This theorem is referenced by:  gsumzadd  18145  dprdfadd  18242
  Copyright terms: Public domain W3C validator