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 eqtrid ( 𝐹 = ∅ → 𝑊 = ∅ )
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 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 ffvelrnda ( ( ( ( 𝜑𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 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 ffvelrnda ( ( ( ( 𝜑𝑊 ≠ ∅ ) ∧ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑓 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 syl5bi ( ( 𝜑𝑊 ≠ ∅ ) → ( 𝐴 ∈ 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 ffvelrnda ( ( ( ( 𝜑𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ 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 ( + , ( 𝐹𝐻 ) ) ‘ 𝑀 ) )