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

Theorem gsumzaddlem 19698
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 (𝐹f + 𝐻) ⊆ (𝑍‘ran (𝐹f + 𝐻)))
gsumzaddlem.4 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
Assertion
Ref Expression
gsumzaddlem (𝜑 → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σ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 18571 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 . . . . . 6 (𝜑0𝐵)
6 gsumzadd.p . . . . . . 7 + = (+g𝐺)
72, 6, 3mndlid 18576 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
81, 5, 7syl2anc 584 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
98adantr 481 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
10 gsumzaddlem.f . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
11 gsumzadd.a . . . . . . . 8 (𝜑𝐴𝑉)
123fvexi 6856 . . . . . . . . 9 0 ∈ V
1312a1i 11 . . . . . . . 8 (𝜑0 ∈ V)
14 gsumzaddlem.h . . . . . . . . . . 11 (𝜑𝐻:𝐴𝐵)
1514, 11fexd 7177 . . . . . . . . . 10 (𝜑𝐻 ∈ V)
1615suppun 8115 . . . . . . . . 9 (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
17 gsumzaddlem.w . . . . . . . . 9 𝑊 = ((𝐹𝐻) supp 0 )
1816, 17sseqtrrdi 3995 . . . . . . . 8 (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
1910, 11, 13, 18gsumcllem 19685 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
2019oveq2d 7373 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
213gsumz 18646 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
221, 11, 21syl2anc 584 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2322adantr 481 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
2420, 23eqtrd 2776 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
2510, 11fexd 7177 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
2625suppun 8115 . . . . . . . . . 10 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
27 uncom 4113 . . . . . . . . . . 11 (𝐹𝐻) = (𝐻𝐹)
2827oveq1i 7367 . . . . . . . . . 10 ((𝐹𝐻) supp 0 ) = ((𝐻𝐹) supp 0 )
2926, 28sseqtrrdi 3995 . . . . . . . . 9 (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
3029, 17sseqtrrdi 3995 . . . . . . . 8 (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
3114, 11, 13, 30gsumcllem 19685 . . . . . . 7 ((𝜑𝑊 = ∅) → 𝐻 = (𝑥𝐴0 ))
3231oveq2d 7373 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥𝐴0 )))
3332, 23eqtrd 2776 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
3424, 33oveq12d 7375 . . . 4 ((𝜑𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
3511adantr 481 . . . . . . . 8 ((𝜑𝑊 = ∅) → 𝐴𝑉)
365ad2antrr 724 . . . . . . . 8 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → 0𝐵)
3735, 36, 36, 19, 31offval2 7637 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝐹f + 𝐻) = (𝑥𝐴 ↦ ( 0 + 0 )))
389mpteq2dv 5207 . . . . . . 7 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ ( 0 + 0 )) = (𝑥𝐴0 ))
3937, 38eqtrd 2776 . . . . . 6 ((𝜑𝑊 = ∅) → (𝐹f + 𝐻) = (𝑥𝐴0 ))
4039oveq2d 7373 . . . . 5 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹f + 𝐻)) = (𝐺 Σg (𝑥𝐴0 )))
4140, 23eqtrd 2776 . . . 4 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹f + 𝐻)) = 0 )
429, 34, 413eqtr4rd 2787 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
4342ex 413 . 2 (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
441adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐺 ∈ Mnd)
452, 6mndcl 18564 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧𝐵𝑤𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
46453expb 1120 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
4744, 46sylan 580 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
4847caovclg 7546 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
49 simprl 769 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (♯‘𝑊) ∈ ℕ)
50 nnuz 12806 . . . . . . . 8 ℕ = (ℤ‘1)
5149, 50eleqtrdi 2848 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (♯‘𝑊) ∈ (ℤ‘1))
5210adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐹:𝐴𝐵)
53 f1of1 6783 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))–1-1𝑊)
5453ad2antll 727 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1𝑊)
55 suppssdm 8108 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
5655a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻))
5717a1i 11 . . . . . . . . . . . . 13 (𝜑𝑊 = ((𝐹𝐻) supp 0 ))
58 dmun 5866 . . . . . . . . . . . . . 14 dom (𝐹𝐻) = (dom 𝐹 ∪ dom 𝐻)
5910fdmd 6679 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 = 𝐴)
6014fdmd 6679 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = 𝐴)
6159, 60uneq12d 4124 . . . . . . . . . . . . . . 15 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴𝐴))
62 unidm 4112 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
6361, 62eqtrdi 2792 . . . . . . . . . . . . . 14 (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
6458, 63eqtr2id 2789 . . . . . . . . . . . . 13 (𝜑𝐴 = dom (𝐹𝐻))
6556, 57, 643sstr4d 3991 . . . . . . . . . . . 12 (𝜑𝑊𝐴)
6665adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑊𝐴)
67 f1ss 6744 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝑊))–1-1𝑊𝑊𝐴) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
6854, 66, 67syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
69 f1f 6738 . . . . . . . . . 10 (𝑓:(1...(♯‘𝑊))–1-1𝐴𝑓:(1...(♯‘𝑊))⟶𝐴)
7068, 69syl 17 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
71 fco 6692 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹𝑓):(1...(♯‘𝑊))⟶𝐵)
7252, 70, 71syl2anc 584 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓):(1...(♯‘𝑊))⟶𝐵)
7372ffvelcdmda 7035 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
7414adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐻:𝐴𝐵)
75 fco 6692 . . . . . . . . 9 ((𝐻:𝐴𝐵𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻𝑓):(1...(♯‘𝑊))⟶𝐵)
7674, 70, 75syl2anc 584 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓):(1...(♯‘𝑊))⟶𝐵)
7776ffvelcdmda 7035 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
7852ffnd 6669 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐹 Fn 𝐴)
7974ffnd 6669 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐻 Fn 𝐴)
8011adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 𝐴𝑉)
81 ovexd 7392 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (1...(♯‘𝑊)) ∈ V)
82 inidm 4178 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
8378, 79, 70, 80, 80, 81, 82ofco 7640 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹f + 𝐻) ∘ 𝑓) = ((𝐹𝑓) ∘f + (𝐻𝑓)))
8483fveq1d 6844 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (((𝐹f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘f + (𝐻𝑓))‘𝑘))
8584adantr 481 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓) ∘f + (𝐻𝑓))‘𝑘))
86 fnfco 6707 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹𝑓) Fn (1...(♯‘𝑊)))
8778, 70, 86syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹𝑓) Fn (1...(♯‘𝑊)))
88 fnfco 6707 . . . . . . . . . 10 ((𝐻 Fn 𝐴𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻𝑓) Fn (1...(♯‘𝑊)))
8979, 70, 88syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻𝑓) Fn (1...(♯‘𝑊)))
90 inidm 4178 . . . . . . . . 9 ((1...(♯‘𝑊)) ∩ (1...(♯‘𝑊))) = (1...(♯‘𝑊))
91 eqidd 2737 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) = ((𝐹𝑓)‘𝑘))
92 eqidd 2737 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) = ((𝐻𝑓)‘𝑘))
9387, 89, 81, 81, 90, 91, 92ofval 7628 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹𝑓) ∘f + (𝐻𝑓))‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
9485, 93eqtrd 2776 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹𝑓)‘𝑘) + ((𝐻𝑓)‘𝑘)))
951ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐺 ∈ Mnd)
96 elfzouz 13576 . . . . . . . . . 10 (𝑛 ∈ (1..^(♯‘𝑊)) → 𝑛 ∈ (ℤ‘1))
9796adantl 482 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ (ℤ‘1))
98 elfzouz2 13587 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ𝑛))
9998adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ𝑛))
100 fzss2 13481 . . . . . . . . . . . 12 ((♯‘𝑊) ∈ (ℤ𝑛) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
10199, 100syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
102101sselda 3944 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(♯‘𝑊)))
10373adantlr 713 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
104102, 103syldan 591 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹𝑓)‘𝑘) ∈ 𝐵)
1052, 6mndcl 18564 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑘𝐵𝑥𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
1061053expb 1120 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
10795, 106sylan 580 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
10897, 104, 107seqcl 13928 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐹𝑓))‘𝑛) ∈ 𝐵)
10977adantlr 713 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
110102, 109syldan 591 . . . . . . . . 9 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻𝑓)‘𝑘) ∈ 𝐵)
11197, 110, 107seqcl 13928 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ 𝐵)
112 fzofzp1 13669 . . . . . . . . 9 (𝑛 ∈ (1..^(♯‘𝑊)) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
113 ffvelcdm 7032 . . . . . . . . 9 (((𝐹𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11472, 112, 113syl2an 596 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ 𝐵)
115 ffvelcdm 7032 . . . . . . . . 9 (((𝐻𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
11676, 112, 115syl2an 596 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻𝑓)‘(𝑛 + 1)) ∈ 𝐵)
117 fvco3 6940 . . . . . . . . . . . 12 ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
11870, 112, 117syl2an 596 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
119 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
120119eleq1d 2822 . . . . . . . . . . . 12 (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
121 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘 ∈ (𝐴𝑥))) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
122121expr 457 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐴𝑥) → (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
123122ralrimiv 3142 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}))
124123ex 413 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
125124alrimiv 1930 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
126125ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})))
127 imassrn 6024 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
12870adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
129128frnd 6676 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝑓𝐴)
130127, 129sstrid 3955 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
131 vex 3449 . . . . . . . . . . . . . . 15 𝑓 ∈ V
132131imaex 7853 . . . . . . . . . . . . . 14 (𝑓 “ (1...𝑛)) ∈ V
133 sseq1 3969 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
134 difeq2 4076 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
135 reseq2 5932 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
136135oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
137136sneqd 4598 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
138137fveq2d 6846 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
139138eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ (𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
140134, 139raleqbidv 3319 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
141133, 140imbi12d 344 . . . . . . . . . . . . . 14 (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
142132, 141spcv 3564 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ∀𝑘 ∈ (𝐴𝑥)(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
143126, 130, 142sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
144 ffvelcdm 7032 . . . . . . . . . . . . . 14 ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
14570, 112, 144syl2an 596 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
146 fzp1nel 13525 . . . . . . . . . . . . . 14 ¬ (𝑛 + 1) ∈ (1...𝑛)
14768adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1𝐴)
148112adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
149 f1elima 7210 . . . . . . . . . . . . . . 15 ((𝑓:(1...(♯‘𝑊))–1-1𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊)) ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
150147, 148, 101, 149syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
151146, 150mtbiri 326 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
152145, 151eldifd 3921 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
153120, 143, 152rspcdva 3582 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
154118, 153eqeltrd 2838 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
155 gsumzadd.z . . . . . . . . . . . . 13 𝑍 = (Cntz‘𝐺)
156132a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V)
15714ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐻:𝐴𝐵)
158157, 130fssresd 6709 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
159 gsumzaddlem.2 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
160159ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
161 resss 5962 . . . . . . . . . . . . . . 15 (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
162161rnssi 5895 . . . . . . . . . . . . . 14 ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
163155cntzidss 19118 . . . . . . . . . . . . . 14 ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
164160, 162, 163sylancl 586 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
16597, 50eleqtrrdi 2849 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ ℕ)
166 f1ores 6798 . . . . . . . . . . . . . . 15 ((𝑓:(1...(♯‘𝑊))–1-1𝐴 ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
167147, 101, 166syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
168 f1of1 6783 . . . . . . . . . . . . . 14 ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
169167, 168syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
170 suppssdm 8108 . . . . . . . . . . . . . . 15 ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
171 dmres 5959 . . . . . . . . . . . . . . . 16 dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
172171a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
173170, 172sseqtrid 3996 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
174 inss1 4188 . . . . . . . . . . . . . . 15 ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
175 df-ima 5646 . . . . . . . . . . . . . . . 16 (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
176175a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
177174, 176sseqtrid 3996 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
178173, 177sstrd 3954 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
179 eqid 2736 . . . . . . . . . . . . 13 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
1802, 3, 6, 155, 95, 156, 158, 164, 165, 169, 178, 179gsumval3 19684 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
181175eqimss2i 4003 . . . . . . . . . . . . . . . . . 18 ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
182 cores 6201 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
183181, 182ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
184 resco 6202 . . . . . . . . . . . . . . . . 17 ((𝐻𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
185183, 184eqtr4i 2767 . . . . . . . . . . . . . . . 16 ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻𝑓) ↾ (1...𝑛))
186185fveq1i 6843 . . . . . . . . . . . . . . 15 (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻𝑓) ↾ (1...𝑛))‘𝑘)
187 fvres 6861 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → (((𝐻𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻𝑓)‘𝑘))
188186, 187eqtrid 2788 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
189188adantl 482 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻𝑓)‘𝑘))
19097, 189seqfveq 13932 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻𝑓))‘𝑛))
191180, 190eqtr2d 2777 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
192 fvex 6855 . . . . . . . . . . . 12 (seq1( + , (𝐻𝑓))‘𝑛) ∈ V
193192elsn 4601 . . . . . . . . . . 11 ((seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
194191, 193sylibr 233 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
1956, 155cntzi 19109 . . . . . . . . . 10 ((((𝐹𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
196154, 194, 195syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)) = ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))))
197196eqcomd 2742 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) = (((𝐹𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻𝑓))‘𝑛)))
1982, 6, 95, 108, 111, 114, 116, 197mnd4g 18570 . . . . . . 7 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((seq1( + , (𝐹𝑓))‘𝑛) + (seq1( + , (𝐻𝑓))‘𝑛)) + (((𝐹𝑓)‘(𝑛 + 1)) + ((𝐻𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹𝑓))‘𝑛) + ((𝐹𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻𝑓))‘𝑛) + ((𝐻𝑓)‘(𝑛 + 1)))))
19948, 48, 51, 73, 77, 94, 198seqcaopr3 13943 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (seq1( + , ((𝐹f + 𝐻) ∘ 𝑓))‘(♯‘𝑊)) = ((seq1( + , (𝐹𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻𝑓))‘(♯‘𝑊))))
20047, 52, 74, 80, 80, 82off 7635 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹f + 𝐻):𝐴𝐵)
201 gsumzaddlem.3 . . . . . . . 8 (𝜑 → ran (𝐹f + 𝐻) ⊆ (𝑍‘ran (𝐹f + 𝐻)))
202201adantr 481 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran (𝐹f + 𝐻) ⊆ (𝑍‘ran (𝐹f + 𝐻)))
20344, 106sylan 580 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ (𝑘𝐵𝑥𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
204203, 52, 74, 80, 80, 82off 7635 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹f + 𝐻):𝐴𝐵)
205 eldifi 4086 . . . . . . . . . 10 (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥𝐴)
206 eqidd 2737 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
207 eqidd 2737 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → (𝐻𝑥) = (𝐻𝑥))
20878, 79, 80, 80, 82, 206, 207ofval 7628 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥𝐴) → ((𝐹f + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
209205, 208sylan2 593 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹f + 𝐻)‘𝑥) = ((𝐹𝑥) + (𝐻𝑥)))
21016adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
211 f1ofo 6791 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))–onto𝑊)
212 forn 6759 . . . . . . . . . . . . . . . 16 (𝑓:(1...(♯‘𝑊))–onto𝑊 → ran 𝑓 = 𝑊)
213211, 212syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ran 𝑓 = 𝑊)
214213, 17eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ran 𝑓 = ((𝐹𝐻) supp 0 ))
215214sseq2d 3976 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
216215ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
217210, 216mpbird 256 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
21812a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → 0 ∈ V)
21952, 217, 80, 218suppssr 8127 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹𝑥) = 0 )
22026adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻𝐹) supp 0 ))
221220, 28sseqtrrdi 3995 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 ))
222214sseq2d 3976 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
223222ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹𝐻) supp 0 )))
224221, 223mpbird 256 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
22574, 224, 80, 218suppssr 8127 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻𝑥) = 0 )
226219, 225oveq12d 7375 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹𝑥) + (𝐻𝑥)) = ( 0 + 0 ))
2278ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
228209, 226, 2273eqtrd 2780 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹f + 𝐻)‘𝑥) = 0 )
229204, 228suppss 8125 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐹f + 𝐻) supp 0 ) ⊆ ran 𝑓)
230 ovex 7390 . . . . . . . . 9 (𝐹f + 𝐻) ∈ V
231230, 131coex 7867 . . . . . . . 8 ((𝐹f + 𝐻) ∘ 𝑓) ∈ V
232 suppimacnv 8105 . . . . . . . . 9 ((((𝐹f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹f + 𝐻) ∘ 𝑓) supp 0 ) = (((𝐹f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
233232eqcomd 2742 . . . . . . . 8 ((((𝐹f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹f + 𝐻) ∘ 𝑓) supp 0 ))
234231, 12, 233mp2an 690 . . . . . . 7 (((𝐹f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹f + 𝐻) ∘ 𝑓) supp 0 )
2352, 3, 6, 155, 44, 80, 200, 202, 49, 68, 229, 234gsumval3 19684 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹f + 𝐻)) = (seq1( + , ((𝐹f + 𝐻) ∘ 𝑓))‘(♯‘𝑊)))
236 gsumzaddlem.1 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
237236adantr 481 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
238 eqid 2736 . . . . . . . 8 ((𝐹𝑓) supp 0 ) = ((𝐹𝑓) supp 0 )
2392, 3, 6, 155, 44, 80, 52, 237, 49, 68, 217, 238gsumval3 19684 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))
240159adantr 481 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
241 eqid 2736 . . . . . . . 8 ((𝐻𝑓) supp 0 ) = ((𝐻𝑓) supp 0 )
2422, 3, 6, 155, 44, 80, 74, 240, 49, 68, 224, 241gsumval3 19684 . . . . . . 7 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻𝑓))‘(♯‘𝑊)))
243239, 242oveq12d 7375 . . . . . 6 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻𝑓))‘(♯‘𝑊))))
244199, 235, 2433eqtr4d 2786 . . . . 5 ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)) → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
245244expr 457 . . . 4 ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
246245exlimdv 1936 . . 3 ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊 → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
247246expimpd 454 . 2 (𝜑 → (((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊) → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
248 gsumzadd.fn . . . . 5 (𝜑𝐹 finSupp 0 )
249 gsumzadd.hn . . . . 5 (𝜑𝐻 finSupp 0 )
250248, 249fsuppun 9324 . . . 4 (𝜑 → ((𝐹𝐻) supp 0 ) ∈ Fin)
25117, 250eqeltrid 2842 . . 3 (𝜑𝑊 ∈ Fin)
252 fz1f1o 15595 . . 3 (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)))
253251, 252syl 17 . 2 (𝜑 → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)))
25443, 247, 253mpjaod 858 1 (𝜑 → (𝐺 Σg (𝐹f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  wal 1539   = wceq 1541  wex 1781  wcel 2106  wral 3064  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586   class class class wbr 5105  cmpt 5188  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ccom 5637   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  f cof 7615   supp csupp 8092  Fincfn 8883   finSupp cfsupp 9305  1c1 11052   + caddc 11054  cn 12153  cuz 12763  ...cfz 13424  ..^cfzo 13567  seqcseq 13906  chash 14230  Basecbs 17083  +gcplusg 17133  0gc0g 17321   Σg cgsu 17322  Mndcmnd 18556  Cntzccntz 19095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-0g 17323  df-gsum 17324  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-cntz 19097
This theorem is referenced by:  gsumzadd  19699  dprdfadd  19799
  Copyright terms: Public domain W3C validator