MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumval3 Structured version   Visualization version   GIF version
Theorem gsumval3 19866
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 18792 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
51, 2, 4syl2anc 582 . . . 4 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
65adantr 479 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )) = 0 )
7 gsumval3.f . . . . . . 7 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
87feqmptd 6962 . . . . . 6 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)))
98adantr 479 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)))
10 gsumval3.h . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐻:(1...𝑀)–1-1→𝐴)
11 f1f 6788 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1→𝐴 β†’ 𝐻:(1...𝑀)⟢𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐻:(1...𝑀)⟢𝐴)
1312ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ 𝐻:(1...𝑀)⟢𝐴)
14 f1f1orn 6845 . . . . . . . . . . . . . . . 16 (𝐻:(1...𝑀)–1-1→𝐴 β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
1510, 14syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
1615adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
17 f1ocnv 6846 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ ◑𝐻:ran 𝐻–1-1-ontoβ†’(1...𝑀))
18 f1of 6834 . . . . . . . . . . . . . 14 (◑𝐻:ran 𝐻–1-1-ontoβ†’(1...𝑀) β†’ ◑𝐻:ran 𝐻⟢(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ◑𝐻:ran 𝐻⟢(1...𝑀))
2019ffvelcdmda 7089 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (β—‘π»β€˜π‘₯) ∈ (1...𝑀))
21 fvco3 6992 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟢𝐴 ∧ (β—‘π»β€˜π‘₯) ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = (πΉβ€˜(π»β€˜(β—‘π»β€˜π‘₯))))
2213, 20, 21syl2anc 582 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = (πΉβ€˜(π»β€˜(β—‘π»β€˜π‘₯))))
23 simpr 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Š = βˆ…) β†’ π‘Š = βˆ…)
2423difeq2d 4114 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((1...𝑀) βˆ– π‘Š) = ((1...𝑀) βˆ– βˆ…))
25 dif0 4368 . . . . . . . . . . . . . . 15 ((1...𝑀) βˆ– βˆ…) = (1...𝑀)
2624, 25eqtrdi 2781 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((1...𝑀) βˆ– π‘Š) = (1...𝑀))
2726adantr 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ ((1...𝑀) βˆ– π‘Š) = (1...𝑀))
2820, 27eleqtrrd 2828 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (β—‘π»β€˜π‘₯) ∈ ((1...𝑀) βˆ– π‘Š))
29 fco 6742 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟢𝐡 ∧ 𝐻:(1...𝑀)⟢𝐴) β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
307, 12, 29syl2anc 582 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
3130adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
32 gsumval3.w . . . . . . . . . . . . . . 15 π‘Š = ((𝐹 ∘ 𝐻) supp 0 )
3332eqimss2i 4034 . . . . . . . . . . . . . 14 ((𝐹 ∘ 𝐻) supp 0 ) βŠ† π‘Š
3433a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ((𝐹 ∘ 𝐻) supp 0 ) βŠ† π‘Š)
35 ovexd 7451 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (1...𝑀) ∈ V)
363fvexi 6906 . . . . . . . . . . . . . 14 0 ∈ V
3736a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 0 ∈ V)
3831, 34, 35, 37suppssr 8199 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ (β—‘π»β€˜π‘₯) ∈ ((1...𝑀) βˆ– π‘Š)) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = 0 )
3928, 38syldan 589 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ ((𝐹 ∘ 𝐻)β€˜(β—‘π»β€˜π‘₯)) = 0 )
40 f1ocnvfv2 7282 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻 ∧ π‘₯ ∈ ran 𝐻) β†’ (π»β€˜(β—‘π»β€˜π‘₯)) = π‘₯)
4116, 40sylan 578 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (π»β€˜(β—‘π»β€˜π‘₯)) = π‘₯)
4241fveq2d 6896 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜(π»β€˜(β—‘π»β€˜π‘₯))) = (πΉβ€˜π‘₯))
4322, 39, 423eqtr3rd 2774 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) = 0 )
44 fvex 6905 . . . . . . . . . . 11 (πΉβ€˜π‘₯) ∈ V
4544elsn 4639 . . . . . . . . . 10 ((πΉβ€˜π‘₯) ∈ { 0 } ↔ (πΉβ€˜π‘₯) = 0 )
4643, 45sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
4746adantlr 713 . . . . . . . 8 ((((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) ∧ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
48 eldif 3949 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴 βˆ– ran 𝐻) ↔ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ ran 𝐻))
49 gsumval3.n . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 supp 0 ) βŠ† ran 𝐻)
5036a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ V)
517, 49, 2, 50suppssr 8199 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) = 0 )
5251, 45sylibr 233 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5348, 52sylan2br 593 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ ran 𝐻)) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5453adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ π‘Š = βˆ…) ∧ (π‘₯ ∈ 𝐴 ∧ Β¬ π‘₯ ∈ ran 𝐻)) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5554anassrs 466 . . . . . . . 8 ((((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) ∧ Β¬ π‘₯ ∈ ran 𝐻) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5647, 55pm2.61dan 811 . . . . . . 7 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ { 0 })
5756, 45sylib 217 . . . . . 6 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) = 0 )
5857mpteq2dva 5243 . . . . 5 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐴 ↦ 0 ))
599, 58eqtrd 2765 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ 0 ))
6059oveq2d 7432 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (𝐺 Ξ£g (π‘₯ ∈ 𝐴 ↦ 0 )))
61 gsumval3.b . . . . . . 7 𝐡 = (Baseβ€˜πΊ)
6261, 3mndidcl 18708 . . . . . 6 (𝐺 ∈ Mnd β†’ 0 ∈ 𝐡)
63 gsumval3.p . . . . . . 7 + = (+gβ€˜πΊ)
6461, 63, 3mndlid 18713 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐡) β†’ ( 0 + 0 ) = 0 )
651, 62, 64syl2anc2 583 . . . . 5 (πœ‘ β†’ ( 0 + 0 ) = 0 )
6665adantr 479 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ ( 0 + 0 ) = 0 )
67 gsumval3.m . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•)
68 nnuz 12895 . . . . . 6 β„• = (β„€β‰₯β€˜1)
6967, 68eleqtrdi 2835 . . . . 5 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
7069adantr 479 . . . 4 ((πœ‘ ∧ π‘Š = βˆ…) β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
7126eleq2d 2811 . . . . . 6 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (π‘₯ ∈ ((1...𝑀) βˆ– π‘Š) ↔ π‘₯ ∈ (1...𝑀)))
7271biimpar 476 . . . . 5 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ (1...𝑀)) β†’ π‘₯ ∈ ((1...𝑀) βˆ– π‘Š))
7331, 34, 35, 37suppssr 8199 . . . . 5 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ ((1...𝑀) βˆ– π‘Š)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) = 0 )
7472, 73syldan 589 . . . 4 (((πœ‘ ∧ π‘Š = βˆ…) ∧ π‘₯ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) = 0 )
7566, 70, 74seqid3 14043 . . 3 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = 0 )
766, 60, 753eqtr4d 2775 . 2 ((πœ‘ ∧ π‘Š = βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
77 fzf 13520 . . . . 5 ...:(β„€ Γ— β„€)βŸΆπ’« β„€
78 ffn 6717 . . . . 5 (...:(β„€ Γ— β„€)βŸΆπ’« β„€ β†’ ... Fn (β„€ Γ— β„€))
79 ovelrn 7594 . . . . 5 (... Fn (β„€ Γ— β„€) β†’ (𝐴 ∈ ran ... ↔ βˆƒπ‘š ∈ β„€ βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛)))
8077, 78, 79mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ βˆƒπ‘š ∈ β„€ βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛))
811ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐺 ∈ Mnd)
82 simpr 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐴 = (π‘š...𝑛))
83 frel 6722 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴⟢𝐡 β†’ Rel 𝐹)
84 reldm0 5924 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 β†’ (𝐹 = βˆ… ↔ dom 𝐹 = βˆ…))
857, 83, 843syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐹 = βˆ… ↔ dom 𝐹 = βˆ…))
867fdmd 6728 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom 𝐹 = 𝐴)
8786eqeq1d 2727 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (dom 𝐹 = βˆ… ↔ 𝐴 = βˆ…))
8885, 87bitrd 278 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐹 = βˆ… ↔ 𝐴 = βˆ…))
89 coeq1 5854 . . . . . . . . . . . . . . . . . . 19 (𝐹 = βˆ… β†’ (𝐹 ∘ 𝐻) = (βˆ… ∘ 𝐻))
90 co01 6260 . . . . . . . . . . . . . . . . . . 19 (βˆ… ∘ 𝐻) = βˆ…
9189, 90eqtrdi 2781 . . . . . . . . . . . . . . . . . 18 (𝐹 = βˆ… β†’ (𝐹 ∘ 𝐻) = βˆ…)
9291oveq1d 7431 . . . . . . . . . . . . . . . . 17 (𝐹 = βˆ… β†’ ((𝐹 ∘ 𝐻) supp 0 ) = (βˆ… supp 0 ))
93 supp0 8168 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V β†’ (βˆ… supp 0 ) = βˆ…)
9436, 93ax-mp 5 . . . . . . . . . . . . . . . . 17 (βˆ… supp 0 ) = βˆ…
9592, 94eqtrdi 2781 . . . . . . . . . . . . . . . 16 (𝐹 = βˆ… β†’ ((𝐹 ∘ 𝐻) supp 0 ) = βˆ…)
9632, 95eqtrid 2777 . . . . . . . . . . . . . . 15 (𝐹 = βˆ… β†’ π‘Š = βˆ…)
9788, 96syl6bir 253 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐴 = βˆ… β†’ π‘Š = βˆ…))
9897necon3d 2951 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Š β‰  βˆ… β†’ 𝐴 β‰  βˆ…))
9998imp 405 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ 𝐴 β‰  βˆ…)
10099adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐴 β‰  βˆ…)
10182, 100eqnetrrd 2999 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (π‘š...𝑛) β‰  βˆ…)
102 fzn0 13547 . . . . . . . . . 10 ((π‘š...𝑛) β‰  βˆ… ↔ 𝑛 ∈ (β„€β‰₯β€˜π‘š))
103101, 102sylib 217 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝑛 ∈ (β„€β‰₯β€˜π‘š))
1047ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐹:𝐴⟢𝐡)
10582feq2d 6703 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹:(π‘š...𝑛)⟢𝐡))
106104, 105mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ 𝐹:(π‘š...𝑛)⟢𝐡)
10761, 63, 81, 103, 106gsumval2 18645 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝐺 Ξ£g 𝐹) = (seqπ‘š( + , 𝐹)β€˜π‘›))
108 frn 6724 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟢𝐴 β†’ ran 𝐻 βŠ† 𝐴)
10910, 11, 1083syl 18 . . . . . . . . . . . . . 14 (πœ‘ β†’ ran 𝐻 βŠ† 𝐴)
110109ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 βŠ† 𝐴)
111110, 82sseqtrd 4013 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 βŠ† (π‘š...𝑛))
112 fzssuz 13574 . . . . . . . . . . . . 13 (π‘š...𝑛) βŠ† (β„€β‰₯β€˜π‘š)
113 uzssz 12873 . . . . . . . . . . . . . 14 (β„€β‰₯β€˜π‘š) βŠ† β„€
114 zssre 12595 . . . . . . . . . . . . . 14 β„€ βŠ† ℝ
115113, 114sstri 3982 . . . . . . . . . . . . 13 (β„€β‰₯β€˜π‘š) βŠ† ℝ
116112, 115sstri 3982 . . . . . . . . . . . 12 (π‘š...𝑛) βŠ† ℝ
117111, 116sstrdi 3985 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 βŠ† ℝ)
118 ltso 11324 . . . . . . . . . . 11 < Or ℝ
119 soss 5604 . . . . . . . . . . 11 (ran 𝐻 βŠ† ℝ β†’ ( < Or ℝ β†’ < Or ran 𝐻))
120117, 118, 119mpisyl 21 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ < Or ran 𝐻)
121 fzfi 13969 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
122121a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1...𝑀) ∈ Fin)
12312, 122fexd 7235 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐻 ∈ V)
124 f1oen3g 8985 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻) β†’ (1...𝑀) β‰ˆ ran 𝐻)
125123, 15, 124syl2anc 582 . . . . . . . . . . . . 13 (πœ‘ β†’ (1...𝑀) β‰ˆ ran 𝐻)
126 enfi 9213 . . . . . . . . . . . . 13 ((1...𝑀) β‰ˆ ran 𝐻 β†’ ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
127125, 126syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
128121, 127mpbii 232 . . . . . . . . . . 11 (πœ‘ β†’ ran 𝐻 ∈ Fin)
129128ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ ran 𝐻 ∈ Fin)
130 fz1iso 14455 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))
131120, 129, 130syl2anc 582 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))
13267nnnn0d 12562 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑀 ∈ β„•0)
133 hashfz1 14337 . . . . . . . . . . . . . . . 16 (𝑀 ∈ β„•0 β†’ (β™―β€˜(1...𝑀)) = 𝑀)
134132, 133syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = 𝑀)
135122, 15hasheqf1od 14344 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜(1...𝑀)) = (β™―β€˜ran 𝐻))
136134, 135eqtr3d 2767 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 = (β™―β€˜ran 𝐻))
137136ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑀 = (β™―β€˜ran 𝐻))
138137fveq2d 6896 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seq1( + , (𝐹 ∘ 𝑓))β€˜π‘€) = (seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜ran 𝐻)))
1391ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐺 ∈ Mnd)
14061, 63mndcl 18701 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
1411403expb 1117 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
142139, 141sylan 578 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
143 gsumval3.c . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝐹 βŠ† (π‘β€˜ran 𝐹))
144143ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐹 βŠ† (π‘β€˜ran 𝐹))
145144sselda 3972 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ran 𝐹) β†’ π‘₯ ∈ (π‘β€˜ran 𝐹))
146 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntzβ€˜πΊ)
14763, 146cntzi 19284 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (π‘β€˜ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) β†’ (π‘₯ + 𝑦) = (𝑦 + π‘₯))
148145, 147sylan 578 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) β†’ (π‘₯ + 𝑦) = (𝑦 + π‘₯))
149148anasss 465 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ (π‘₯ ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) β†’ (π‘₯ + 𝑦) = (𝑦 + π‘₯))
15061, 63mndass 18702 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯ + 𝑦) + 𝑧) = (π‘₯ + (𝑦 + 𝑧)))
151139, 150sylan 578 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯ + 𝑦) + 𝑧) = (π‘₯ + (𝑦 + 𝑧)))
15269ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑀 ∈ (β„€β‰₯β€˜1))
1537ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐹:𝐴⟢𝐡)
154153frnd 6725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐹 βŠ† 𝐡)
155 simprr 771 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))
156 isof1o 7327 . . . . . . . . . . . . . . . . 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 7432 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (1...𝑀) = (1...(β™―β€˜ran 𝐻)))
159158f1oeq2d 6830 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 ↔ 𝑓:(1...(β™―β€˜ran 𝐻))–1-1-ontoβ†’ran 𝐻))
160157, 159mpbird 256 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
161 f1ocnv 6846 . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻)
164 f1oco 6857 . . . . . . . . . . . . . 14 ((◑𝑓:ran 𝐻–1-1-ontoβ†’(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)–1-1-ontoβ†’(1...𝑀))
165162, 163, 164syl2anc 582 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)–1-1-ontoβ†’(1...𝑀))
166 ffn 6717 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴⟢𝐡 β†’ 𝐹 Fn 𝐴)
167 dffn4 6812 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–ontoβ†’ran 𝐹)
168166, 167sylib 217 . . . . . . . . . . . . . . . 16 (𝐹:𝐴⟢𝐡 β†’ 𝐹:𝐴–ontoβ†’ran 𝐹)
169 fof 6806 . . . . . . . . . . . . . . . 16 (𝐹:𝐴–ontoβ†’ran 𝐹 β†’ 𝐹:𝐴⟢ran 𝐹)
170153, 168, 1693syl 18 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐹:𝐴⟢ran 𝐹)
171 f1of 6834 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ 𝑓:(1...𝑀)⟢ran 𝐻)
172160, 171syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...𝑀)⟢ran 𝐻)
173109ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐻 βŠ† 𝐴)
174172, 173fssd 6735 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...𝑀)⟢𝐴)
175 fco 6742 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟢ran 𝐹 ∧ 𝑓:(1...𝑀)⟢𝐴) β†’ (𝐹 ∘ 𝑓):(1...𝑀)⟢ran 𝐹)
176170, 174, 175syl2anc 582 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐹 ∘ 𝑓):(1...𝑀)⟢ran 𝐹)
177176ffvelcdmda 7089 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝑓)β€˜π‘₯) ∈ ran 𝐹)
178 f1ococnv2 6861 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ (𝑓 ∘ ◑𝑓) = ( I β†Ύ ran 𝐻))
179160, 178syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝑓 ∘ ◑𝑓) = ( I β†Ύ ran 𝐻))
180179coeq1d 5858 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ((𝑓 ∘ ◑𝑓) ∘ 𝐻) = (( I β†Ύ ran 𝐻) ∘ 𝐻))
181 f1of 6834 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-ontoβ†’ran 𝐻 β†’ 𝐻:(1...𝑀)⟢ran 𝐻)
182 fcoi2 6767 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟢ran 𝐻 β†’ (( I β†Ύ ran 𝐻) ∘ 𝐻) = 𝐻)
183163, 181, 1823syl 18 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (( I β†Ύ ran 𝐻) ∘ 𝐻) = 𝐻)
184180, 183eqtr2d 2766 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻 = ((𝑓 ∘ ◑𝑓) ∘ 𝐻))
185 coass 6264 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∘ ◑𝑓) ∘ 𝐻) = (𝑓 ∘ (◑𝑓 ∘ 𝐻))
186184, 185eqtrdi 2781 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐻 = (𝑓 ∘ (◑𝑓 ∘ 𝐻)))
187186coeq2d 5859 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◑𝑓 ∘ 𝐻))))
188 coass 6264 . . . . . . . . . . . . . . . . 17 ((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◑𝑓 ∘ 𝐻)))
189187, 188eqtr4di 2783 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻)))
190189fveq1d 6894 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ((𝐹 ∘ 𝐻)β€˜π‘˜) = (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜))
191190adantr 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘˜) = (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜))
192 f1of 6834 . . . . . . . . . . . . . . . . 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 6742 . . . . . . . . . . . . . . . 16 ((◑𝑓:ran 𝐻⟢(1...𝑀) ∧ 𝐻:(1...𝑀)⟢ran 𝐻) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)⟢(1...𝑀))
196193, 194, 195syl2anc 582 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (◑𝑓 ∘ 𝐻):(1...𝑀)⟢(1...𝑀))
197 fvco3 6992 . . . . . . . . . . . . . . 15 (((◑𝑓 ∘ 𝐻):(1...𝑀)⟢(1...𝑀) ∧ π‘˜ ∈ (1...𝑀)) β†’ (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜((◑𝑓 ∘ 𝐻)β€˜π‘˜)))
198196, 197sylan 578 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘˜ ∈ (1...𝑀)) β†’ (((𝐹 ∘ 𝑓) ∘ (◑𝑓 ∘ 𝐻))β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜((◑𝑓 ∘ 𝐻)β€˜π‘˜)))
199191, 198eqtrd 2765 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘˜ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘˜) = ((𝐹 ∘ 𝑓)β€˜((◑𝑓 ∘ 𝐻)β€˜π‘˜)))
200142, 149, 151, 152, 154, 165, 177, 199seqf1o 14040 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seq1( + , (𝐹 ∘ 𝑓))β€˜π‘€))
20161, 63, 3mndlid 18713 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ π‘₯ ∈ 𝐡) β†’ ( 0 + π‘₯) = π‘₯)
202139, 201sylan 578 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ 𝐡) β†’ ( 0 + π‘₯) = π‘₯)
20361, 63, 3mndrid 18714 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ + 0 ) = π‘₯)
204139, 203sylan 578 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ + 0 ) = π‘₯)
205139, 62syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 0 ∈ 𝐡)
206 fdm 6726 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟢𝐴 β†’ dom 𝐻 = (1...𝑀))
20710, 11, 2063syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom 𝐻 = (1...𝑀))
208 eluzfz1 13540 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝑀))
209 ne0i 4330 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) β†’ (1...𝑀) β‰  βˆ…)
21069, 208, 2093syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (1...𝑀) β‰  βˆ…)
211207, 210eqnetrd 2998 . . . . . . . . . . . . . . 15 (πœ‘ β†’ dom 𝐻 β‰  βˆ…)
212 dm0rn0 5921 . . . . . . . . . . . . . . . 16 (dom 𝐻 = βˆ… ↔ ran 𝐻 = βˆ…)
213212necon3bii 2983 . . . . . . . . . . . . . . 15 (dom 𝐻 β‰  βˆ… ↔ ran 𝐻 β‰  βˆ…)
214211, 213sylib 217 . . . . . . . . . . . . . 14 (πœ‘ β†’ ran 𝐻 β‰  βˆ…)
215214ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐻 β‰  βˆ…)
216111adantrr 715 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ ran 𝐻 βŠ† (π‘š...𝑛))
217 simprl 769 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝐴 = (π‘š...𝑛))
218217eleq2d 2811 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (π‘₯ ∈ 𝐴 ↔ π‘₯ ∈ (π‘š...𝑛)))
219218biimpar 476 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (π‘š...𝑛)) β†’ π‘₯ ∈ 𝐴)
220153ffvelcdmda 7089 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ 𝐡)
221219, 220syldan 589 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (π‘š...𝑛)) β†’ (πΉβ€˜π‘₯) ∈ 𝐡)
222217difeq1d 4113 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (𝐴 βˆ– ran 𝐻) = ((π‘š...𝑛) βˆ– ran 𝐻))
223222eleq2d 2811 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (π‘₯ ∈ (𝐴 βˆ– ran 𝐻) ↔ π‘₯ ∈ ((π‘š...𝑛) βˆ– ran 𝐻)))
224223biimpar 476 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ((π‘š...𝑛) βˆ– ran 𝐻)) β†’ π‘₯ ∈ (𝐴 βˆ– ran 𝐻))
22551ad4ant14 750 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ (𝐴 βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) = 0 )
226224, 225syldan 589 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ π‘₯ ∈ ((π‘š...𝑛) βˆ– ran 𝐻)) β†’ (πΉβ€˜π‘₯) = 0 )
227 f1of 6834 . . . . . . . . . . . . . . 15 (𝑓:(1...(β™―β€˜ran 𝐻))–1-1-ontoβ†’ran 𝐻 β†’ 𝑓:(1...(β™―β€˜ran 𝐻))⟢ran 𝐻)
228155, 156, 2273syl 18 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ 𝑓:(1...(β™―β€˜ran 𝐻))⟢ran 𝐻)
229 fvco3 6992 . . . . . . . . . . . . . 14 ((𝑓:(1...(β™―β€˜ran 𝐻))⟢ran 𝐻 ∧ 𝑦 ∈ (1...(β™―β€˜ran 𝐻))) β†’ ((𝐹 ∘ 𝑓)β€˜π‘¦) = (πΉβ€˜(π‘“β€˜π‘¦)))
230228, 229sylan 578 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(β™―β€˜ran 𝐻))) β†’ ((𝐹 ∘ 𝑓)β€˜π‘¦) = (πΉβ€˜(π‘“β€˜π‘¦)))
231202, 204, 142, 205, 155, 215, 216, 221, 226, 230seqcoll2 14458 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seqπ‘š( + , 𝐹)β€˜π‘›) = (seq1( + , (𝐹 ∘ 𝑓))β€˜(β™―β€˜ran 𝐻)))
232138, 200, 2313eqtr4d 2775 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (𝐴 = (π‘š...𝑛) ∧ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻))) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›))
233232expr 455 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›)))
234233exlimdv 1928 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜ran 𝐻)), ran 𝐻) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›)))
235131, 234mpd 15 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seqπ‘š( + , 𝐹)β€˜π‘›))
236107, 235eqtr4d 2768 . . . . . . 7 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ 𝐴 = (π‘š...𝑛)) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
237236ex 411 . . . . . 6 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (𝐴 = (π‘š...𝑛) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
238237rexlimdvw 3150 . . . . 5 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
239238rexlimdvw 3150 . . . 4 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (βˆƒπ‘š ∈ β„€ βˆƒπ‘› ∈ β„€ 𝐴 = (π‘š...𝑛) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
24080, 239biimtrid 241 . . 3 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (𝐴 ∈ ran ... β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
241 suppssdm 8180 . . . . . . . . . . 11 ((𝐹 ∘ 𝐻) supp 0 ) βŠ† dom (𝐹 ∘ 𝐻)
24232, 241eqsstri 4007 . . . . . . . . . 10 π‘Š βŠ† dom (𝐹 ∘ 𝐻)
243242, 30fssdm 6737 . . . . . . . . 9 (πœ‘ β†’ π‘Š βŠ† (1...𝑀))
244 fz1ssnn 13564 . . . . . . . . . 10 (1...𝑀) βŠ† β„•
245 nnssre 12246 . . . . . . . . . 10 β„• βŠ† ℝ
246244, 245sstri 3982 . . . . . . . . 9 (1...𝑀) βŠ† ℝ
247243, 246sstrdi 3985 . . . . . . . 8 (πœ‘ β†’ π‘Š βŠ† ℝ)
248 soss 5604 . . . . . . . 8 (π‘Š βŠ† ℝ β†’ ( < Or ℝ β†’ < Or π‘Š))
249247, 118, 248mpisyl 21 . . . . . . 7 (πœ‘ β†’ < Or π‘Š)
250 ssfi 9196 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ π‘Š βŠ† (1...𝑀)) β†’ π‘Š ∈ Fin)
251121, 243, 250sylancr 585 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ Fin)
252 fz1iso 14455 . . . . . . 7 (( < Or π‘Š ∧ π‘Š ∈ Fin) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
253249, 251, 252syl2anc 582 . . . . . 6 (πœ‘ β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
254253ad2antrr 724 . . . . 5 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
25561, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32gsumval3lem2 19865 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))β€˜(β™―β€˜π‘Š)))
2561ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 𝐺 ∈ Mnd)
257256, 201sylan 578 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ 𝐡) β†’ ( 0 + π‘₯) = π‘₯)
258256, 203sylan 578 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ + 0 ) = π‘₯)
259256, 141sylan 578 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯ + 𝑦) ∈ 𝐡)
260256, 62syl 17 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 0 ∈ 𝐡)
261 simprr 771 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))
262 simplr 767 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ π‘Š β‰  βˆ…)
263243ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ π‘Š βŠ† (1...𝑀))
26430ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (𝐹 ∘ 𝐻):(1...𝑀)⟢𝐡)
265264ffvelcdmda 7089 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ (1...𝑀)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) ∈ 𝐡)
26633a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ ((𝐹 ∘ 𝐻) supp 0 ) βŠ† π‘Š)
267 ovexd 7451 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (1...𝑀) ∈ V)
26836a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 0 ∈ V)
269264, 266, 267, 268suppssr 8199 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ π‘₯ ∈ ((1...𝑀) βˆ– π‘Š)) β†’ ((𝐹 ∘ 𝐻)β€˜π‘₯) = 0 )
270 coass 6264 . . . . . . . . . . 11 ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓))
271270fveq1i 6893 . . . . . . . . . 10 (((𝐹 ∘ 𝐻) ∘ 𝑓)β€˜π‘¦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))β€˜π‘¦)
272 isof1o 7327 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š) β†’ 𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š)
273 f1of 6834 . . . . . . . . . . . 12 (𝑓:(1...(β™―β€˜π‘Š))–1-1-ontoβ†’π‘Š β†’ 𝑓:(1...(β™―β€˜π‘Š))βŸΆπ‘Š)
274261, 272, 2733syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ 𝑓:(1...(β™―β€˜π‘Š))βŸΆπ‘Š)
275 fvco3 6992 . . . . . . . . . . 11 ((𝑓:(1...(β™―β€˜π‘Š))βŸΆπ‘Š ∧ 𝑦 ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘ 𝐻) ∘ 𝑓)β€˜π‘¦) = ((𝐹 ∘ 𝐻)β€˜(π‘“β€˜π‘¦)))
276274, 275sylan 578 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ 𝑦 ∈ (1...(β™―β€˜π‘Š))) β†’ (((𝐹 ∘ 𝐻) ∘ 𝑓)β€˜π‘¦) = ((𝐹 ∘ 𝐻)β€˜(π‘“β€˜π‘¦)))
277271, 276eqtr3id 2779 . . . . . . . . 9 ((((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) ∧ 𝑦 ∈ (1...(β™―β€˜π‘Š))) β†’ ((𝐹 ∘ (𝐻 ∘ 𝑓))β€˜π‘¦) = ((𝐹 ∘ 𝐻)β€˜(π‘“β€˜π‘¦)))
278257, 258, 259, 260, 261, 262, 263, 265, 269, 277seqcoll2 14458 . . . . . . . 8 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))β€˜(β™―β€˜π‘Š)))
279255, 278eqtr4d 2768 . . . . . . 7 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ (Β¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š))) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
280279expr 455 . . . . . 6 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ (𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
281280exlimdv 1928 . . . . 5 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ (βˆƒπ‘“ 𝑓 Isom < , < ((1...(β™―β€˜π‘Š)), π‘Š) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
282254, 281mpd 15 . . . 4 (((πœ‘ ∧ π‘Š β‰  βˆ…) ∧ Β¬ 𝐴 ∈ ran ...) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
283282ex 411 . . 3 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (Β¬ 𝐴 ∈ ran ... β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€)))
284240, 283pm2.61d 179 . 2 ((πœ‘ ∧ π‘Š β‰  βˆ…) β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
28576, 284pm2.61dane 3019 1 (πœ‘ β†’ (𝐺 Ξ£g 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))β€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2930  βˆƒwrex 3060  Vcvv 3463   βˆ– cdif 3936   βŠ† wss 3939  βˆ…c0 4318  π’« cpw 4598  {csn 4624   class class class wbr 5143   ↦ cmpt 5226   I cid 5569   Or wor 5583   Γ— cxp 5670  β—‘ccnv 5671  dom cdm 5672  ran crn 5673   β†Ύ cres 5674   ∘ ccom 5676  Rel wrel 5677   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“ontoβ†’wfo 6541  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7416   supp csupp 8163   β‰ˆ cen 8959  Fincfn 8962  β„cr 11137  1c1 11139   < clt 11278  β„•cn 12242  β„•0cn0 12502  β„€cz 12588  β„€β‰₯cuz 12852  ...cfz 13516  seqcseq 13998  β™―chash 14321  Basecbs 17179  +gcplusg 17232  0gc0g 17420   Ξ£g cgsu 17421  Mndcmnd 18693  Cntzccntz 19270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  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 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7991  df-2nd 7992  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-n0 12503  df-z 12589  df-uz 12853  df-fz 13517  df-fzo 13660  df-seq 13999  df-hash 14322  df-0g 17422  df-gsum 17423  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-cntz 19272
This theorem is referenced by:  gsumzres  19868  gsumzcl2  19869  gsumzf1o  19871  gsumzaddlem  19880  gsumconst  19893  gsumzmhm  19896  gsumzoppg  19903  gsumfsum  21371  wilthlem3  27020
  Copyright terms: Public domain W3C validator