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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ 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 syl5eq ⊢ ( 𝐹 = ∅ → 𝑊 = ∅ )
99 90 98 syl6bir ⊢ ( 𝜑 → ( 𝐴 = ∅ → 𝑊 = ∅ ) )
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 fex2 ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ Fin ∧ 𝐴 ∈ 𝑉 ) → 𝐻 ∈ V )
126 19 124 6 125 syl3anc ⊢ ( 𝜑 → 𝐻 ∈ V )
127 f1oen3g ⊢ ( ( 𝐻 ∈ V ∧ 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ) → ( 1 ... 𝑀 ) ≈ ran 𝐻 )
128 126 22 127 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ≈ ran 𝐻 )
129 enfi ⊢ ( ( 1 ... 𝑀 ) ≈ ran 𝐻 → ( ( 1 ... 𝑀 ) ∈ Fin ↔ ran 𝐻 ∈ Fin ) )
130 128 129 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∈ Fin ↔ ran 𝐻 ∈ Fin ) )
131 123 130 mpbii ⊢ ( 𝜑 → ran 𝐻 ∈ Fin )
132 131 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ran 𝐻 ∈ Fin )
133 fz1iso ⊢ ( ( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) )
134 122 132 133 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) )
135 9 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
136 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
137 135 136 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
138 124 22 hasheqf1od ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = ( ♯ ‘ ran 𝐻 ) )
139 137 138 eqtr3d ⊢ ( 𝜑 → 𝑀 = ( ♯ ‘ ran 𝐻 ) )
140 139 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑀 = ( ♯ ‘ ran 𝐻 ) )
141 140 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ran 𝐻 ) ) )
142 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐺 ∈ Mnd )
143 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
144 143 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
145 142 144 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
146 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
147 146 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ran 𝐹 ) → 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) )
148 3 4 cntzi ⊢ ( ( 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
149 147 148 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ran 𝐹 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
150 149 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
151 1 3 mndass ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
152 142 151 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
153 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
154 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
155 154 frnd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐹 ⊆ 𝐵 )
156 simprr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) )
157 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 )
158 156 157 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 )
159 140 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 1 ... 𝑀 ) = ( 1 ... ( ♯ ‘ ran 𝐻 ) ) )
160 159 f1oeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ↔ 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 ) )
161 158 160 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
162 f1ocnv ⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) )
163 161 162 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) )
164 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
165 f1oco ⊢ ( ( ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) ∧ 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
166 163 164 165 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
167 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
168 dffn4 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
169 167 168 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ran 𝐹 )
170 fof ⊢ ( 𝐹 : 𝐴 –onto→ ran 𝐹 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
171 154 169 170 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
172 f1of ⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → 𝑓 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
173 161 172 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
174 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐻 ⊆ 𝐴 )
175 173 174 fssd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
176 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐹 )
177 171 175 176 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐹 )
178 177 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) ∈ ran 𝐹 )
179 f1ococnv2 ⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → ( 𝑓 ∘ ◡ 𝑓 ) = ( I ↾ ran 𝐻 ) )
180 161 179 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑓 ∘ ◡ 𝑓 ) = ( I ↾ ran 𝐻 ) )
181 180 coeq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ 𝐻 ) = ( ( I ↾ ran 𝐻 ) ∘ 𝐻 ) )
182 f1of ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 → 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
183 fcoi2 ⊢ ( 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 → ( ( I ↾ ran 𝐻 ) ∘ 𝐻 ) = 𝐻 )
184 164 182 183 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ( I ↾ ran 𝐻 ) ∘ 𝐻 ) = 𝐻 )
185 181 184 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 = ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ 𝐻 ) )
186 coass ⊢ ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ 𝐻 ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) )
187 185 186 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 = ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) )
188 187 coeq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ) )
189 coass ⊢ ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) = ( 𝐹 ∘ ( 𝑓 ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) )
190 188 189 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐹 ∘ 𝐻 ) = ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) )
191 190 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) )
192 191 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) )
193 f1of ⊢ ( ◡ 𝑓 : ran 𝐻 –1-1-onto→ ( 1 ... 𝑀 ) → ◡ 𝑓 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) )
194 161 162 193 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ◡ 𝑓 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) )
195 164 182 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 )
196 fco ⊢ ( ( ◡ 𝑓 : ran 𝐻 ⟶ ( 1 ... 𝑀 ) ∧ 𝐻 : ( 1 ... 𝑀 ) ⟶ ran 𝐻 ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
197 194 195 196 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
198 fvco3 ⊢ ( ( ( ◡ 𝑓 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ ( ( ◡ 𝑓 ∘ 𝐻 ) ‘ 𝑘 ) ) )
199 197 198 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐹 ∘ 𝑓 ) ∘ ( ◡ 𝑓 ∘ 𝐻 ) ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ ( ( ◡ 𝑓 ∘ 𝐻 ) ‘ 𝑘 ) ) )
200 192 199 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ ( ( ◡ 𝑓 ∘ 𝐻 ) ‘ 𝑘 ) ) )
201 145 150 152 153 155 166 178 200 seqf1o ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑀 ) )
202 1 3 2 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
203 142 202 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
204 1 3 2 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
205 142 204 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
206 142 66 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 0 ∈ 𝐵 )
207 fdm ⊢ ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 → dom 𝐻 = ( 1 ... 𝑀 ) )
208 10 18 207 3syl ⊢ ( 𝜑 → dom 𝐻 = ( 1 ... 𝑀 ) )
209 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑀 ) )
210 ne0i ⊢ ( 1 ∈ ( 1 ... 𝑀 ) → ( 1 ... 𝑀 ) ≠ ∅ )
211 71 209 210 3syl ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ≠ ∅ )
212 208 211 eqnetrd ⊢ ( 𝜑 → dom 𝐻 ≠ ∅ )
213 dm0rn0 ⊢ ( dom 𝐻 = ∅ ↔ ran 𝐻 = ∅ )
214 213 necon3bii ⊢ ( dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅ )
215 212 214 sylib ⊢ ( 𝜑 → ran 𝐻 ≠ ∅ )
216 215 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐻 ≠ ∅ )
217 113 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ran 𝐻 ⊆ ( 𝑚 ... 𝑛 ) )
218 simprl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝐴 = ( 𝑚 ... 𝑛 ) )
219 218 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( 𝑚 ... 𝑛 ) ) )
220 219 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 𝑚 ... 𝑛 ) ) → 𝑥 ∈ 𝐴 )
221 154 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
222 220 221 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 𝑚 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
223 218 difeq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝐴 ∖ ran 𝐻 ) = ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) )
224 223 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ↔ 𝑥 ∈ ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) ) )
225 224 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) ) → 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) )
226 56 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
227 225 226 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑥 ∈ ( ( 𝑚 ... 𝑛 ) ∖ ran 𝐻 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
228 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) –1-1-onto→ ran 𝐻 → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ⟶ ran 𝐻 )
229 156 157 228 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ⟶ ran 𝐻 )
230 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ⟶ ran 𝐻 ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) )
231 229 230 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ ran 𝐻 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) )
232 203 205 145 206 156 216 217 222 227 231 seqcoll2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ran 𝐻 ) ) )
233 141 201 232 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
234 233 expr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) )
235 234 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ ran 𝐻 ) ) , ran 𝐻 ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) )
236 134 235 mpd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
237 109 236 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ 𝐴 = ( 𝑚 ... 𝑛 ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
238 237 ex ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐴 = ( 𝑚 ... 𝑛 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
239 238 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑚 ... 𝑛 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
240 239 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑚 ... 𝑛 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
241 82 240 syl5bi ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐴 ∈ ran ... → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
242 suppssdm ⊢ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ dom ( 𝐹 ∘ 𝐻 )
243 12 242 eqsstri ⊢ 𝑊 ⊆ dom ( 𝐹 ∘ 𝐻 )
244 243 37 fssdm ⊢ ( 𝜑 → 𝑊 ⊆ ( 1 ... 𝑀 ) )
245 fz1ssnn ⊢ ( 1 ... 𝑀 ) ⊆ ℕ
246 nnssre ⊢ ℕ ⊆ ℝ
247 245 246 sstri ⊢ ( 1 ... 𝑀 ) ⊆ ℝ
248 244 247 sstrdi ⊢ ( 𝜑 → 𝑊 ⊆ ℝ )
249 soss ⊢ ( 𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊 ) )
250 248 120 249 mpisyl ⊢ ( 𝜑 → < Or 𝑊 )
251 ssfi ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → 𝑊 ∈ Fin )
252 123 244 251 sylancr ⊢ ( 𝜑 → 𝑊 ∈ Fin )
253 fz1iso ⊢ ( ( < Or 𝑊 ∧ 𝑊 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
254 250 252 253 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
255 254 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
256 1 2 3 4 5 6 7 8 9 10 11 12 gsumval3lem2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
257 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐺 ∈ Mnd )
258 257 202 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
259 257 204 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
260 257 144 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
261 257 66 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 0 ∈ 𝐵 )
262 simprr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) )
263 simplr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ≠ ∅ )
264 244 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ⊆ ( 1 ... 𝑀 ) )
265 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
266 265 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐵 )
267 39 a1i ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ 𝑊 )
268 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 1 ... 𝑀 ) ∈ V )
269 42 a1i ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 0 ∈ V )
270 265 267 268 269 suppssr ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = 0 )
271 coass ⊢ ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) = ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) )
272 271 fveq1i ⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑦 )
273 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 )
274 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
275 262 273 274 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
276 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝐻 ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
277 275 276 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) ∘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝐻 ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
278 272 277 syl5eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑦 ) = ( ( 𝐹 ∘ 𝐻 ) ‘ ( 𝑓 ‘ 𝑦 ) ) )
279 258 259 260 261 262 263 264 266 270 278 seqcoll2 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
280 256 279 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
281 280 expr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
282 281 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ( ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
283 255 282 mpd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ¬ 𝐴 ∈ ran ... ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
284 283 ex ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( ¬ 𝐴 ∈ ran ... → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) ) )
285 241 284 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )
286 78 285 pm2.61dane ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝐻 ) ) ‘ 𝑀 ) )