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

Theorem gsumzaddlem 18367
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 17355 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 . . . . . 6 (𝜑0𝐵)
6 gsumzadd.p . . . . . . 7 + = (+g𝐺)
72, 6, 3mndlid 17358 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
81, 5, 7syl2anc 694 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
98adantr 480 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
10 gsumzaddlem.f . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
11 gsumzadd.a . . . . . . . 8 (𝜑𝐴𝑉)
12 fvex 6239 . . . . . . . . . 10 (0g𝐺) ∈ V
133, 12eqeltri 2726 . . . . . . . . 9 0 ∈ V
1413a1i 11 . . . . . . . 8 (𝜑0 ∈ V)
15 gsumzaddlem.h . . . . . . . . . . 11 (𝜑𝐻:𝐴𝐵)
16 fex 6530 . . . . . . . . . . 11 ((𝐻:𝐴𝐵𝐴𝑉) → 𝐻 ∈ V)
1715, 11, 16syl2anc 694 . . . . . . . . . 10 (𝜑𝐻 ∈ V)
1817suppun 7360 . . . . . . . . 9 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
19 gsumzaddlem.w . . . . . . . . 9 𝑊 = ((𝐹𝐻) supp 0 )
2018, 19syl6sseqr 3685 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
2110, 11, 14, 20gsumcllem 18355 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
2221oveq2d 6706 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
233gsumz 17421 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
241, 11, 23syl2anc 694 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2524adantr 480 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2622, 25eqtrd 2685 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
27 fex 6530 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
2810, 11, 27syl2anc 694 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
2928suppun 7360 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
30 uncom 3790 . . . . . . . . . . 11 (𝐹𝐻) = (𝐻𝐹)
3130oveq1i 6700 . . . . . . . . . 10 ((𝐹𝐻) supp 0 ) = ((𝐻𝐹) supp 0 )
3229, 31syl6sseqr 3685 . . . . . . . . 9 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
3332, 19syl6sseqr 3685 . . . . . . . 8 (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
3415, 11, 14, 33gsumcllem 18355 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐻 = (𝑥𝐴0 ))
3534oveq2d 6706 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥𝐴0 )))
3635, 25eqtrd 2685 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
3726, 36oveq12d 6708 . . . 4 ((𝜑𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
3811adantr 480 . . . . . . . 8 ((𝜑𝑊 = ∅) → 𝐴𝑉)
395ad2antrr 762 . . . . . . . 8 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → 0𝐵)
4038, 39, 39, 21, 34offval2 6956 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴 ↦ ( 0 + 0 )))
419mpteq2dv 4778 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ ( 0 + 0 )) = (𝑥𝐴0 ))
4240, 41eqtrd 2685 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐹𝑓 + 𝐻) = (𝑥𝐴0 ))
4342oveq2d 6706 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (𝐺 Σg (𝑥𝐴0 )))
4443, 25eqtrd 2685 . . . 4 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = 0 )
459, 37, 443eqtr4rd 2696 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
4645ex 449 . 2 (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
471adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
482, 6mndcl 17348 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧𝐵𝑤𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
49483expb 1285 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5047, 49sylan 487 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
5150caovclg 6868 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
52 simprl 809 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ ℕ)
53 nnuz 11761 . . . . . . . 8 ℕ = (ℤ‘1)
5452, 53syl6eleq 2740 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (#‘𝑊) ∈ (ℤ‘1))
5510adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
56 f1of1 6174 . . . . . . . . . . . 12 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–1-1𝑊)
5756ad2antll 765 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1𝑊)
58 suppssdm 7353 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
5958a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻))
6019a1i 11 . . . . . . . . . . . . 13 (𝜑𝑊 = ((𝐹𝐻) supp 0 ))
61 dmun 5363 . . . . . . . . . . . . . 14 dom (𝐹𝐻) = (dom 𝐹 ∪ dom 𝐻)
62 fdm 6089 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
6310, 62syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
64 fdm 6089 . . . . . . . . . . . . . . . . 17 (𝐻:𝐴𝐵 → dom 𝐻 = 𝐴)
6515, 64syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = 𝐴)
6663, 65uneq12d 3801 . . . . . . . . . . . . . . 15 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴𝐴))
67 unidm 3789 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
6866, 67syl6eq 2701 . . . . . . . . . . . . . 14 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
6961, 68syl5req 2698 . . . . . . . . . . . . 13 (𝜑𝐴 = dom (𝐹𝐻))
7059, 60, 693sstr4d 3681 . . . . . . . . . . . 12 (𝜑𝑊𝐴)
7170adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
72 f1ss 6144 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝑊))–1-1𝑊𝑊𝐴) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
7357, 71, 72syl2anc 694 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
74 f1f 6139 . . . . . . . . . 10 (𝑓:(1...(#‘𝑊))–1-1𝐴𝑓:(1...(#‘𝑊))⟶𝐴)
7573, 74syl 17 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝐴)
76 fco 6096 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹𝑓):(1...(#‘𝑊))⟶𝐵)
7755, 75, 76syl2anc 694 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓):(1...(#‘𝑊))⟶𝐵)
7877ffvelrnda 6399 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
7915adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐻:𝐴𝐵)
80 fco 6096 . . . . . . . . 9 ((𝐻:𝐴𝐵𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻𝑓):(1...(#‘𝑊))⟶𝐵)
8179, 75, 80syl2anc 694 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓):(1...(#‘𝑊))⟶𝐵)
8281ffvelrnda 6399 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
8355ffnd 6084 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
8479ffnd 6084 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐻 Fn 𝐴)
8511adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 𝐴𝑉)
86 ovexd 6720 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (1...(#‘𝑊)) ∈ V)
87 inidm 3855 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
8883, 84, 75, 85, 85, 86, 87ofco 6959 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) ∘ 𝑓) = ((𝐹𝑓) ∘𝑓 + (𝐻𝑓)))
8988fveq1d 6231 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
9089adantr 480 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘))
91 fnfco 6107 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹𝑓) Fn (1...(#‘𝑊)))
9283, 75, 91syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓) Fn (1...(#‘𝑊)))
93 fnfco 6107 . . . . . . . . . 10 ((𝐻 Fn 𝐴𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻𝑓) Fn (1...(#‘𝑊)))
9484, 75, 93syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓) Fn (1...(#‘𝑊)))
95 inidm 3855 . . . . . . . . 9 ((1...(#‘𝑊)) ∩ (1...(#‘𝑊))) = (1...(#‘𝑊))
96 eqidd 2652 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑓)‘𝑘))
97 eqidd 2652 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) = ((𝐻𝑓)‘𝑘))
9892, 94, 86, 86, 95, 96, 97ofval 6948 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓) ∘𝑓 + (𝐻𝑓))‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
9990, 98eqtrd 2685 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
1001ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐺 ∈ Mnd)
101 elfzouz 12513 . . . . . . . . . 10 (𝑛 ∈ (1..^(#‘𝑊)) → 𝑛 ∈ (ℤ‘1))
102101adantl 481 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ (ℤ‘1))
103 elfzouz2 12523 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈ (ℤ𝑛))
104103adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈ (ℤ𝑛))
105 fzss2 12419 . . . . . . . . . . . 12 ((#‘𝑊) ∈ (ℤ𝑛) → (1...𝑛) ⊆ (1...(#‘𝑊)))
106104, 105syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (1...𝑛) ⊆ (1...(#‘𝑊)))
107106sselda 3636 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(#‘𝑊)))
10878adantlr 751 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
109107, 108syldan 486 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
1102, 6mndcl 17348 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑘𝐵𝑥𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
1111103expb 1285 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
112100, 111sylan 487 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
113102, 109, 112seqcl 12861 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐹𝑓))‘𝑛) ∈ 𝐵)
11482adantlr 751 . . . . . . . . . 10 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
115107, 114syldan 486 . . . . . . . . 9 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
116102, 115, 112seqcl 12861 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ 𝐵)
117 fzofzp1 12605 . . . . . . . . 9 (𝑛 ∈ (1..^(#‘𝑊)) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
118 ffvelrn 6397 . . . . . . . . 9 (((𝐹𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11977, 117, 118syl2an 493 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
120 ffvelrn 6397 . . . . . . . . 9 (((𝐻𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
12181, 117, 120syl2an 493 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
122 fvco3 6314 . . . . . . . . . . . 12 ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
12375, 117, 122syl2an 493 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
124 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
125124eleq1d 2715 . . . . . . . . . . . 12 (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
126 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
127126expr 642 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐴𝑥) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
128127ralrimiv 2994 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
129128ex 449 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
130129alrimiv 1895 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
131130ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
132 imassrn 5512 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
13375adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝐴)
134 frn 6091 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))⟶𝐴 → ran 𝑓𝐴)
135133, 134syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝑓𝐴)
136132, 135syl5ss 3647 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
137 vex 3234 . . . . . . . . . . . . . . 15 𝑓 ∈ V
138137imaex 7146 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ∈ V
139 sseq1 3659 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
140 difeq2 3755 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
141 reseq2 5423 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
142141oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
143142sneqd 4222 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
144143fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
145144eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
146140, 145raleqbidv 3182 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
147139, 146imbi12d 333 . . . . . . . . . . . . . 14 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
148138, 147spcv 3330 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
149131, 136, 148sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
150 ffvelrn 6397 . . . . . . . . . . . . . 14 ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
15175, 117, 150syl2an 493 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
152 fzp1nel 12462 . . . . . . . . . . . . . 14 ¬ (𝑛 + 1) ∈ (1...𝑛)
15373adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))–1-1𝐴)
154117adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
155 f1elima 6560 . . . . . . . . . . . . . . 15 ((𝑓:(1...(#‘𝑊))–1-1𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊)) ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
156153, 154, 106, 155syl3anc 1366 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
157152, 156mtbiri 316 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
158151, 157eldifd 3618 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
159125, 149, 158rspcdva 3347 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
160123, 159eqeltrd 2730 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
161 gsumzadd.z . . . . . . . . . . . . 13 𝑍 = (Cntz‘𝐺)
162138a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V)
16315ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐻:𝐴𝐵)
164163, 136fssresd 6109 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
165 gsumzaddlem.2 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
166165ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
167 resss 5457 . . . . . . . . . . . . . . 15 (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
168 rnss 5386 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻)
169167, 168ax-mp 5 . . . . . . . . . . . . . 14 ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
170161cntzidss 17816 . . . . . . . . . . . . . 14 ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
171166, 169, 170sylancl 695 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
172102, 53syl6eleqr 2741 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ ℕ)
173 f1ores 6189 . . . . . . . . . . . . . . 15 ((𝑓:(1...(#‘𝑊))–1-1𝐴 ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
174153, 106, 173syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
175 f1of1 6174 . . . . . . . . . . . . . 14 ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
176174, 175syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
177 suppssdm 7353 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
178 dmres 5454 . . . . . . . . . . . . . . . 16 dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
179178a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
180177, 179syl5sseq 3686 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
181 inss1 3866 . . . . . . . . . . . . . . 15 ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
182 df-ima 5156 . . . . . . . . . . . . . . . 16 (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
183182a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
184181, 183syl5sseq 3686 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
185180, 184sstrd 3646 . . . . . . . . . . . . 13 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
186 eqid 2651 . . . . . . . . . . . . 13 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
1872, 3, 6, 161, 100, 162, 164, 171, 172, 176, 185, 186gsumval3 18354 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
188182eqimss2i 3693 . . . . . . . . . . . . . . . . . 18 ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
189 cores 5676 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
190188, 189ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
191 resco 5677 . . . . . . . . . . . . . . . . 17 ((𝐻𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
192190, 191eqtr4i 2676 . . . . . . . . . . . . . . . 16 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻𝑓) ↾ (1...𝑛))
193192fveq1i 6230 . . . . . . . . . . . . . . 15 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻𝑓) ↾ (1...𝑛))‘𝑘)
194 fvres 6245 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → (((𝐻𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻𝑓)‘𝑘))
195193, 194syl5eq 2697 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
196195adantl 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
197102, 196seqfveq 12865 . . . . . . . . . . . 12 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻𝑓))‘𝑛))
198187, 197eqtr2d 2686 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
199 fvex 6239 . . . . . . . . . . . 12 (seq1( + , (𝐻𝑓))‘𝑛) ∈ V
200199elsn 4225 . . . . . . . . . . 11 ((seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
201198, 200sylibr 224 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
2026, 161cntzi 17808 . . . . . . . . . 10 ((((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
203160, 201, 202syl2anc 694 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
204203eqcomd 2657 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) = (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)))
2052, 6, 100, 113, 116, 119, 121, 204mnd4g 17354 . . . . . . 7 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((seq1( + , (𝐹𝑓))‘𝑛) + (seq1( + , (𝐻𝑓))‘𝑛)) + (((𝐹𝑓)‘(𝑛 + 1)) + ((𝐻𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐻𝑓)‘(𝑛 + 1)))))
20651, 51, 54, 78, 82, 99, 205seqcaopr3 12876 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)) = ((seq1( + , (𝐹𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻𝑓))‘(#‘𝑊))))
20750, 55, 79, 85, 85, 87off 6954 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
208 gsumzaddlem.3 . . . . . . . 8 (𝜑 → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
209208adantr 480 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran (𝐹𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹𝑓 + 𝐻)))
21047, 111sylan 487 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
211210, 55, 79, 85, 85, 87off 6954 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓 + 𝐻):𝐴𝐵)
212 eldifi 3765 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥𝐴)
213 eqidd 2652 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
214 eqidd 2652 . . . . . . . . . . 11 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐻𝑥) = (𝐻𝑥))
21583, 84, 85, 85, 87, 213, 214ofval 6948 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
216212, 215sylan2 490 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
21718adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
218 f1ofo 6182 . . . . . . . . . . . . . . . 16 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))–onto𝑊)
219 forn 6156 . . . . . . . . . . . . . . . 16 (𝑓:(1...(#‘𝑊))–onto𝑊 → ran 𝑓 = 𝑊)
220218, 219syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ran 𝑓 = 𝑊)
221220, 19syl6eq 2701 . . . . . . . . . . . . . 14 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ran 𝑓 = ((𝐹𝐻) supp 0 ))
222221sseq2d 3666 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
223222ad2antll 765 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
224217, 223mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
22513a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → 0 ∈ V)
22655, 224, 85, 225suppssr 7371 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹𝑥) = 0 )
22729adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
228227, 31syl6sseqr 3685 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
229221sseq2d 3666 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
230229ad2antll 765 . . . . . . . . . . . 12 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
231228, 230mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
23279, 231, 85, 225suppssr 7371 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻𝑥) = 0 )
233226, 232oveq12d 6708 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
2348ad2antrr 762 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
235216, 233, 2343eqtrd 2689 . . . . . . . 8 (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑓 + 𝐻)‘𝑥) = 0 )
236211, 235suppss 7370 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐹𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓)
237 ovex 6718 . . . . . . . . 9 (𝐹𝑓 + 𝐻) ∈ V
238237, 137coex 7160 . . . . . . . 8 ((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V
239 suppimacnv 7351 . . . . . . . . 9 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
240239eqcomd 2657 . . . . . . . 8 ((((𝐹𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 ))
241238, 13, 240mp2an 708 . . . . . . 7 (((𝐹𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹𝑓 + 𝐻) ∘ 𝑓) supp 0 )
2422, 3, 6, 161, 47, 85, 207, 209, 52, 73, 236, 241gsumval3 18354 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = (seq1( + , ((𝐹𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)))
243 gsumzaddlem.1 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
244243adantr 480 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
245 eqid 2651 . . . . . . . 8 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
2462, 3, 6, 161, 47, 85, 55, 244, 52, 73, 224, 245gsumval3 18354 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))
247165adantr 480 . . . . . . . 8 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
248 eqid 2651 . . . . . . . 8 ((𝐻𝑓) supp 0 ) = ((𝐻𝑓) supp 0 )
2492, 3, 6, 161, 47, 85, 79, 247, 52, 73, 231, 248gsumval3 18354 . . . . . . 7 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻𝑓))‘(#‘𝑊)))
250246, 249oveq12d 6708 . . . . . 6 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻𝑓))‘(#‘𝑊))))
251206, 242, 2503eqtr4d 2695 . . . . 5 ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
252251expr 642 . . . 4 ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
253252exlimdv 1901 . . 3 ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
254253expimpd 628 . 2 (𝜑 → (((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊) → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
255 gsumzadd.fn . . . . 5 (𝜑𝐹 finSupp 0 )
256 gsumzadd.hn . . . . 5 (𝜑𝐻 finSupp 0 )
257255, 256fsuppun 8335 . . . 4 (𝜑 → ((𝐹𝐻) supp 0 ) ∈ Fin)
25819, 257syl5eqel 2734 . . 3 (𝜑𝑊 ∈ Fin)
259 fz1f1o 14485 . . 3 (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
260258, 259syl 17 . 2 (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)))
26146, 254, 260mpjaod 395 1 (𝜑 → (𝐺 Σg (𝐹𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  wral 2941  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210   class class class wbr 4685  cmpt 4762  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  𝑓 cof 6937   supp csupp 7340  Fincfn 7997   finSupp cfsupp 8316  1c1 9975   + caddc 9977  cn 11058  cuz 11725  ...cfz 12364  ..^cfzo 12504  seqcseq 12841  #chash 13157  Basecbs 15904  +gcplusg 15988  0gc0g 16147   Σg cgsu 16148  Mndcmnd 17341  Cntzccntz 17794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-0g 16149  df-gsum 16150  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-cntz 17796
This theorem is referenced by:  gsumzadd  18368  dprdfadd  18465
  Copyright terms: Public domain W3C validator