Metamath Proof Explorer

Theorem gsumval3

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)

Ref Expression
Hypotheses 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 gsumval3 ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 gsumval3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumval3.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumval3.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumval3.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5 gsumval3.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 gsumval3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 gsumval3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 gsumval3.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9 gsumval3.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
10 gsumval3.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
11 gsumval3.n ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ran 𝐻 )
12 gsumval3.w ⊢ 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 )
13 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
14 5 6 13 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
16 7 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
18 f1f ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
19 10 18 syl ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
21 f1f1orn ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
22 10 21 syl ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
24 f1ocnv ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → ◡ 𝐻 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) )
25 f1of ⊢ ( ◡ 𝐻 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) → ◡ 𝐻 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) )
26 23 24 25 3syl ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ◡ 𝐻 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) )
27 26 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( ◡ 𝐻 ‘ 𝑥 ) ∈ ( 1 ... 𝑀 ) )
28 fvco3 ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( ◡ 𝐻 ‘ 𝑥 ) ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ) )
29 20 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝑊 = ∅ )
31 30 difeq2d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( 1 ... 𝑀 ) ∖ 𝑊 ) = ( ( 1 ... 𝑀 ) ∖ ∅ ) )
32 dif0 ⊢ ( ( 1 ... 𝑀 ) ∖ ∅ ) = ( 1 ... 𝑀 )
33 31 32 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( 1 ... 𝑀 ) ∖ 𝑊 ) = ( 1 ... 𝑀 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( ( 1 ... 𝑀 ) ∖ 𝑊 ) = ( 1 ... 𝑀 ) )
35 27 34 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( ◡ 𝐻 ‘ 𝑥 ) ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) )
36 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
37 7 19 36 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
39 12 eqimss2i ⊢ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ 𝑊
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ 𝑊 )
41 ovexd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 1 ... 𝑀 ) ∈ V )
42 2 fvexi ⊢ 0 ∈ V
43 42 a1i ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 0 ∈ V )
44 38 40 41 43 suppssr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = 0 )
45 35 44 syldan ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = 0 )
46 f1ocnvfv2 ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = 𝑥 )
47 23 46 sylan ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = 𝑥 )
48 47 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝐹 ‘ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
49 29 45 48 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝐹 ‘ 𝑥 ) = 0 )
50 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
51 50 elsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝑥 ) = 0 )
52 49 51 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
53 52 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ ran 𝐻 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
54 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻 ) )
55 42 a1i ⊢ ( 𝜑 → 0 ∈ V )
56 7 11 6 55 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
57 56 51 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
58 54 57 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
59 58 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
60 59 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑥 ∈ ran 𝐻 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
61 53 60 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
62 61 51 sylib ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 0 )
63 62 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
64 17 63 eqtrd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
65 64 oveq2d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )
66 1 2 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
67 1 3 2 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐵 ) → ( 0 + 0 ) = 0 )
68 5 66 67 syl2anc2 ⊢ ( 𝜑 → ( 0 + 0 ) = 0 )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 0 + 0 ) = 0 )
70 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
71 9 70 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
73 33 eleq2d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) ↔ 𝑥 ∈ ( 1 ... 𝑀 ) ) )
74 73 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) )
75 38 40 41 43 suppssr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = 0 )
76 74 75 syldan ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = 0 )
77 69 72 76 seqid3 ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = 0 )
78 15 65 77 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
79 fzf ⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
80 ffn ⊢ ( ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ → ... Fn ( ℤ × ℤ ) )
81 ovelrn ⊢ ( ... Fn ( ℤ × ℤ ) → ( 𝐴 ∈ ran ... ↔ ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑚 ... 𝑛 ) ) )
82 79 80 81 mp2b ⊢ ( 𝐴 ∈ ran ... ↔ ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑚 ... 𝑛 ) )
83 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → 𝐺 ∈ Mnd )
84 simpr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → 𝐴 = ( 𝑚 ... 𝑛 ) )
85 frel ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Rel 𝐹 )
86 reldm0 ⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
87 7 85 86 3syl ⊢ ( 𝜑 → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
88 7 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
89 88 eqeq1d ⊢ ( 𝜑 → ( dom 𝐹 = ∅ ↔ 𝐴 = ∅ ) )
90 87 89 bitrd ⊢ ( 𝜑 → ( 𝐹 = ∅ ↔ 𝐴 = ∅ ) )
91 coeq1 ⊢ ( 𝐹 = ∅ → ( 𝐹 ∘ 𝐻 ) = ( ∅ ∘ 𝐻 ) )
92 co01 ⊢ ( ∅ ∘ 𝐻 ) = ∅
93 91 92 eqtrdi ⊢ ( 𝐹 = ∅ → ( 𝐹 ∘ 𝐻 ) = ∅ )
94 93 oveq1d ⊢ ( 𝐹 = ∅ → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ∅ supp 0 ) )
95 supp0 ⊢ ( 0 ∈ V → ( ∅ supp 0 ) = ∅ )
96 42 95 ax-mp ⊢ ( ∅ supp 0 ) = ∅
97 94 96 eqtrdi ⊢ ( 𝐹 = ∅ → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ∅ )
98 12 97 eqtrid ⊢ ( 𝐹 = ∅ → 𝑊 = ∅ )
99 90 98 biimtrrdi ⊢ ( 𝜑 → ( 𝐴 = ∅ → 𝑊 = ∅ ) )
100 99 necon3d ⊢ ( 𝜑 → ( 𝑊 ≠ ∅ → 𝐴 ≠ ∅ ) )
101 100 imp ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → 𝐴 ≠ ∅ )
102 101 adantr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → 𝐴 ≠ ∅ )
103 84 102 eqnetrrd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝑚 ... 𝑛 ) ≠ ∅ )
104 fzn0 ⊢ ( ( 𝑚 ... 𝑛 ) ≠ ∅ ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) )
105 103 104 sylib ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) )
106 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
107 84 feq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : ( 𝑚 ... 𝑛 ) ⟶ 𝐵 ) )
108 106 107 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → 𝐹 : ( 𝑚 ... 𝑛 ) ⟶ 𝐵 )
109 1 3 83 105 108 gsumval2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
110 frn ⊢ ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 → ran 𝐻 ⊆ 𝐴 )
111 10 18 110 3syl ⊢ ( 𝜑 → ran 𝐻 ⊆ 𝐴 )
112 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ran 𝐻 ⊆ 𝐴 )
113 112 84 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ran 𝐻 ⊆ ( 𝑚 ... 𝑛 ) )
114 fzssuz ⊢ ( 𝑚 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑚 )
115 uzssz ⊢ ( ℤ≥ ‘ 𝑚 ) ⊆ ℤ
116 zssre ⊢ ℤ ⊆ ℝ
117 115 116 sstri ⊢ ( ℤ≥ ‘ 𝑚 ) ⊆ ℝ
118 114 117 sstri ⊢ ( 𝑚 ... 𝑛 ) ⊆ ℝ
119 113 118 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ran 𝐻 ⊆ ℝ )
120 ltso ⊢ < Or ℝ
121 soss ⊢ ( ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻 ) )
122 119 120 121 mpisyl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → < Or ran 𝐻 )
123 fzfi ⊢ ( 1 ... 𝑀 ) ∈ Fin
124 123 a1i ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
125 19 124 fexd ⊢ ( 𝜑 → 𝐻 ∈ V )
126 f1oen3g ⊢ ( ( 𝐻 ∈ V ∧ 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ) → ( 1 ... 𝑀 ) ≈ ran 𝐻 )
127 125 22 126 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ≈ ran 𝐻 )
128 enfi ⊢ ( ( 1 ... 𝑀 ) ≈ ran 𝐻 → ( ( 1 ... 𝑀 ) ∈ Fin ↔ ran 𝐻 ∈ Fin ) )
129 127 128 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∈ Fin ↔ ran 𝐻 ∈ Fin ) )
130 123 129 mpbii ⊢ ( 𝜑 → ran 𝐻 ∈ Fin )
131 130 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ran 𝐻 ∈ Fin )
132 fz1iso ⊢ ( ( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) )
133 122 131 132 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) )
134 9 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
135 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
136 134 135 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
137 124 22 hasheqf1od ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = ( ♯ ‘ ran 𝐻 ) )
138 136 137 eqtr3d ⊢ ( 𝜑 → 𝑀 = ( ♯ ‘ ran 𝐻 ) )
139 138 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑀 = ( ♯ ‘ ran 𝐻 ) )
140 139 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ran 𝐻 ) ) )
141 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐺 ∈ Mnd )
142 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
143 142 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
144 141 143 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
145 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
146 145 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ran 𝐹 ) → 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) )
147 3 4 cntzi ⊢ ( ( 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
148 146 147 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ran 𝐹 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
149 148 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
150 1 3 mndass ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
151 141 150 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
152 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
153 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
154 153 frnd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐹 ⊆ 𝐵 )
155 simprr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) )
156 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 )
157 155 156 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 )
158 139 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 1 ... 𝑀 ) = ( 1 ... ( ♯ ‘ ran 𝐻 ) ) )
159 158 f1oeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ↔ 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 ) )
160 157 159 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
161 f1ocnv ⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) )
162 160 161 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) )
163 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
164 f1oco ⊢ ( ( ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) ∧ 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
165 162 163 164 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
166 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
167 dffn4 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
168 166 167 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ran 𝐹 )
169 fof ⊢ ( 𝐹 : 𝐴 –onto→ ran 𝐹 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
170 153 168 169 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
171 f1of ⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → 𝑓 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
172 160 171 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
173 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐻 ⊆ 𝐴 )
174 172 173 fssd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
175 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐹 )
176 170 174 175 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐹 )
177 176 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ∈ ran 𝐹 )
178 f1ococnv2 ⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → ( 𝑓 ∘ ◡ 𝑓 ) = ( I ↾ ran 𝐻 ) )
179 160 178 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑓 ∘ ◡ 𝑓 ) = ( I ↾ ran 𝐻 ) )
180 179 coeq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ 𝐻 ) = ( ( I ↾ ran 𝐻 ) ∘ 𝐻 ) )
181 f1of ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
182 fcoi2 ⊢ ( 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 → ( ( I ↾ ran 𝐻 ) ∘ 𝐻 ) = 𝐻 )
183 163 181 182 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ( I ↾ ran 𝐻 ) ∘ 𝐻 ) = 𝐻 )
184 180 183 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 = ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ 𝐻 ) )
185 coass ⊢ ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ 𝐻 ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) )
186 184 185 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 = ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) )
187 186 coeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ) )
188 coass ⊢ ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) = ( 𝐹 ∘ ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) )
189 187 188 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐹 ∘ 𝐻 ) = ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) )
190 189 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) )
191 190 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) )
192 f1of ⊢ ( ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) → ◡ 𝑓 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) )
193 160 161 192 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ◡ 𝑓 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) )
194 163 181 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
195 fco ⊢ ( ( ◡ 𝑓 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) ∧ 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
196 193 194 195 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
197 fvco3 ⊢ ( ( ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ ( ( ◡ 𝑓 ∘ 𝐻 ) ‘ 𝑘 ) ) )
198 196 197 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ ( ( ◡ 𝑓 ∘ 𝐻 ) ‘ 𝑘 ) ) )
199 191 198 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ ( ( ◡ 𝑓 ∘ 𝐻 ) ‘ 𝑘 ) ) )
200 144 149 151 152 154 165 177 199 seqf1o ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑀 ) )
201 1 3 2 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
202 141 201 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
203 1 3 2 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
204 141 203 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
205 141 66 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 0 ∈ 𝐵 )
206 fdm ⊢ ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 → dom 𝐻 = ( 1 ... 𝑀 ) )
207 10 18 206 3syl ⊢ ( 𝜑 → dom 𝐻 = ( 1 ... 𝑀 ) )
208 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑀 ) )
209 ne0i ⊢ ( 1 ∈ ( 1 ... 𝑀 ) → ( 1 ... 𝑀 ) ≠ ∅ )
210 71 208 209 3syl ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ≠ ∅ )
211 207 210 eqnetrd ⊢ ( 𝜑 → dom 𝐻 ≠ ∅ )
212 dm0rn0 ⊢ ( dom 𝐻 = ∅ ↔ ran 𝐻 = ∅ )
213 212 necon3bii ⊢ ( dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅ )
214 211 213 sylib ⊢ ( 𝜑 → ran 𝐻 ≠ ∅ )
215 214 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐻 ≠ ∅ )
216 113 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐻 ⊆ ( 𝑚 ... 𝑛 ) )
217 simprl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐴 = ( 𝑚 ... 𝑛 ) )
218 217 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( 𝑚 ... 𝑛 ) ) )
219 218 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 𝑚 ... 𝑛 ) ) → 𝑥 ∈ 𝐴 )
220 153 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
221 219 220 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 𝑚 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
222 217 difeq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐴 ∖ ran 𝐻 ) = ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) )
223 222 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ↔ 𝑥 ∈ ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) ) )
224 223 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) ) → 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) )
225 56 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
226 224 225 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
227 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ⟶ ran 𝐻 )
228 155 156 227 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ⟶ ran 𝐻 )
229 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ⟶ ran 𝐻 ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) )
230 228 229 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) )
231 202 204 144 205 155 215 216 221 226 230 seqcoll2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ran 𝐻 ) ) )
232 140 200 231 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
233 232 expr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) )
234 233 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) )
235 133 234 mpd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
236 109 235 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
237 236 ex ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐴 = ( 𝑚 ... 𝑛 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
238 237 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑚 ... 𝑛 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
239 238 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑚 ... 𝑛 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
240 82 239 biimtrid ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐴 ∈ ran ... → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
241 suppssdm ⊢ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ dom ( 𝐹 ∘ 𝐻 )
242 12 241 eqsstri ⊢ 𝑊 ⊆ dom ( 𝐹 ∘ 𝐻 )
243 242 37 fssdm ⊢ ( 𝜑 → 𝑊 ⊆ ( 1 ... 𝑀 ) )
244 fz1ssnn ⊢ ( 1 ... 𝑀 ) ⊆ ℕ
245 nnssre ⊢ ℕ ⊆ ℝ
246 244 245 sstri ⊢ ( 1 ... 𝑀 ) ⊆ ℝ
247 243 246 sstrdi ⊢ ( 𝜑 → 𝑊 ⊆ ℝ )
248 soss ⊢ ( 𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊 ) )
249 247 120 248 mpisyl ⊢ ( 𝜑 → < Or 𝑊 )
250 ssfi ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → 𝑊 ∈ Fin )
251 123 243 250 sylancr ⊢ ( 𝜑 → 𝑊 ∈ Fin )
252 fz1iso ⊢ ( ( < Or 𝑊 ∧ 𝑊 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
253 249 251 252 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
254 253 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
255 1 2 3 4 5 6 7 8 9 10 11 12 gsumval3lem2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
256 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐺 ∈ Mnd )
257 256 201 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
258 256 203 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
259 256 143 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
260 256 66 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 0 ∈ 𝐵 )
261 simprr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
262 simplr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ≠ ∅ )
263 243 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ⊆ ( 1 ... 𝑀 ) )
264 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
265 264 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐵 )
266 39 a1i ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ 𝑊 )
267 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 1 ... 𝑀 ) ∈ V )
268 42 a1i ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 0 ∈ V )
269 264 266 267 268 suppssr ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = 0 )
270 coass ⊢ ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) = ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) )
271 270 fveq1i ⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑦 )
272 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 )
273 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
274 261 272 273 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
275 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝐻 ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
276 274 275 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝐻 ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
277 271 276 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝐻 ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
278 257 258 259 260 261 262 263 265 269 277 seqcoll2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
279 255 278 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
280 279 expr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
281 280 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ( ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
282 254 281 mpd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
283 282 ex ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( ¬ 𝐴 ∈ ran ... → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
284 240 283 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
285 78 284 pm2.61dane ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )