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

Theorem gsumzaddlem 18249
 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 17236 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 . . . . . 6 (𝜑0𝐵)
6 gsumzadd.p . . . . . . 7 + = (+g𝐺)
72, 6, 3mndlid 17239 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
81, 5, 7syl2anc 692 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
98adantr 481 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
10 gsumzaddlem.f . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
11 gsumzadd.a . . . . . . . 8 (𝜑𝐴𝑉)
12 fvex 6163 . . . . . . . . . 10 (0g𝐺) ∈ V
133, 12eqeltri 2694 . . . . . . . . 9 0 ∈ V
1413a1i 11 . . . . . . . 8 (𝜑0 ∈ V)
15 gsumzaddlem.h . . . . . . . . . . 11 (𝜑𝐻:𝐴𝐵)
16 fex 6450 . . . . . . . . . . 11 ((𝐻:𝐴𝐵𝐴𝑉) → 𝐻 ∈ V)
1715, 11, 16syl2anc 692 . . . . . . . . . 10 (𝜑𝐻 ∈ V)
1817suppun 7267 . . . . . . . . 9 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
19 gsumzaddlem.w . . . . . . . . 9 𝑊 = ((𝐹𝐻) supp 0 )
2018, 19syl6sseqr 3636 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
2110, 11, 14, 20gsumcllem 18237 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
2221oveq2d 6626 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
233gsumz 17302 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
241, 11, 23syl2anc 692 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2524adantr 481 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2622, 25eqtrd 2655 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
27 fex 6450 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
2810, 11, 27syl2anc 692 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
2928suppun 7267 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
30 uncom 3740 . . . . . . . . . . 11 (𝐹𝐻) = (𝐻𝐹)
3130oveq1i 6620 . . . . . . . . . 10 ((𝐹𝐻) supp 0 ) = ((𝐻𝐹) supp 0 )
3229, 31syl6sseqr 3636 . . . . . . . . 9 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
3332, 19syl6sseqr 3636 . . . . . . . 8 (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
3415, 11, 14, 33gsumcllem 18237 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐻 = (𝑥𝐴0 ))
3534oveq2d 6626 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥𝐴0 )))
3635, 25eqtrd 2655 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
3726, 36oveq12d 6628 . . . 4 ((𝜑𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
3811adantr 481 . . . . . . . 8 ((𝜑𝑊 = ∅) → 𝐴𝑉)
395ad2antrr 761 . . . . . . . 8 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → 0𝐵)
4038, 39, 39, 21, 34offval2 6874 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴 ↦ ( 0 + 0 )))
419mpteq2dv 4710 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ ( 0 + 0 )) = (𝑥𝐴0 ))
4240, 41eqtrd 2655 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴0 ))
4342oveq2d 6626 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (𝐺 Σg (𝑥𝐴0 )))
4443, 25eqtrd 2655 . . . 4 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = 0 )
459, 37, 443eqtr4rd 2666 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
4645ex 450 . 2 (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
471adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
482, 6mndcl 17229 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧𝐵𝑤𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
49483expb 1263 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5047, 49sylan 488 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5150caovclg 6786 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
52 simprl 793 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ ℕ)
53 nnuz 11674 . . . . . . . 8 ℕ = (ℤ‘1)
5452, 53syl6eleq 2708 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ (ℤ‘1))
5510adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
56 f1of1 6098 . . . . . . . . . . . 12 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–1-1𝑊)
5756ad2antll 764 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1𝑊)
58 suppssdm 7260 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
5958a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻))
6019a1i 11 . . . . . . . . . . . . 13 (𝜑𝑊 = ((𝐹𝐻) supp 0 ))
61 dmun 5296 . . . . . . . . . . . . . 14 dom (𝐹𝐻) = (dom 𝐹 ∪ dom 𝐻)
62 fdm 6013 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
6310, 62syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
64 fdm 6013 . . . . . . . . . . . . . . . . 17 (𝐻:𝐴𝐵 → dom 𝐻 = 𝐴)
6515, 64syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = 𝐴)
6663, 65uneq12d 3751 . . . . . . . . . . . . . . 15 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴𝐴))
67 unidm 3739 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
6866, 67syl6eq 2671 . . . . . . . . . . . . . 14 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
6961, 68syl5req 2668 . . . . . . . . . . . . 13 (𝜑𝐴 = dom (𝐹𝐻))
7059, 60, 693sstr4d 3632 . . . . . . . . . . . 12 (𝜑𝑊𝐴)
7170adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
72 f1ss 6068 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝑊))–1-1𝑊𝑊𝐴) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
7357, 71, 72syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
74 f1f 6063 . . . . . . . . . 10 (𝑓:(1...(#‘𝑊))–1-1𝐴𝑓:(1...(#‘𝑊))⟶𝐴)
7573, 74syl 17 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝐴)
76 fco 6020 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹𝑓):(1...(#‘𝑊))⟶𝐵)
7755, 75, 76syl2anc 692 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓):(1...(#‘𝑊))⟶𝐵)
7877ffvelrnda 6320 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
7915adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐻:𝐴𝐵)
80 fco 6020 . . . . . . . . 9 ((𝐻:𝐴𝐵𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻𝑓):(1...(#‘𝑊))⟶𝐵)
8179, 75, 80syl2anc 692 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓):(1...(#‘𝑊))⟶𝐵)
8281ffvelrnda 6320 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
8355ffnd 6008 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
8479ffnd 6008 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐻 Fn 𝐴)
8511adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐴𝑉)
86 ovex 6638 . . . . . . . . . . . 12 (1...(#‘𝑊)) ∈ V
8786a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (1...(#‘𝑊)) ∈ V)
88 inidm 3805 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
8983, 84, 75, 85, 85, 87, 88ofco 6877 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) ∘ 𝑓) = ((𝐹𝑓) ∘𝑓 + (𝐻𝑓)))
9089fveq1d 6155 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
9190adantr 481 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
92 fnfco 6031 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹𝑓) Fn (1...(#‘𝑊)))
9383, 75, 92syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓) Fn (1...(#‘𝑊)))
94 fnfco 6031 . . . . . . . . . 10 ((𝐻 Fn 𝐴𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻𝑓) Fn (1...(#‘𝑊)))
9584, 75, 94syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓) Fn (1...(#‘𝑊)))
96 inidm 3805 . . . . . . . . 9 ((1...(#‘𝑊)) ∩ (1...(#‘𝑊))) = (1...(#‘𝑊))
97 eqidd 2622 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑓)‘𝑘))
98 eqidd 2622 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) = ((𝐻𝑓)‘𝑘))
9993, 95, 87, 87, 96, 97, 98ofval 6866 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
10091, 99eqtrd 2655 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
1011ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐺 ∈ Mnd)
102 elfzouz 12422 . . . . . . . . . 10 (𝑛 ∈ (1..^(#‘𝑊)) → 𝑛 ∈ (ℤ‘1))
103102adantl 482 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ (ℤ‘1))
104 elfzouz2 12432 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈ (ℤ𝑛))
105104adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈ (ℤ𝑛))
106 fzss2 12330 . . . . . . . . . . . 12 ((#‘𝑊) ∈ (ℤ𝑛) → (1...𝑛) ⊆ (1...(#‘𝑊)))
107105, 106syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (1...𝑛) ⊆ (1...(#‘𝑊)))
108107sselda 3587 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(#‘𝑊)))
10978adantlr 750 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
110108, 109syldan 487 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
1112, 6mndcl 17229 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑘𝐵𝑥𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
1121113expb 1263 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
113101, 112sylan 488 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
114103, 110, 113seqcl 12768 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐹𝑓))‘𝑛) ∈ 𝐵)
11582adantlr 750 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
116108, 115syldan 487 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
117103, 116, 113seqcl 12768 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ 𝐵)
118 fzofzp1 12513 . . . . . . . . 9 (𝑛 ∈ (1..^(#‘𝑊)) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
119 ffvelrn 6318 . . . . . . . . 9 (((𝐹𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
12077, 118, 119syl2an 494 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
121 ffvelrn 6318 . . . . . . . . 9 (((𝐻𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
12281, 118, 121syl2an 494 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
123 fvco3 6237 . . . . . . . . . . . 12 ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
12475, 118, 123syl2an 494 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
125 fveq2 6153 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
126125eleq1d 2683 . . . . . . . . . . . 12 (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
127 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
128127expr 642 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐴𝑥) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
129128ralrimiv 2960 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
130129ex 450 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
131130alrimiv 1852 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
132131ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
133 imassrn 5441 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
13475adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝐴)
135 frn 6015 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))⟶𝐴 → ran 𝑓𝐴)
136134, 135syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝑓𝐴)
137133, 136syl5ss 3598 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
138 vex 3192 . . . . . . . . . . . . . . 15 𝑓 ∈ V
139138imaex 7058 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ∈ V
140 sseq1 3610 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
141 difeq2 3705 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
142 reseq2 5356 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
143142oveq2d 6626 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
144143sneqd 4165 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
145144fveq2d 6157 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
146145eleq2d 2684 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
147141, 146raleqbidv 3144 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
148140, 147imbi12d 334 . . . . . . . . . . . . . 14 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
149139, 148spcv 3288 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
150132, 137, 149sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
151 ffvelrn 6318 . . . . . . . . . . . . . 14 ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
15275, 118, 151syl2an 494 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
153 fzp1nel 12372 . . . . . . . . . . . . . 14 ¬ (𝑛 + 1) ∈ (1...𝑛)
15473adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
155118adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
156 f1elima 6480 . . . . . . . . . . . . . . 15 ((𝑓:(1...(#‘𝑊))–1-1𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊)) ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
157154, 155, 107, 156syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
158153, 157mtbiri 317 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
159152, 158eldifd 3570 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
160126, 150, 159rspcdva 3304 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
161124, 160eqeltrd 2698 . . . . . . . . . 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 761 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐻:𝐴𝐵)
165164, 137fssresd 6033 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
166 gsumzaddlem.2 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
167166ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
168 resss 5386 . . . . . . . . . . . . . . 15 (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
169 rnss 5319 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻)
170168, 169ax-mp 5 . . . . . . . . . . . . . 14 ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
171162cntzidss 17698 . . . . . . . . . . . . . 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 2709 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ ℕ)
174 f1ores 6113 . . . . . . . . . . . . . . 15 ((𝑓:(1...(#‘𝑊))–1-1𝐴 ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
175154, 107, 174syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
176 f1of1 6098 . . . . . . . . . . . . . 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 7260 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
179 dmres 5383 . . . . . . . . . . . . . . . 16 dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
180179a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
181178, 180syl5sseq 3637 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
182 inss1 3816 . . . . . . . . . . . . . . 15 ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
183 df-ima 5092 . . . . . . . . . . . . . . . 16 (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
184183a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
185182, 184syl5sseq 3637 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
186181, 185sstrd 3597 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
187 eqid 2621 . . . . . . . . . . . . 13 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
1882, 3, 6, 162, 101, 163, 165, 172, 173, 177, 186, 187gsumval3 18236 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
189183eqimss2i 3644 . . . . . . . . . . . . . . . . . 18 ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
190 cores 5602 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
191189, 190ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
192 resco 5603 . . . . . . . . . . . . . . . . 17 ((𝐻𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
193191, 192eqtr4i 2646 . . . . . . . . . . . . . . . 16 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻𝑓) ↾ (1...𝑛))
194193fveq1i 6154 . . . . . . . . . . . . . . 15 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻𝑓) ↾ (1...𝑛))‘𝑘)
195 fvres 6169 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → (((𝐻𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻𝑓)‘𝑘))
196194, 195syl5eq 2667 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
197196adantl 482 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
198103, 197seqfveq 12772 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻𝑓))‘𝑛))
199188, 198eqtr2d 2656 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
200 fvex 6163 . . . . . . . . . . . 12 (seq1( + , (𝐻𝑓))‘𝑛) ∈ V
201200elsn 4168 . . . . . . . . . . 11 ((seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
202199, 201sylibr 224 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
2036, 162cntzi 17690 . . . . . . . . . 10 ((((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
204161, 202, 203syl2anc 692 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
205204eqcomd 2627 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) = (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)))
2062, 6, 101, 114, 117, 120, 122, 205mnd4g 17235 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((seq1( + , (𝐹𝑓))‘𝑛) + (seq1( + , (𝐻𝑓))‘𝑛)) + (((𝐹𝑓)‘(𝑛 + 1)) + ((𝐻𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐻𝑓)‘(𝑛 + 1)))))
20751, 51, 54, 78, 82, 100, 206seqcaopr3 12783 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)) = ((seq1( + , (𝐹𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻𝑓))‘(#‘𝑊))))
20850, 55, 79, 85, 85, 88off 6872 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
209 gsumzaddlem.3 . . . . . . . 8 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
210209adantr 481 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
21147, 112sylan 488 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
212211, 55, 79, 85, 85, 88off 6872 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
213 eldifi 3715 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥𝐴)
214 eqidd 2622 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
215 eqidd 2622 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐻𝑥) = (𝐻𝑥))
21683, 84, 85, 85, 88, 214, 215ofval 6866 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
217213, 216sylan2 491 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
21818adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
219 f1ofo 6106 . . . . . . . . . . . . . . . 16 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–onto𝑊)
220 forn 6080 . . . . . . . . . . . . . . . 16 (𝑓:(1...(#‘𝑊))–onto𝑊 → ran 𝑓 = 𝑊)
221219, 220syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ran 𝑓 = 𝑊)
222221, 19syl6eq 2671 . . . . . . . . . . . . . 14 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ran 𝑓 = ((𝐹𝐻) supp 0 ))
223222sseq2d 3617 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
224223ad2antll 764 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
225218, 224mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
22613a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 0 ∈ V)
22755, 225, 85, 226suppssr 7278 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹𝑥) = 0 )
22829adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
229228, 31syl6sseqr 3636 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
230222sseq2d 3617 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
231230ad2antll 764 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
232229, 231mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
23379, 232, 85, 226suppssr 7278 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻𝑥) = 0 )
234227, 233oveq12d 6628 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
2358ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
236217, 234, 2353eqtrd 2659 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = 0 )
237212, 236suppss 7277 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓)
238 ovex 6638 . . . . . . . . 9 (𝐹𝑓 + 𝐻) ∈ V
239238, 138coex 7072 . . . . . . . 8 ((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V
240 suppimacnv 7258 . . . . . . . . 9 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
241240eqcomd 2627 . . . . . . . 8 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ))
242239, 13, 241mp2an 707 . . . . . . 7 (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 )
2432, 3, 6, 162, 47, 85, 208, 210, 52, 73, 237, 242gsumval3 18236 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)))
244 gsumzaddlem.1 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
245244adantr 481 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
246 eqid 2621 . . . . . . . 8 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
2472, 3, 6, 162, 47, 85, 55, 245, 52, 73, 225, 246gsumval3 18236 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))
248166adantr 481 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
249 eqid 2621 . . . . . . . 8 ((𝐻𝑓) supp 0 ) = ((𝐻𝑓) supp 0 )
2502, 3, 6, 162, 47, 85, 79, 248, 52, 73, 232, 249gsumval3 18236 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻𝑓))‘(#‘𝑊)))
251247, 250oveq12d 6628 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻𝑓))‘(#‘𝑊))))
252207, 243, 2513eqtr4d 2665 . . . . 5 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
253252expr 642 . . . 4 ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
254253exlimdv 1858 . . 3 ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
255254expimpd 628 . 2 (𝜑 → (((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
256 gsumzadd.fn . . . . 5 (𝜑𝐹 finSupp 0 )
257 gsumzadd.hn . . . . 5 (𝜑𝐻 finSupp 0 )
258256, 257fsuppun 8245 . . . 4 (𝜑 → ((𝐹𝐻) supp 0 ) ∈ Fin)
25919, 258syl5eqel 2702 . . 3 (𝜑𝑊 ∈ Fin)
260 fz1f1o 14381 . . 3 (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
261259, 260syl 17 . 2 (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
26246, 255, 261mpjaod 396 1 (𝜑 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384  ∀wal 1478   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∀wral 2907  Vcvv 3189   ∖ cdif 3556   ∪ cun 3557   ∩ cin 3558   ⊆ wss 3559  ∅c0 3896  {csn 4153   class class class wbr 4618   ↦ cmpt 4678  ◡ccnv 5078  dom cdm 5079  ran crn 5080   ↾ cres 5081   “ cima 5082   ∘ ccom 5083   Fn wfn 5847  ⟶wf 5848  –1-1→wf1 5849  –onto→wfo 5850  –1-1-onto→wf1o 5851  ‘cfv 5852  (class class class)co 6610   ∘𝑓 cof 6855   supp csupp 7247  Fincfn 7906   finSupp cfsupp 8226  1c1 9888   + caddc 9890  ℕcn 10971  ℤ≥cuz 11638  ...cfz 12275  ..^cfzo 12413  seqcseq 12748  #chash 13064  Basecbs 15788  +gcplusg 15869  0gc0g 16028   Σg cgsu 16029  Mndcmnd 17222  Cntzccntz 17676 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-oi 8366  df-card 8716  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-fz 12276  df-fzo 12414  df-seq 12749  df-hash 13065  df-0g 16030  df-gsum 16031  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-cntz 17678 This theorem is referenced by:  gsumzadd  18250  dprdfadd  18347
 Copyright terms: Public domain W3C validator