MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumzaddlem Structured version   Visualization version   GIF version
Theorem gsumzaddlem 19791
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 18642 . . . . . . 7 (𝐺 ∈ Mnd β†’ 0 ∈ 𝐡)
51, 4syl 17 . . . . . 6 (πœ‘ β†’ 0 ∈ 𝐡)
6 gsumzadd.p . . . . . . 7 + = (+gβ€˜πΊ)
72, 6, 3mndlid 18647 . . . . . 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 6905 . . . . . . . . 9 0 ∈ V
1312a1i 11 . . . . . . . 8 (πœ‘ β†’ 0 ∈ V)
14 gsumzaddlem.h . . . . . . . . . . 11 (πœ‘ β†’ 𝐻:𝐴⟢𝐡)
1514, 11fexd 7231 . . . . . . . . . 10 (πœ‘ β†’ 𝐻 ∈ V)
1615suppun 8171 . . . . . . . . 9 (πœ‘ β†’ (𝐹 supp 0 ) βŠ† ((𝐹 βˆͺ 𝐻) supp 0 ))
17 gsumzaddlem.w . . . . . . . . 9 π‘Š = ((𝐹 βˆͺ 𝐻) supp 0 )
1816, 17sseqtrrdi 4033 . . . . . . . 8 (πœ‘ β†’ (𝐹 supp 0 ) βŠ† π‘Š)
1910, 11, 13, 18gsumcllem 19778 . . . . . . 7 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ 0 ))
2019oveq2d 7427 . . . . . 6 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )))
213gsumz 18719 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
221, 11, 21syl2anc 584 . . . . . . 7 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
2322adantr 481 . . . . . 6 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
2420, 23eqtrd 2772 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐹) = 0 )
2510, 11fexd 7231 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ V)
2625suppun 8171 . . . . . . . . . 10 (πœ‘ β†’ (𝐻 supp 0 ) βŠ† ((𝐻 βˆͺ 𝐹) supp 0 ))
27 uncom 4153 . . . . . . . . . . 11 (𝐹 βˆͺ 𝐻) = (𝐻 βˆͺ 𝐹)
2827oveq1i 7421 . . . . . . . . . 10 ((𝐹 βˆͺ 𝐻) supp 0 ) = ((𝐻 βˆͺ 𝐹) supp 0 )
2926, 28sseqtrrdi 4033 . . . . . . . . 9 (πœ‘ β†’ (𝐻 supp 0 ) βŠ† ((𝐹 βˆͺ 𝐻) supp 0 ))
3029, 17sseqtrrdi 4033 . . . . . . . 8 (πœ‘ β†’ (𝐻 supp 0 ) βŠ† π‘Š)
3114, 11, 13, 30gsumcllem 19778 . . . . . . 7 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐻 = (π‘₯ ∈ 𝐴 ↦ 0 ))
3231oveq2d 7427 . . . . . 6 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐻) = (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )))
3332, 23eqtrd 2772 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐻) = 0 )
3424, 33oveq12d 7429 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((𝐺 Ξ£g 𝐹) + (𝐺 Ξ£g 𝐻)) = ( 0 + 0 ))
3511adantr 481 . . . . . . . 8 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐴 ∈ 𝑉)
365ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) β†’ 0 ∈ 𝐡)
3735, 36, 36, 19, 31offval2 7692 . . . . . . 7 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐹 ∘f + 𝐻) = (π‘₯ ∈ 𝐴 ↦ ( 0 + 0 )))
389mpteq2dv 5250 . . . . . . 7 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (π‘₯ ∈ 𝐴 ↦ ( 0 + 0 )) = (π‘₯ ∈ 𝐴 ↦ 0 ))
3937, 38eqtrd 2772 . . . . . 6 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐹 ∘f + 𝐻) = (π‘₯ ∈ 𝐴 ↦ 0 ))
4039oveq2d 7427 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g (𝐹 ∘f + 𝐻)) = (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )))
4140, 23eqtrd 2772 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g (𝐹 ∘f + 𝐻)) = 0 )
429, 34, 413eqtr4rd 2783 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g (𝐹 ∘f + 𝐻)) = ((𝐺 Ξ£g 𝐹) + (𝐺 Ξ£g 𝐻)))
4342ex 413 . 2 (πœ‘ β†’ (π‘Š = βˆ… β†’ (𝐺 Ξ£g (𝐹 ∘f + 𝐻)) = ((𝐺 Ξ£g 𝐹) + (𝐺 Ξ£g 𝐻))))
441adantr 481 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝐺 ∈ Mnd)
452, 6mndcl 18635 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐡 ∧ 𝑀 ∈ 𝐡) β†’ (𝑧 + 𝑀) ∈ 𝐡)
46453expb 1120 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑧 ∈ 𝐡 ∧ 𝑀 ∈ 𝐡)) β†’ (𝑧 + 𝑀) ∈ 𝐡)
4744, 46sylan 580 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑀 ∈ 𝐡)) β†’ (𝑧 + 𝑀) ∈ 𝐡)
4847caovclg 7601 . . . . . . 7 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
49 simprl 769 . . . . . . . 8 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (β™―β€˜π‘Š) ∈ β„•)
50 nnuz 12867 . . . . . . . 8 β„• = (β„€β‰₯β€˜1)
5149, 50eleqtrdi 2843 . . . . . . 7 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (β™―β€˜π‘Š) ∈ (β„€β‰₯β€˜1))
5210adantr 481 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝐹:𝐴⟢𝐡)
53 f1of1 6832 . . . . . . . . . . . 12 (𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š β†’ 𝑓:(1...(β™―β€˜π‘Š))–1-1β†’π‘Š)
5453ad2antll 727 . . . . . . . . . . 11 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝑓:(1...(β™―β€˜π‘Š))–1-1β†’π‘Š)
55 suppssdm 8164 . . . . . . . . . . . . . 14 ((𝐹 βˆͺ 𝐻) supp 0 ) βŠ† dom (𝐹 βˆͺ 𝐻)
5655a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐹 βˆͺ 𝐻) supp 0 ) βŠ† dom (𝐹 βˆͺ 𝐻))
5717a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Š = ((𝐹 βˆͺ 𝐻) supp 0 ))
58 dmun 5910 . . . . . . . . . . . . . 14 dom (𝐹 βˆͺ 𝐻) = (dom 𝐹 βˆͺ dom 𝐻)
5910fdmd 6728 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom 𝐹 = 𝐴)
6014fdmd 6728 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom 𝐻 = 𝐴)
6159, 60uneq12d 4164 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (dom 𝐹 βˆͺ dom 𝐻) = (𝐴 βˆͺ 𝐴))
62 unidm 4152 . . . . . . . . . . . . . . 15 (𝐴 βˆͺ 𝐴) = 𝐴
6361, 62eqtrdi 2788 . . . . . . . . . . . . . 14 (πœ‘ β†’ (dom 𝐹 βˆͺ dom 𝐻) = 𝐴)
6458, 63eqtr2id 2785 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 = dom (𝐹 βˆͺ 𝐻))
6556, 57, 643sstr4d 4029 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Š βŠ† 𝐴)
6665adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ π‘Š βŠ† 𝐴)
67 f1ss 6793 . . . . . . . . . . 11 ((𝑓:(1...(β™―β€˜π‘Š))–1-1β†’π‘Š ∧ π‘Š βŠ† 𝐴) β†’ 𝑓:(1...(β™―β€˜π‘Š))–1-1→𝐴)
6854, 66, 67syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝑓:(1...(β™―β€˜π‘Š))–1-1→𝐴)
69 f1f 6787 . . . . . . . . . 10 (𝑓:(1...(β™―β€˜π‘Š))–1-1→𝐴 β†’ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴)
7068, 69syl 17 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴)
71 fco 6741 . . . . . . . . 9 ((𝐹:𝐴⟢𝐡 ∧ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴) β†’ (𝐹 ∘ 𝑓):(1...(β™―β€˜π‘Š))⟢𝐡)
7252, 70, 71syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐹 ∘ 𝑓):(1...(β™―β€˜π‘Š))⟢𝐡)
7372ffvelcdmda 7086 . . . . . . 7 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ 𝑓)β€˜π‘˜) ∈ 𝐡)
7414adantr 481 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝐻:𝐴⟢𝐡)
75 fco 6741 . . . . . . . . 9 ((𝐻:𝐴⟢𝐡 ∧ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴) β†’ (𝐻 ∘ 𝑓):(1...(β™―β€˜π‘Š))⟢𝐡)
7674, 70, 75syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐻 ∘ 𝑓):(1...(β™―β€˜π‘Š))⟢𝐡)
7776ffvelcdmda 7086 . . . . . . 7 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐻 ∘ 𝑓)β€˜π‘˜) ∈ 𝐡)
7852ffnd 6718 . . . . . . . . . . 11 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝐹 Fn 𝐴)
7974ffnd 6718 . . . . . . . . . . 11 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝐻 Fn 𝐴)
8011adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ 𝐴 ∈ 𝑉)
81 ovexd 7446 . . . . . . . . . . 11 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (1...(β™―β€˜π‘Š)) ∈ V)
82 inidm 4218 . . . . . . . . . . 11 (𝐴 ∩ 𝐴) = 𝐴
8378, 79, 70, 80, 80, 81, 82ofco 7695 . . . . . . . . . 10 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ ((𝐹 ∘f + 𝐻) ∘ 𝑓) = ((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓)))
8483fveq1d 6893 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (((𝐹 ∘f + 𝐻) ∘ 𝑓)β€˜π‘˜) = (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))β€˜π‘˜))
8584adantr 481 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘f + 𝐻) ∘ 𝑓)β€˜π‘˜) = (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))β€˜π‘˜))
86 fnfco 6756 . . . . . . . . . 10 ((𝐹 Fn 𝐴 ∧ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴) β†’ (𝐹 ∘ 𝑓) Fn (1...(β™―β€˜π‘Š)))
8778, 70, 86syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐹 ∘ 𝑓) Fn (1...(β™―β€˜π‘Š)))
88 fnfco 6756 . . . . . . . . . 10 ((𝐻 Fn 𝐴 ∧ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴) β†’ (𝐻 ∘ 𝑓) Fn (1...(β™―β€˜π‘Š)))
8979, 70, 88syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐻 ∘ 𝑓) Fn (1...(β™―β€˜π‘Š)))
90 inidm 4218 . . . . . . . . 9 ((1...(β™―β€˜π‘Š)) ∩ (1...(β™―β€˜π‘Š))) = (1...(β™―β€˜π‘Š))
91 eqidd 2733 . . . . . . . . 9 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ 𝑓)β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜π‘˜))
92 eqidd 2733 . . . . . . . . 9 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐻 ∘ 𝑓)β€˜π‘˜) = ((𝐻 ∘ 𝑓)β€˜π‘˜))
9387, 89, 81, 81, 90, 91, 92ofval 7683 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))β€˜π‘˜) = (((𝐹 ∘ 𝑓)β€˜π‘˜) + ((𝐻 ∘ 𝑓)β€˜π‘˜)))
9485, 93eqtrd 2772 . . . . . . 7 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘˜ ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘f + 𝐻) ∘ 𝑓)β€˜π‘˜) = (((𝐹 ∘ 𝑓)β€˜π‘˜) + ((𝐻 ∘ 𝑓)β€˜π‘˜)))
951ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ 𝐺 ∈ Mnd)
96 elfzouz 13638 . . . . . . . . . 10 (𝑛 ∈ (1..^(β™―β€˜π‘Š)) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
9796adantl 482 . . . . . . . . 9 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
98 elfzouz2 13649 . . . . . . . . . . . . 13 (𝑛 ∈ (1..^(β™―β€˜π‘Š)) β†’ (β™―β€˜π‘Š) ∈ (β„€β‰₯β€˜π‘›))
9998adantl 482 . . . . . . . . . . . 12 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (β™―β€˜π‘Š) ∈ (β„€β‰₯β€˜π‘›))
100 fzss2 13543 . . . . . . . . . . . 12 ((β™―β€˜π‘Š) ∈ (β„€β‰₯β€˜π‘›) β†’ (1...𝑛) βŠ† (1...(β™―β€˜π‘Š)))
10199, 100syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (1...𝑛) βŠ† (1...(β™―β€˜π‘Š)))
102101sselda 3982 . . . . . . . . . 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 18635 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ π‘˜ ∈ 𝐡 ∧ π‘₯ ∈ 𝐡) β†’ (π‘˜ + π‘₯) ∈ 𝐡)
1061053expb 1120 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (π‘˜ ∈ 𝐡 ∧ π‘₯ ∈ 𝐡)) β†’ (π‘˜ + π‘₯) ∈ 𝐡)
10795, 106sylan 580 . . . . . . . . 9 ((((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) ∧ (π‘˜ ∈ 𝐡 ∧ π‘₯ ∈ 𝐡)) β†’ (π‘˜ + π‘₯) ∈ 𝐡)
10897, 104, 107seqcl 13990 . . . . . . . 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 13990 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) ∈ 𝐡)
112 fzofzp1 13731 . . . . . . . . 9 (𝑛 ∈ (1..^(β™―β€˜π‘Š)) β†’ (𝑛 + 1) ∈ (1...(β™―β€˜π‘Š)))
113 ffvelcdm 7083 . . . . . . . . 9 (((𝐹 ∘ 𝑓):(1...(β™―β€˜π‘Š))⟢𝐡 ∧ (𝑛 + 1) ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ 𝑓)β€˜(𝑛 + 1)) ∈ 𝐡)
11472, 112, 113syl2an 596 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ 𝑓)β€˜(𝑛 + 1)) ∈ 𝐡)
115 ffvelcdm 7083 . . . . . . . . 9 (((𝐻 ∘ 𝑓):(1...(β™―β€˜π‘Š))⟢𝐡 ∧ (𝑛 + 1) ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐻 ∘ 𝑓)β€˜(𝑛 + 1)) ∈ 𝐡)
11676, 112, 115syl2an 596 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((𝐻 ∘ 𝑓)β€˜(𝑛 + 1)) ∈ 𝐡)
117 fvco3 6990 . . . . . . . . . . . 12 ((𝑓:(1...(β™―β€˜π‘Š))⟢𝐴 ∧ (𝑛 + 1) ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ 𝑓)β€˜(𝑛 + 1)) = (πΉβ€˜(π‘“β€˜(𝑛 + 1))))
11870, 112, 117syl2an 596 . . . . . . . . . . 11 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ 𝑓)β€˜(𝑛 + 1)) = (πΉβ€˜(π‘“β€˜(𝑛 + 1))))
119 fveq2 6891 . . . . . . . . . . . . 13 (π‘˜ = (π‘“β€˜(𝑛 + 1)) β†’ (πΉβ€˜π‘˜) = (πΉβ€˜(π‘“β€˜(𝑛 + 1))))
120119eleq1d 2818 . . . . . . . . . . . 12 (π‘˜ = (π‘“β€˜(𝑛 + 1)) β†’ ((πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))}) ↔ (πΉβ€˜(π‘“β€˜(𝑛 + 1))) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))})))
121 gsumzaddlem.4 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘₯ βŠ† 𝐴 ∧ π‘˜ ∈ (𝐴 βˆ– π‘₯))) β†’ (πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))}))
122121expr 457 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ βŠ† 𝐴) β†’ (π‘˜ ∈ (𝐴 βˆ– π‘₯) β†’ (πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))})))
123122ralrimiv 3145 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ βŠ† 𝐴) β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))}))
124123ex 413 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘₯ βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))})))
125124alrimiv 1930 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘₯(π‘₯ βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))})))
126125ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ βˆ€π‘₯(π‘₯ βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))})))
127 imassrn 6070 . . . . . . . . . . . . . 14 (𝑓 β€œ (1...𝑛)) βŠ† ran 𝑓
12870adantr 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ 𝑓:(1...(β™―β€˜π‘Š))⟢𝐴)
129128frnd 6725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ran 𝑓 βŠ† 𝐴)
130127, 129sstrid 3993 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (𝑓 β€œ (1...𝑛)) βŠ† 𝐴)
131 vex 3478 . . . . . . . . . . . . . . 15 𝑓 ∈ V
132131imaex 7909 . . . . . . . . . . . . . 14 (𝑓 β€œ (1...𝑛)) ∈ V
133 sseq1 4007 . . . . . . . . . . . . . . 15 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ (π‘₯ βŠ† 𝐴 ↔ (𝑓 β€œ (1...𝑛)) βŠ† 𝐴))
134 difeq2 4116 . . . . . . . . . . . . . . . 16 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ (𝐴 βˆ– π‘₯) = (𝐴 βˆ– (𝑓 β€œ (1...𝑛))))
135 reseq2 5976 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ (𝐻 β†Ύ π‘₯) = (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))
136135oveq2d 7427 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ (𝐺 Ξ£g (𝐻 β†Ύ π‘₯)) = (𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛)))))
137136sneqd 4640 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ {(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))} = {(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))})
138137fveq2d 6895 . . . . . . . . . . . . . . . . 17 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))}) = (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))}))
139138eleq2d 2819 . . . . . . . . . . . . . . . 16 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ ((πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))}) ↔ (πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))})))
140134, 139raleqbidv 3342 . . . . . . . . . . . . . . 15 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ (βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))}) ↔ βˆ€π‘˜ ∈ (𝐴 βˆ– (𝑓 β€œ (1...𝑛)))(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))})))
141133, 140imbi12d 344 . . . . . . . . . . . . . 14 (π‘₯ = (𝑓 β€œ (1...𝑛)) β†’ ((π‘₯ βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))})) ↔ ((𝑓 β€œ (1...𝑛)) βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– (𝑓 β€œ (1...𝑛)))(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))}))))
142132, 141spcv 3595 . . . . . . . . . . . . 13 (βˆ€π‘₯(π‘₯ βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– π‘₯)(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ π‘₯))})) β†’ ((𝑓 β€œ (1...𝑛)) βŠ† 𝐴 β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– (𝑓 β€œ (1...𝑛)))(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))})))
143126, 130, 142sylc 65 . . . . . . . . . . . 12 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ βˆ€π‘˜ ∈ (𝐴 βˆ– (𝑓 β€œ (1...𝑛)))(πΉβ€˜π‘˜) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))}))
144 ffvelcdm 7083 . . . . . . . . . . . . . 14 ((𝑓:(1...(β™―β€˜π‘Š))⟢𝐴 ∧ (𝑛 + 1) ∈ (1...(β™―β€˜π‘Š))) β†’ (π‘“β€˜(𝑛 + 1)) ∈ 𝐴)
14570, 112, 144syl2an 596 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (π‘“β€˜(𝑛 + 1)) ∈ 𝐴)
146 fzp1nel 13587 . . . . . . . . . . . . . 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 7264 . . . . . . . . . . . . . . 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 3959 . . . . . . . . . . . 12 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (π‘“β€˜(𝑛 + 1)) ∈ (𝐴 βˆ– (𝑓 β€œ (1...𝑛))))
153120, 143, 152rspcdva 3613 . . . . . . . . . . 11 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (πΉβ€˜(π‘“β€˜(𝑛 + 1))) ∈ (π‘β€˜{(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))}))
154118, 153eqeltrd 2833 . . . . . . . . . 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 6758 . . . . . . . . . . . . 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 6006 . . . . . . . . . . . . . . 15 (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) βŠ† 𝐻
162161rnssi 5939 . . . . . . . . . . . . . 14 ran (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) βŠ† ran 𝐻
163155cntzidss 19206 . . . . . . . . . . . . . 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 2844 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ 𝑛 ∈ β„•)
166 f1ores 6847 . . . . . . . . . . . . . . 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 6832 . . . . . . . . . . . . . 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 8164 . . . . . . . . . . . . . . 15 ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) supp 0 ) βŠ† dom (𝐻 β†Ύ (𝑓 β€œ (1...𝑛)))
171 dmres 6003 . . . . . . . . . . . . . . . 16 dom (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) = ((𝑓 β€œ (1...𝑛)) ∩ dom 𝐻)
172171a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ dom (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) = ((𝑓 β€œ (1...𝑛)) ∩ dom 𝐻))
173170, 172sseqtrid 4034 . . . . . . . . . . . . . 14 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) supp 0 ) βŠ† ((𝑓 β€œ (1...𝑛)) ∩ dom 𝐻))
174 inss1 4228 . . . . . . . . . . . . . . 15 ((𝑓 β€œ (1...𝑛)) ∩ dom 𝐻) βŠ† (𝑓 β€œ (1...𝑛))
175 df-ima 5689 . . . . . . . . . . . . . . . 16 (𝑓 β€œ (1...𝑛)) = ran (𝑓 β†Ύ (1...𝑛))
176175a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (𝑓 β€œ (1...𝑛)) = ran (𝑓 β†Ύ (1...𝑛)))
177174, 176sseqtrid 4034 . . . . . . . . . . . . . 14 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((𝑓 β€œ (1...𝑛)) ∩ dom 𝐻) βŠ† ran (𝑓 β†Ύ (1...𝑛)))
178173, 177sstrd 3992 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) supp 0 ) βŠ† ran (𝑓 β†Ύ (1...𝑛)))
179 eqid 2732 . . . . . . . . . . . . 13 (((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))) supp 0 ) = (((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))) supp 0 )
1802, 3, 6, 155, 95, 156, 158, 164, 165, 169, 178, 179gsumval3 19777 . . . . . . . . . . . 12 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛)))) = (seq1( + , ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))))β€˜π‘›))
181175eqimss2i 4043 . . . . . . . . . . . . . . . . . 18 ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝑓 β€œ (1...𝑛))
182 cores 6248 . . . . . . . . . . . . . . . . . 18 (ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝑓 β€œ (1...𝑛)) β†’ ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))) = (𝐻 ∘ (𝑓 β†Ύ (1...𝑛))))
183181, 182ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))) = (𝐻 ∘ (𝑓 β†Ύ (1...𝑛)))
184 resco 6249 . . . . . . . . . . . . . . . . 17 ((𝐻 ∘ 𝑓) β†Ύ (1...𝑛)) = (𝐻 ∘ (𝑓 β†Ύ (1...𝑛)))
185183, 184eqtr4i 2763 . . . . . . . . . . . . . . . 16 ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))) = ((𝐻 ∘ 𝑓) β†Ύ (1...𝑛))
186185fveq1i 6892 . . . . . . . . . . . . . . 15 (((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛)))β€˜π‘˜) = (((𝐻 ∘ 𝑓) β†Ύ (1...𝑛))β€˜π‘˜)
187 fvres 6910 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (1...𝑛) β†’ (((𝐻 ∘ 𝑓) β†Ύ (1...𝑛))β€˜π‘˜) = ((𝐻 ∘ 𝑓)β€˜π‘˜))
188186, 187eqtrid 2784 . . . . . . . . . . . . . 14 (π‘˜ ∈ (1...𝑛) β†’ (((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛)))β€˜π‘˜) = ((𝐻 ∘ 𝑓)β€˜π‘˜))
189188adantl 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛)))β€˜π‘˜) = ((𝐻 ∘ 𝑓)β€˜π‘˜))
19097, 189seqfveq 13994 . . . . . . . . . . . 12 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (seq1( + , ((𝐻 β†Ύ (𝑓 β€œ (1...𝑛))) ∘ (𝑓 β†Ύ (1...𝑛))))β€˜π‘›) = (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›))
191180, 190eqtr2d 2773 . . . . . . . . . . 11 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) = (𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛)))))
192 fvex 6904 . . . . . . . . . . . 12 (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) ∈ V
193192elsn 4643 . . . . . . . . . . 11 ((seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) ∈ {(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))} ↔ (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) = (𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛)))))
194191, 193sylibr 233 . . . . . . . . . 10 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) ∈ {(𝐺 Ξ£g (𝐻 β†Ύ (𝑓 β€œ (1...𝑛))))})
1956, 155cntzi 19195 . . . . . . . . . 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 2738 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ ((seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) + ((𝐹 ∘ 𝑓)β€˜(𝑛 + 1))) = (((𝐹 ∘ 𝑓)β€˜(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›)))
1982, 6, 95, 108, 111, 114, 116, 197mnd4g 18641 . . . . . . 7 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ 𝑛 ∈ (1..^(β™―β€˜π‘Š))) β†’ (((seq1( + , (𝐹 ∘ 𝑓))β€˜π‘›) + (seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›)) + (((𝐹 ∘ 𝑓)β€˜(𝑛 + 1)) + ((𝐻 ∘ 𝑓)β€˜(𝑛 + 1)))) = (((seq1( + , (𝐹 ∘ 𝑓))β€˜π‘›) + ((𝐹 ∘ 𝑓)β€˜(𝑛 + 1))) + ((seq1( + , (𝐻 ∘ 𝑓))β€˜π‘›) + ((𝐻 ∘ 𝑓)β€˜(𝑛 + 1)))))
19948, 48, 51, 73, 77, 94, 198seqcaopr3 14005 . . . . . 6 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (seq1( + , ((𝐹 ∘f + 𝐻) ∘ 𝑓))β€˜(β™―β€˜π‘Š)) = ((seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜π‘Š)) + (seq1( + , (𝐻 ∘ 𝑓))β€˜(β™―β€˜π‘Š))))
20047, 52, 74, 80, 80, 82off 7690 . . . . . . 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 7690 . . . . . . . 8 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐹 ∘f + 𝐻):𝐴⟢𝐡)
205 eldifi 4126 . . . . . . . . . 10 (π‘₯ ∈ (𝐴 βˆ– ran 𝑓) β†’ π‘₯ ∈ 𝐴)
206 eqidd 2733 . . . . . . . . . . 11 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘₯))
207 eqidd 2733 . . . . . . . . . . 11 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ 𝐴) β†’ (π»β€˜π‘₯) = (π»β€˜π‘₯))
20878, 79, 80, 80, 82, 206, 207ofval 7683 . . . . . . . . . 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 6840 . . . . . . . . . . . . . . . 16 (𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š β†’ 𝑓:(1...(β™―β€˜π‘Š))–ontoβ†’π‘Š)
212 forn 6808 . . . . . . . . . . . . . . . 16 (𝑓:(1...(β™―β€˜π‘Š))–ontoβ†’π‘Š β†’ ran 𝑓 = π‘Š)
213211, 212syl 17 . . . . . . . . . . . . . . 15 (𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š β†’ ran 𝑓 = π‘Š)
214213, 17eqtrdi 2788 . . . . . . . . . . . . . 14 (𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š β†’ ran 𝑓 = ((𝐹 βˆͺ 𝐻) supp 0 ))
215214sseq2d 4014 . . . . . . . . . . . . 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 8183 . . . . . . . . . 10 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝑓)) β†’ (πΉβ€˜π‘₯) = 0 )
22026adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐻 supp 0 ) βŠ† ((𝐻 βˆͺ 𝐹) supp 0 ))
221220, 28sseqtrrdi 4033 . . . . . . . . . . . 12 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐻 supp 0 ) βŠ† ((𝐹 βˆͺ 𝐻) supp 0 ))
222214sseq2d 4014 . . . . . . . . . . . . 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 8183 . . . . . . . . . 10 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝑓)) β†’ (π»β€˜π‘₯) = 0 )
226219, 225oveq12d 7429 . . . . . . . . 9 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝑓)) β†’ ((πΉβ€˜π‘₯) + (π»β€˜π‘₯)) = ( 0 + 0 ))
2278ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝑓)) β†’ ( 0 + 0 ) = 0 )
228209, 226, 2273eqtrd 2776 . . . . . . . 8 (((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝑓)) β†’ ((𝐹 ∘f + 𝐻)β€˜π‘₯) = 0 )
229204, 228suppss 8181 . . . . . . 7 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ ((𝐹 ∘f + 𝐻) supp 0 ) βŠ† ran 𝑓)
230 ovex 7444 . . . . . . . . 9 (𝐹 ∘f + 𝐻) ∈ V
231230, 131coex 7923 . . . . . . . 8 ((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V
232 suppimacnv 8161 . . . . . . . . 9 ((((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) β†’ (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 ) = (β—‘((𝐹 ∘f + 𝐻) ∘ 𝑓) β€œ (V βˆ– { 0 })))
233232eqcomd 2738 . . . . . . . 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 19777 . . . . . 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 2732 . . . . . . . 8 ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 )
2392, 3, 6, 155, 44, 80, 52, 237, 49, 68, 217, 238gsumval3 19777 . . . . . . 7 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜π‘Š)))
240159adantr 481 . . . . . . . 8 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ ran 𝐻 βŠ† (π‘β€˜ran 𝐻))
241 eqid 2732 . . . . . . . 8 ((𝐻 ∘ 𝑓) supp 0 ) = ((𝐻 ∘ 𝑓) supp 0 )
2422, 3, 6, 155, 44, 80, 74, 240, 49, 68, 224, 241gsumval3 19777 . . . . . . 7 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ (𝐺 Ξ£g 𝐻) = (seq1( + , (𝐻 ∘ 𝑓))β€˜(β™―β€˜π‘Š)))
243239, 242oveq12d 7429 . . . . . 6 ((πœ‘ ∧ ((β™―β€˜π‘Š) ∈ β„• ∧ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)) β†’ ((𝐺 Ξ£g 𝐹) + (𝐺 Ξ£g 𝐻)) = ((seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜π‘Š)) + (seq1( + , (𝐻 ∘ 𝑓))β€˜(β™―β€˜π‘Š))))
244199, 235, 2433eqtr4d 2782 . . . . 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 9384 . . . 4 (πœ‘ β†’ ((𝐹 βˆͺ 𝐻) supp 0 ) ∈ Fin)
25117, 250eqeltrid 2837 . . 3 (πœ‘ β†’ π‘Š ∈ Fin)
252 fz1f1o 15658 . . 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 3061  Vcvv 3474   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628   class class class wbr 5148   ↦ cmpt 5231  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   ∘ ccom 5680   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“ontoβ†’wfo 6541  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7411   ∘f cof 7670   supp csupp 8148  Fincfn 8941   finSupp cfsupp 9363  1c1 11113   + caddc 11115  β„•cn 12214  β„€β‰₯cuz 12824  ...cfz 13486  ..^cfzo 13629  seqcseq 13968  β™―chash 14292  Basecbs 17146  +gcplusg 17199  0gc0g 17387   Ξ£g cgsu 17388  Mndcmnd 18627  Cntzccntz 19181
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-n0 12475  df-z 12561  df-uz 12825  df-fz 13487  df-fzo 13630  df-seq 13969  df-hash 14293  df-0g 17389  df-gsum 17390  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-cntz 19183
This theorem is referenced by:  gsumzadd  19792  dprdfadd  19892
  Copyright terms: Public domain W3C validator