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

Theorem gsumval3 19689
Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.)
Hypotheses
Ref Expression
gsumval3.b 𝐡 = (Baseβ€˜πΊ)
gsumval3.0 0 = (0gβ€˜πΊ)
gsumval3.p + = (+gβ€˜πΊ)
gsumval3.z 𝑍 = (Cntzβ€˜πΊ)
gsumval3.g (πœ‘ β†’ 𝐺 ∈ Mnd)
gsumval3.a (πœ‘ β†’ 𝐴 ∈ 𝑉)
gsumval3.f (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
gsumval3.c (πœ‘ β†’ ran 𝐹 βŠ† (π‘β€˜ran 𝐹))
gsumval3.m (πœ‘ β†’ 𝑀 ∈ β„•)
gsumval3.h (πœ‘ β†’ 𝐻:(1...𝑀)–1-1→𝐴)
gsumval3.n (πœ‘ β†’ (𝐹 supp 0 ) βŠ† ran 𝐻)
gsumval3.w π‘Š = ((𝐹 ∘ 𝐻) supp 0 )
Assertion
Ref Expression
gsumval3 (πœ‘ β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))

Proof of Theorem gsumval3
Dummy variables 𝑓 π‘˜ π‘š 𝑛 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumval3.g . . . . 5 (πœ‘ β†’ 𝐺 ∈ Mnd)
2 gsumval3.a . . . . 5 (πœ‘ β†’ 𝐴 ∈ 𝑉)
3 gsumval3.0 . . . . . 6 0 = (0gβ€˜πΊ)
43gsumz 18651 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
51, 2, 4syl2anc 585 . . . 4 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
65adantr 482 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
7 gsumval3.f . . . . . . 7 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
87feqmptd 6911 . . . . . 6 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)))
98adantr 482 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)))
10 gsumval3.h . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐻:(1...𝑀)–1-1→𝐴)
11 f1f 6739 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1→𝐴 β†’ 𝐻:(1...𝑀)⟢𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐻:(1...𝑀)⟢𝐴)
1312ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ 𝐻:(1...𝑀)⟢𝐴)
14 f1f1orn 6796 . . . . . . . . . . . . . . . 16 (𝐻:(1...𝑀)–1-1→𝐴 β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
1510, 14syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
1615adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
17 f1ocnv 6797 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ ◑𝐻:ran 𝐻–1-1-ontoβ†’(1...𝑀))
18 f1of 6785 . . . . . . . . . . . . . 14 (◑𝐻:ran 𝐻–1-1-ontoβ†’(1...𝑀) β†’ ◑𝐻:ran 𝐻⟢(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ◑𝐻:ran 𝐻⟢(1...𝑀))
2019ffvelcdmda 7036 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (β—‘π»β€˜π‘₯) ∈ (1...𝑀))
21 fvco3 6941 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟢𝐴 ∧ (β—‘π»β€˜π‘₯) ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = (πΉβ€˜(π»β€˜(β—‘π»β€˜π‘₯))))
2213, 20, 21syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = (πΉβ€˜(π»β€˜(β—‘π»β€˜π‘₯))))
23 simpr 486 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Š = βˆ…) β†’ π‘Š = βˆ…)
2423difeq2d 4083 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((1...𝑀) βˆ– π‘Š) = ((1...𝑀) βˆ– βˆ…))
25 dif0 4333 . . . . . . . . . . . . . . 15 ((1...𝑀) βˆ– βˆ…) = (1...𝑀)
2624, 25eqtrdi 2789 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((1...𝑀) βˆ– π‘Š) = (1...𝑀))
2726adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ ((1...𝑀) βˆ– π‘Š) = (1...𝑀))
2820, 27eleqtrrd 2837 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (β—‘π»β€˜π‘₯) ∈ ((1...𝑀) βˆ– π‘Š))
29 fco 6693 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟢𝐡 ∧ 𝐻:(1...𝑀)⟢𝐴) β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
307, 12, 29syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
3130adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
32 gsumval3.w . . . . . . . . . . . . . . 15 π‘Š = ((𝐹 ∘ 𝐻) supp 0 )
3332eqimss2i 4004 . . . . . . . . . . . . . 14 ((𝐹 ∘ 𝐻) supp 0 ) βŠ† π‘Š
3433a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((𝐹 ∘ 𝐻) supp 0 ) βŠ† π‘Š)
35 ovexd 7393 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (1...𝑀) ∈ V)
363fvexi 6857 . . . . . . . . . . . . . 14 0 ∈ V
3736a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 0 ∈ V)
3831, 34, 35, 37suppssr 8128 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ (β—‘π»β€˜π‘₯) ∈ ((1...𝑀) βˆ– π‘Š)) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = 0 )
3928, 38syldan 592 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = 0 )
40 f1ocnvfv2 7224 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻 ∧ π‘₯ ∈ ran 𝐻) β†’ (π»β€˜(β—‘π»β€˜π‘₯)) = π‘₯)
4116, 40sylan 581 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (π»β€˜(β—‘π»β€˜π‘₯)) = π‘₯)
4241fveq2d 6847 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜(π»β€˜(β—‘π»β€˜π‘₯))) = (πΉβ€˜π‘₯))
4322, 39, 423eqtr3rd 2782 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) = 0 )
44 fvex 6856 . . . . . . . . . . 11 (πΉβ€˜π‘₯) ∈ V
4544elsn 4602 . . . . . . . . . 10 ((πΉβ€˜π‘₯) ∈ { 0 } ↔ (πΉβ€˜π‘₯) = 0 )
4643, 45sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
4746adantlr 714 . . . . . . . 8 ((((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
48 eldif 3921 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴 βˆ– ran 𝐻) ↔ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ ran 𝐻))
49 gsumval3.n . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 supp 0 ) βŠ† ran 𝐻)
5036a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ V)
517, 49, 2, 50suppssr 8128 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) = 0 )
5251, 45sylibr 233 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5348, 52sylan2br 596 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ ran 𝐻)) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5453adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ π‘Š = βˆ…) ∧ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ ran 𝐻)) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5554anassrs 469 . . . . . . . 8 ((((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5647, 55pm2.61dan 812 . . . . . . 7 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5756, 45sylib 217 . . . . . 6 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) = 0 )
5857mpteq2dva 5206 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐴 ↦ 0 ))
599, 58eqtrd 2773 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ 0 ))
6059oveq2d 7374 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )))
61 gsumval3.b . . . . . . 7 𝐡 = (Baseβ€˜πΊ)
6261, 3mndidcl 18576 . . . . . 6 (𝐺 ∈ Mnd β†’ 0 ∈ 𝐡)
63 gsumval3.p . . . . . . 7 + = (+gβ€˜πΊ)
6461, 63, 3mndlid 18581 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐡) β†’ ( 0 + 0 ) = 0 )
651, 62, 64syl2anc2 586 . . . . 5 (πœ‘ β†’ ( 0 + 0 ) = 0 )
6665adantr 482 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ( 0 + 0 ) = 0 )
67 gsumval3.m . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•)
68 nnuz 12811 . . . . . 6 β„• = (β„€β‰₯β€˜1)
6967, 68eleqtrdi 2844 . . . . 5 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
7069adantr 482 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
7126eleq2d 2820 . . . . . 6 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (π‘₯ ∈ ((1...𝑀) βˆ– π‘Š) ↔ π‘₯ ∈ (1...𝑀)))
7271biimpar 479 . . . . 5 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ (1...𝑀)) β†’ π‘₯ ∈ ((1...𝑀) βˆ– π‘Š))
7331, 34, 35, 37suppssr 8128 . . . . 5 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ((1...𝑀) βˆ– π‘Š)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) = 0 )
7472, 73syldan 592 . . . 4 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) = 0 )
7566, 70, 74seqid3 13958 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = 0 )
766, 60, 753eqtr4d 2783 . 2 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
77 fzf 13434 . . . . 5 ...:(β„€ Γ— β„€)βŸΆπ’« β„€
78 ffn 6669 . . . . 5 (...:(β„€ Γ— β„€)βŸΆπ’« β„€ β†’ ... Fn (β„€ Γ— β„€))
79 ovelrn 7531 . . . . 5 (... Fn (β„€ Γ— β„€) β†’ (𝐴 ∈ ran ... ↔ βˆƒπ‘š ∈ β„€ βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛)))
8077, 78, 79mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ βˆƒπ‘š ∈ β„€ βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛))
811ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐺 ∈ Mnd)
82 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐴 = (π‘š...𝑛))
83 frel 6674 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴⟢𝐡 β†’ Rel 𝐹)
84 reldm0 5884 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 β†’ (𝐹 = βˆ… ↔ dom 𝐹 = βˆ…))
857, 83, 843syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐹 = βˆ… ↔ dom 𝐹 = βˆ…))
867fdmd 6680 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom 𝐹 = 𝐴)
8786eqeq1d 2735 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (dom 𝐹 = βˆ… ↔ 𝐴 = βˆ…))
8885, 87bitrd 279 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐹 = βˆ… ↔ 𝐴 = βˆ…))
89 coeq1 5814 . . . . . . . . . . . . . . . . . . 19 (𝐹 = βˆ… β†’ (𝐹 ∘ 𝐻) = (βˆ… ∘ 𝐻))
90 co01 6214 . . . . . . . . . . . . . . . . . . 19 (βˆ… ∘ 𝐻) = βˆ…
9189, 90eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (𝐹 = βˆ… β†’ (𝐹 ∘ 𝐻) = βˆ…)
9291oveq1d 7373 . . . . . . . . . . . . . . . . 17 (𝐹 = βˆ… β†’ ((𝐹 ∘ 𝐻) supp 0 ) = (βˆ… supp 0 ))
93 supp0 8098 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V β†’ (βˆ… supp 0 ) = βˆ…)
9436, 93ax-mp 5 . . . . . . . . . . . . . . . . 17 (βˆ… supp 0 ) = βˆ…
9592, 94eqtrdi 2789 . . . . . . . . . . . . . . . 16 (𝐹 = βˆ… β†’ ((𝐹 ∘ 𝐻) supp 0 ) = βˆ…)
9632, 95eqtrid 2785 . . . . . . . . . . . . . . 15 (𝐹 = βˆ… β†’ π‘Š = βˆ…)
9788, 96syl6bir 254 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐴 = βˆ… β†’ π‘Š = βˆ…))
9897necon3d 2961 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Š β‰  βˆ… β†’ 𝐴 β‰  βˆ…))
9998imp 408 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ 𝐴 β‰  βˆ…)
10099adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐴 β‰  βˆ…)
10182, 100eqnetrrd 3009 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (π‘š...𝑛) β‰  βˆ…)
102 fzn0 13461 . . . . . . . . . 10 ((π‘š...𝑛) β‰  βˆ… ↔ 𝑛 ∈ (β„€β‰₯β€˜π‘š))
103101, 102sylib 217 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝑛 ∈ (β„€β‰₯β€˜π‘š))
1047ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐹:𝐴⟢𝐡)
10582feq2d 6655 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹:(π‘š...𝑛)⟢𝐡))
106104, 105mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐹:(π‘š...𝑛)⟢𝐡)
10761, 63, 81, 103, 106gsumval2 18546 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝐺 Ξ£g 𝐹) = (seqπ‘š( + , 𝐹)β€˜π‘›))
108 frn 6676 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟢𝐴 β†’ ran 𝐻 βŠ† 𝐴)
10910, 11, 1083syl 18 . . . . . . . . . . . . . 14 (πœ‘ β†’ ran 𝐻 βŠ† 𝐴)
110109ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 βŠ† 𝐴)
111110, 82sseqtrd 3985 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 βŠ† (π‘š...𝑛))
112 fzssuz 13488 . . . . . . . . . . . . 13 (π‘š...𝑛) βŠ† (β„€β‰₯β€˜π‘š)
113 uzssz 12789 . . . . . . . . . . . . . 14 (β„€β‰₯β€˜π‘š) βŠ† β„€
114 zssre 12511 . . . . . . . . . . . . . 14 β„€ βŠ† ℝ
115113, 114sstri 3954 . . . . . . . . . . . . 13 (β„€β‰₯β€˜π‘š) βŠ† ℝ
116112, 115sstri 3954 . . . . . . . . . . . 12 (π‘š...𝑛) βŠ† ℝ
117111, 116sstrdi 3957 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 βŠ† ℝ)
118 ltso 11240 . . . . . . . . . . 11 < Or ℝ
119 soss 5566 . . . . . . . . . . 11 (ran 𝐻 βŠ† ℝ β†’ ( < Or ℝ β†’ < Or ran 𝐻))
120117, 118, 119mpisyl 21 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ < Or ran 𝐻)
121 fzfi 13883 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
122121a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1...𝑀) ∈ Fin)
12312, 122fexd 7178 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐻 ∈ V)
124 f1oen3g 8909 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻) β†’ (1...𝑀) β‰ˆ ran 𝐻)
125123, 15, 124syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (1...𝑀) β‰ˆ ran 𝐻)
126 enfi 9137 . . . . . . . . . . . . 13 ((1...𝑀) β‰ˆ ran 𝐻 β†’ ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
127125, 126syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
128121, 127mpbii 232 . . . . . . . . . . 11 (πœ‘ β†’ ran 𝐻 ∈ Fin)
129128ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 ∈ Fin)
130 fz1iso 14367 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))
131120, 129, 130syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))
13267nnnn0d 12478 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑀 ∈ β„•0)
133 hashfz1 14252 . . . . . . . . . . . . . . . 16 (𝑀 ∈ β„•0 β†’ (β™―β€˜(1...𝑀)) = 𝑀)
134132, 133syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = 𝑀)
135122, 15hasheqf1od 14259 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = (β™―β€˜ran 𝐻))
136134, 135eqtr3d 2775 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 = (β™―β€˜ran 𝐻))
137136ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑀 = (β™―β€˜ran 𝐻))
138137fveq2d 6847 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seq1( + , (𝐹 ∘ 𝑓))β€˜π‘€) = (seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜ran 𝐻)))
1391ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐺 ∈ Mnd)
14061, 63mndcl 18569 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
1411403expb 1121 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
142139, 141sylan 581 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
143 gsumval3.c . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝐹 βŠ† (π‘β€˜ran 𝐹))
144143ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐹 βŠ† (π‘β€˜ran 𝐹))
145144sselda 3945 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ran 𝐹) β†’ π‘₯ ∈ (π‘β€˜ran 𝐹))
146 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntzβ€˜πΊ)
14763, 146cntzi 19114 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (π‘β€˜ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) β†’ (π‘₯ + 𝑦) = (𝑦 + π‘₯))
148145, 147sylan 581 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) β†’ (π‘₯ + 𝑦) = (𝑦 + π‘₯))
149148anasss 468 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ (π‘₯ ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) β†’ (π‘₯ + 𝑦) = (𝑦 + π‘₯))
15061, 63mndass 18570 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯ + 𝑦) + 𝑧) = (π‘₯ + (𝑦 + 𝑧)))
151139, 150sylan 581 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯ + 𝑦) + 𝑧) = (π‘₯ + (𝑦 + 𝑧)))
15269ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
1537ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐹:𝐴⟢𝐡)
154153frnd 6677 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐹 βŠ† 𝐡)
155 simprr 772 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))
156 isof1o 7269 . . . . . . . . . . . . . . . . 17 (𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻) β†’ 𝑓:(1...(β™―β€˜ran 𝐻))–1-1-ontoβ†’ran 𝐻)
157155, 156syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...(β™―β€˜ran 𝐻))–1-1-ontoβ†’ran 𝐻)
158137oveq2d 7374 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (1...𝑀) = (1...(β™―β€˜ran 𝐻)))
159158f1oeq2d 6781 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 ↔ 𝑓:(1...(β™―β€˜ran 𝐻))–1-1-ontoβ†’ran 𝐻))
160157, 159mpbird 257 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
161 f1ocnv 6797 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ ◑𝑓:ran 𝐻–1-1-ontoβ†’(1...𝑀))
162160, 161syl 17 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ◑𝑓:ran 𝐻–1-1-ontoβ†’(1...𝑀))
16315ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
164 f1oco 6808 . . . . . . . . . . . . . 14 ((◑𝑓:ran 𝐻–1-1-ontoβ†’(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)–1-1-ontoβ†’(1...𝑀))
165162, 163, 164syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)–1-1-ontoβ†’(1...𝑀))
166 ffn 6669 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴⟢𝐡 β†’ 𝐹 Fn 𝐴)
167 dffn4 6763 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–ontoβ†’ran 𝐹)
168166, 167sylib 217 . . . . . . . . . . . . . . . 16 (𝐹:𝐴⟢𝐡 β†’ 𝐹:𝐴–ontoβ†’ran 𝐹)
169 fof 6757 . . . . . . . . . . . . . . . 16 (𝐹:𝐴–ontoβ†’ran 𝐹 β†’ 𝐹:𝐴⟢ran 𝐹)
170153, 168, 1693syl 18 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐹:𝐴⟢ran 𝐹)
171 f1of 6785 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ 𝑓:(1...𝑀)⟢ran 𝐻)
172160, 171syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...𝑀)⟢ran 𝐻)
173109ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐻 βŠ† 𝐴)
174172, 173fssd 6687 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...𝑀)⟢𝐴)
175 fco 6693 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟢ran 𝐹 ∧ 𝑓:(1...𝑀)⟢𝐴) β†’ (𝐹 ∘ 𝑓):(1...𝑀)⟢ran 𝐹)
176170, 174, 175syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐹 ∘ 𝑓):(1...𝑀)⟢ran 𝐹)
177176ffvelcdmda 7036 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝑓)β€˜π‘₯) ∈ ran 𝐹)
178 f1ococnv2 6812 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ (𝑓 ∘ ◑𝑓) = ( I β†Ύ ran 𝐻))
179160, 178syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝑓 ∘ ◑𝑓) = ( I β†Ύ ran 𝐻))
180179coeq1d 5818 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ((𝑓 ∘ ◑𝑓) ∘ 𝐻) = (( I β†Ύ ran 𝐻) ∘ 𝐻))
181 f1of 6785 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ 𝐻:(1...𝑀)⟢ran 𝐻)
182 fcoi2 6718 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟢ran 𝐻 β†’ (( I β†Ύ ran 𝐻) ∘ 𝐻) = 𝐻)
183163, 181, 1823syl 18 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (( I β†Ύ ran 𝐻) ∘ 𝐻) = 𝐻)
184180, 183eqtr2d 2774 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻 = ((𝑓 ∘ ◑𝑓) ∘ 𝐻))
185 coass 6218 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∘ ◑𝑓) ∘ 𝐻) = (𝑓 ∘ (◑𝑓 ∘ 𝐻))
186184, 185eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻 = (𝑓 ∘ (◑𝑓 ∘ 𝐻)))
187186coeq2d 5819 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◑𝑓 ∘ 𝐻))))
188 coass 6218 . . . . . . . . . . . . . . . . 17 ((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◑𝑓 ∘ 𝐻)))
189187, 188eqtr4di 2791 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻)))
190189fveq1d 6845 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ((𝐹 ∘ 𝐻)β€˜π‘˜) = (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜))
191190adantr 482 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘˜) = (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜))
192 f1of 6785 . . . . . . . . . . . . . . . . 17 (◑𝑓:ran 𝐻–1-1-ontoβ†’(1...𝑀) β†’ ◑𝑓:ran 𝐻⟢(1...𝑀))
193160, 161, 1923syl 18 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ◑𝑓:ran 𝐻⟢(1...𝑀))
194163, 181syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻:(1...𝑀)⟢ran 𝐻)
195 fco 6693 . . . . . . . . . . . . . . . 16 ((◑𝑓:ran 𝐻⟢(1...𝑀) ∧ 𝐻:(1...𝑀)⟢ran 𝐻) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)⟢(1...𝑀))
196193, 194, 195syl2anc 585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)⟢(1...𝑀))
197 fvco3 6941 . . . . . . . . . . . . . . 15 (((◑𝑓 ∘ 𝐻):(1...𝑀)⟢(1...𝑀) ∧ π‘˜ ∈ (1...𝑀)) β†’ (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜((◑𝑓 ∘ 𝐻)β€˜π‘˜)))
198196, 197sylan 581 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘˜ ∈ (1...𝑀)) β†’ (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜((◑𝑓 ∘ 𝐻)β€˜π‘˜)))
199191, 198eqtrd 2773 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜((◑𝑓 ∘ 𝐻)β€˜π‘˜)))
200142, 149, 151, 152, 154, 165, 177, 199seqf1o 13955 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seq1( + , (𝐹 ∘ 𝑓))β€˜π‘€))
20161, 63, 3mndlid 18581 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ π‘₯ ∈ 𝐡) β†’ ( 0 + π‘₯) = π‘₯)
202139, 201sylan 581 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ 𝐡) β†’ ( 0 + π‘₯) = π‘₯)
20361, 63, 3mndrid 18582 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ + 0 ) = π‘₯)
204139, 203sylan 581 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ + 0 ) = π‘₯)
205139, 62syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 0 ∈ 𝐡)
206 fdm 6678 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟢𝐴 β†’ dom 𝐻 = (1...𝑀))
20710, 11, 2063syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom 𝐻 = (1...𝑀))
208 eluzfz1 13454 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝑀))
209 ne0i 4295 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) β†’ (1...𝑀) β‰  βˆ…)
21069, 208, 2093syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (1...𝑀) β‰  βˆ…)
211207, 210eqnetrd 3008 . . . . . . . . . . . . . . 15 (πœ‘ β†’ dom 𝐻 β‰  βˆ…)
212 dm0rn0 5881 . . . . . . . . . . . . . . . 16 (dom 𝐻 = βˆ… ↔ ran 𝐻 = βˆ…)
213212necon3bii 2993 . . . . . . . . . . . . . . 15 (dom 𝐻 β‰  βˆ… ↔ ran 𝐻 β‰  βˆ…)
214211, 213sylib 217 . . . . . . . . . . . . . 14 (πœ‘ β†’ ran 𝐻 β‰  βˆ…)
215214ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐻 β‰  βˆ…)
216111adantrr 716 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐻 βŠ† (π‘š...𝑛))
217 simprl 770 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐴 = (π‘š...𝑛))
218217eleq2d 2820 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ (π‘š...𝑛)))
219218biimpar 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (π‘š...𝑛)) β†’ π‘₯ ∈ 𝐴)
220153ffvelcdmda 7036 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ 𝐡)
221219, 220syldan 592 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (π‘š...𝑛)) β†’ (πΉβ€˜π‘₯) ∈ 𝐡)
222217difeq1d 4082 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐴 βˆ– ran 𝐻) = ((π‘š...𝑛) βˆ– ran 𝐻))
223222eleq2d 2820 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (π‘₯ ∈ (𝐴 βˆ– ran 𝐻) ↔ π‘₯ ∈ ((π‘š...𝑛) βˆ– ran 𝐻)))
224223biimpar 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ((π‘š...𝑛) βˆ– ran 𝐻)) β†’ π‘₯ ∈ (𝐴 βˆ– ran 𝐻))
22551ad4ant14 751 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) = 0 )
226224, 225syldan 592 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ((π‘š...𝑛) βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) = 0 )
227 f1of 6785 . . . . . . . . . . . . . . 15 (𝑓:(1...(β™―β€˜ran 𝐻))–1-1-ontoβ†’ran 𝐻 β†’ 𝑓:(1...(β™―β€˜ran 𝐻))⟢ran 𝐻)
228155, 156, 2273syl 18 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...(β™―β€˜ran 𝐻))⟢ran 𝐻)
229 fvco3 6941 . . . . . . . . . . . . . 14 ((𝑓:(1...(β™―β€˜ran 𝐻))⟢ran 𝐻 ∧ 𝑦 ∈ (1...(β™―β€˜ran 𝐻))) β†’ ((𝐹 ∘ 𝑓)β€˜π‘¦) = (πΉβ€˜(π‘“β€˜π‘¦)))
230228, 229sylan 581 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(β™―β€˜ran 𝐻))) β†’ ((𝐹 ∘ 𝑓)β€˜π‘¦) = (πΉβ€˜(π‘“β€˜π‘¦)))
231202, 204, 142, 205, 155, 215, 216, 221, 226, 230seqcoll2 14370 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seqπ‘š( + , 𝐹)β€˜π‘›) = (seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜ran 𝐻)))
232138, 200, 2313eqtr4d 2783 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›))
233232expr 458 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›)))
234233exlimdv 1937 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›)))
235131, 234mpd 15 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›))
236107, 235eqtr4d 2776 . . . . . . 7 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
237236ex 414 . . . . . 6 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (𝐴 = (π‘š...𝑛) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
238237rexlimdvw 3154 . . . . 5 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
239238rexlimdvw 3154 . . . 4 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (βˆƒπ‘š ∈ β„€ βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
24080, 239biimtrid 241 . . 3 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (𝐴 ∈ ran ... β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
241 suppssdm 8109 . . . . . . . . . . 11 ((𝐹 ∘ 𝐻) supp 0 ) βŠ† dom (𝐹 ∘ 𝐻)
24232, 241eqsstri 3979 . . . . . . . . . 10 π‘Š βŠ† dom (𝐹 ∘ 𝐻)
243242, 30fssdm 6689 . . . . . . . . 9 (πœ‘ β†’ π‘Š βŠ† (1...𝑀))
244 fz1ssnn 13478 . . . . . . . . . 10 (1...𝑀) βŠ† β„•
245 nnssre 12162 . . . . . . . . . 10 β„• βŠ† ℝ
246244, 245sstri 3954 . . . . . . . . 9 (1...𝑀) βŠ† ℝ
247243, 246sstrdi 3957 . . . . . . . 8 (πœ‘ β†’ π‘Š βŠ† ℝ)
248 soss 5566 . . . . . . . 8 (π‘Š βŠ† ℝ β†’ ( < Or ℝ β†’ < Or π‘Š))
249247, 118, 248mpisyl 21 . . . . . . 7 (πœ‘ β†’ < Or π‘Š)
250 ssfi 9120 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ π‘Š βŠ† (1...𝑀)) β†’ π‘Š ∈ Fin)
251121, 243, 250sylancr 588 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ Fin)
252 fz1iso 14367 . . . . . . 7 (( < Or π‘Š ∧ π‘Š ∈ Fin) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
253249, 251, 252syl2anc 585 . . . . . 6 (πœ‘ β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
254253ad2antrr 725 . . . . 5 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
25561, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32gsumval3lem2 19688 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))β€˜(β™―β€˜π‘Š)))
2561ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 𝐺 ∈ Mnd)
257256, 201sylan 581 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ 𝐡) β†’ ( 0 + π‘₯) = π‘₯)
258256, 203sylan 581 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ + 0 ) = π‘₯)
259256, 141sylan 581 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
260256, 62syl 17 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 0 ∈ 𝐡)
261 simprr 772 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
262 simplr 768 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ π‘Š β‰  βˆ…)
263243ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ π‘Š βŠ† (1...𝑀))
26430ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
265264ffvelcdmda 7036 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) ∈ 𝐡)
26633a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ ((𝐹 ∘ 𝐻) supp 0 ) βŠ† π‘Š)
267 ovexd 7393 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (1...𝑀) ∈ V)
26836a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 0 ∈ V)
269264, 266, 267, 268suppssr 8128 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ ((1...𝑀) βˆ– π‘Š)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) = 0 )
270 coass 6218 . . . . . . . . . . 11 ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
271270fveq1i 6844 . . . . . . . . . 10 (((𝐹 ∘ 𝐻) ∘ 𝑓)β€˜π‘¦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))β€˜π‘¦)
272 isof1o 7269 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š) β†’ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)
273 f1of 6785 . . . . . . . . . . . 12 (𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š β†’ 𝑓:(1...(β™―β€˜π‘Š))βŸΆπ‘Š)
274261, 272, 2733syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 𝑓:(1...(β™―β€˜π‘Š))βŸΆπ‘Š)
275 fvco3 6941 . . . . . . . . . . 11 ((𝑓:(1...(β™―β€˜π‘Š))βŸΆπ‘Š ∧ 𝑦 ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘ 𝐻) ∘ 𝑓)β€˜π‘¦) = ((𝐹 ∘ 𝐻)β€˜(π‘“β€˜π‘¦)))
276274, 275sylan 581 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ 𝑦 ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘ 𝐻) ∘ 𝑓)β€˜π‘¦) = ((𝐹 ∘ 𝐻)β€˜(π‘“β€˜π‘¦)))
277271, 276eqtr3id 2787 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ 𝑦 ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ (𝐻 ∘ 𝑓))β€˜π‘¦) = ((𝐹 ∘ 𝐻)β€˜(π‘“β€˜π‘¦)))
278257, 258, 259, 260, 261, 262, 263, 265, 269, 277seqcoll2 14370 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))β€˜(β™―β€˜π‘Š)))
279255, 278eqtr4d 2776 . . . . . . 7 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
280279expr 458 . . . . . 6 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ (𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
281280exlimdv 1937 . . . . 5 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ (βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
282254, 281mpd 15 . . . 4 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
283282ex 414 . . 3 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (Β¬ 𝐴 ∈ ran ... β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
284240, 283pm2.61d 179 . 2 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
28576, 284pm2.61dane 3029 1 (πœ‘ β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2940  βˆƒwrex 3070  Vcvv 3444   βˆ– cdif 3908   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587   class class class wbr 5106   ↦ cmpt 5189   I cid 5531   Or wor 5545   Γ— cxp 5632  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   ∘ ccom 5638  Rel wrel 5639   Fn wfn 6492  βŸΆwf 6493  β€“1-1β†’wf1 6494  β€“ontoβ†’wfo 6495  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497   Isom wiso 6498  (class class class)co 7358   supp csupp 8093   β‰ˆ cen 8883  Fincfn 8886  β„cr 11055  1c1 11057   < clt 11194  β„•cn 12158  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  ...cfz 13430  seqcseq 13912  β™―chash 14236  Basecbs 17088  +gcplusg 17138  0gc0g 17326   Ξ£g cgsu 17327  Mndcmnd 18561  Cntzccntz 19100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-nn 12159  df-n0 12419  df-z 12505  df-uz 12769  df-fz 13431  df-fzo 13574  df-seq 13913  df-hash 14237  df-0g 17328  df-gsum 17329  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-cntz 19102
This theorem is referenced by:  gsumzres  19691  gsumzcl2  19692  gsumzf1o  19694  gsumzaddlem  19703  gsumconst  19716  gsumzmhm  19719  gsumzoppg  19726  gsumfsum  20880  wilthlem3  26435
  Copyright terms: Public domain W3C validator