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

Theorem gsumval3 18236
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 17302 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
51, 2, 4syl2anc 692 . . . 4 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
65adantr 481 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
7 gsumval3.f . . . . . . 7 (𝜑𝐹:𝐴𝐵)
87feqmptd 6211 . . . . . 6 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
98adantr 481 . . . . 5 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
10 gsumval3.h . . . . . . . . . . . . . 14 (𝜑𝐻:(1...𝑀)–1-1𝐴)
11 f1f 6063 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)⟶𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (𝜑𝐻:(1...𝑀)⟶𝐴)
1312ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14 f1f1orn 6110 . . . . . . . . . . . . . . . 16 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1510, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
1615adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
17 f1ocnv 6111 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:ran 𝐻1-1-onto→(1...𝑀))
18 f1of 6099 . . . . . . . . . . . . . 14 (𝐻:ran 𝐻1-1-onto→(1...𝑀) → 𝐻:ran 𝐻⟶(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 𝐻:ran 𝐻⟶(1...𝑀))
2019ffvelrnda 6320 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ (1...𝑀))
21 fvco3 6237 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟶𝐴 ∧ (𝐻𝑥) ∈ (1...𝑀)) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
2213, 20, 21syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
23 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑊 = ∅) → 𝑊 = ∅)
2423difeq2d 3711 . . . . . . . . . . . . . . 15 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25 dif0 3929 . . . . . . . . . . . . . . 15 ((1...𝑀) ∖ ∅) = (1...𝑀)
2624, 25syl6eq 2671 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2726adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2820, 27eleqtrrd 2701 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29 fco 6020 . . . . . . . . . . . . . . 15 ((𝐹:𝐴𝐵𝐻:(1...𝑀)⟶𝐴) → (𝐹𝐻):(1...𝑀)⟶𝐵)
307, 12, 29syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐻):(1...𝑀)⟶𝐵)
3130adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (𝐹𝐻):(1...𝑀)⟶𝐵)
32 gsumval3.w . . . . . . . . . . . . . . 15 𝑊 = ((𝐹𝐻) supp 0 )
3332eqimss2i 3644 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ 𝑊
3433a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
35 ovex 6638 . . . . . . . . . . . . . 14 (1...𝑀) ∈ V
3635a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (1...𝑀) ∈ V)
37 fvex 6163 . . . . . . . . . . . . . . 15 (0g𝐺) ∈ V
383, 37eqeltri 2694 . . . . . . . . . . . . . 14 0 ∈ V
3938a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 0 ∈ V)
4031, 34, 36, 39suppssr 7278 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
4128, 40syldan 487 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
42 f1ocnvfv2 6493 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4316, 42sylan 488 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4443fveq2d 6157 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(𝐻𝑥))) = (𝐹𝑥))
4522, 41, 443eqtr3rd 2664 . . . . . . . . . 10 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) = 0 )
46 fvex 6163 . . . . . . . . . . 11 (𝐹𝑥) ∈ V
4746elsn 4168 . . . . . . . . . 10 ((𝐹𝑥) ∈ { 0 } ↔ (𝐹𝑥) = 0 )
4845, 47sylibr 224 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
4948adantlr 750 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
50 eldif 3569 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
51 gsumval3.n . . . . . . . . . . . . 13 (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
5238a1i 11 . . . . . . . . . . . . 13 (𝜑0 ∈ V)
537, 51, 2, 52suppssr 7278 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
5453, 47sylibr 224 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5550, 54sylan2br 493 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5655adantlr 750 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5756anassrs 679 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
5849, 57pm2.61dan 831 . . . . . . 7 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ { 0 })
5958, 47sylib 208 . . . . . 6 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) = 0 )
6059mpteq2dva 4709 . . . . 5 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴0 ))
619, 60eqtrd 2655 . . . 4 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
6261oveq2d 6626 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
63 gsumval3.b . . . . . . . 8 𝐵 = (Base‘𝐺)
6463, 3mndidcl 17236 . . . . . . 7 (𝐺 ∈ Mnd → 0𝐵)
651, 64syl 17 . . . . . 6 (𝜑0𝐵)
66 gsumval3.p . . . . . . 7 + = (+g𝐺)
6763, 66, 3mndlid 17239 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
681, 65, 67syl2anc 692 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
6968adantr 481 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
70 gsumval3.m . . . . . 6 (𝜑𝑀 ∈ ℕ)
71 nnuz 11674 . . . . . 6 ℕ = (ℤ‘1)
7270, 71syl6eleq 2708 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
7372adantr 481 . . . 4 ((𝜑𝑊 = ∅) → 𝑀 ∈ (ℤ‘1))
7426eleq2d 2684 . . . . . 6 ((𝜑𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
7574biimpar 502 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
7631, 34, 36, 39suppssr 7278 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
7775, 76syldan 487 . . . 4 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) = 0 )
7869, 73, 77seqid3 12792 . . 3 ((𝜑𝑊 = ∅) → (seq1( + , (𝐹𝐻))‘𝑀) = 0 )
796, 62, 783eqtr4d 2665 . 2 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
80 fzf 12279 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
81 ffn 6007 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
82 ovelrn 6770 . . . . 5 (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
8380, 81, 82mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
841ad2antrr 761 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
85 simpr 477 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
86 frel 6012 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → Rel 𝐹)
87 reldm0 5308 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
887, 86, 873syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
89 fdm 6013 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
907, 89syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐴)
9190eqeq1d 2623 . . . . . . . . . . . . . . . 16 (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
9288, 91bitrd 268 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
93 coeq1 5244 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ∅ → (𝐹𝐻) = (∅ ∘ 𝐻))
94 co01 5614 . . . . . . . . . . . . . . . . . . 19 (∅ ∘ 𝐻) = ∅
9593, 94syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (𝐹 = ∅ → (𝐹𝐻) = ∅)
9695oveq1d 6625 . . . . . . . . . . . . . . . . 17 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = (∅ supp 0 ))
97 supp0 7252 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V → (∅ supp 0 ) = ∅)
9838, 97ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ supp 0 ) = ∅
9996, 98syl6eq 2671 . . . . . . . . . . . . . . . 16 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = ∅)
10032, 99syl5eq 2667 . . . . . . . . . . . . . . 15 (𝐹 = ∅ → 𝑊 = ∅)
10192, 100syl6bir 244 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
102101necon3d 2811 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
103102imp 445 . . . . . . . . . . . 12 ((𝜑𝑊 ≠ ∅) → 𝐴 ≠ ∅)
104103adantr 481 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
10585, 104eqnetrrd 2858 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
106 fzn0 12304 . . . . . . . . . 10 ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ𝑚))
107105, 106sylib 208 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ𝑚))
1087ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴𝐵)
10985feq2d 5993 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴𝐵𝐹:(𝑚...𝑛)⟶𝐵))
110108, 109mpbid 222 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
11163, 66, 84, 107, 110gsumval2 17208 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
112 frn 6015 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻𝐴)
11310, 11, 1123syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻𝐴)
114113ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻𝐴)
115114, 85sseqtrd 3625 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
116 fzssuz 12331 . . . . . . . . . . . . 13 (𝑚...𝑛) ⊆ (ℤ𝑚)
117 uzssz 11658 . . . . . . . . . . . . . 14 (ℤ𝑚) ⊆ ℤ
118 zssre 11335 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
119117, 118sstri 3596 . . . . . . . . . . . . 13 (ℤ𝑚) ⊆ ℝ
120116, 119sstri 3596 . . . . . . . . . . . 12 (𝑚...𝑛) ⊆ ℝ
121115, 120syl6ss 3599 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
122 ltso 10069 . . . . . . . . . . 11 < Or ℝ
123 soss 5018 . . . . . . . . . . 11 (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
124121, 122, 123mpisyl 21 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
125 fzfi 12718 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
126125a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑀) ∈ Fin)
127 fex2 7075 . . . . . . . . . . . . . . 15 ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴𝑉) → 𝐻 ∈ V)
12812, 126, 2, 127syl3anc 1323 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ V)
129 f1oen3g 7922 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
130128, 15, 129syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ≈ ran 𝐻)
131 enfi 8127 . . . . . . . . . . . . 13 ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
132130, 131syl 17 . . . . . . . . . . . 12 (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
133125, 132mpbii 223 . . . . . . . . . . 11 (𝜑 → ran 𝐻 ∈ Fin)
134133ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
135 fz1iso 13191 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
136124, 134, 135syl2anc 692 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
13770nnnn0d 11302 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℕ0)
138 hashfz1 13081 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (#‘(1...𝑀)) = 𝑀)
139137, 138syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (#‘(1...𝑀)) = 𝑀)
140 hashen 13082 . . . . . . . . . . . . . . . . 17 (((1...𝑀) ∈ Fin ∧ ran 𝐻 ∈ Fin) → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
141125, 133, 140sylancr 694 . . . . . . . . . . . . . . . 16 (𝜑 → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻))
142130, 141mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → (#‘(1...𝑀)) = (#‘ran 𝐻))
143139, 142eqtr3d 2657 . . . . . . . . . . . . . 14 (𝜑𝑀 = (#‘ran 𝐻))
144143ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 = (#‘ran 𝐻))
145144fveq2d 6157 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝑓))‘𝑀) = (seq1( + , (𝐹𝑓))‘(#‘ran 𝐻)))
1461ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
14763, 66mndcl 17229 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
1481473expb 1263 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
149146, 148sylan 488 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
150 gsumval3.c . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
151150ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
152151sselda 3587 . . . . . . . . . . . . . . 15 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
153 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntz‘𝐺)
15466, 153cntzi 17690 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
155152, 154sylan 488 . . . . . . . . . . . . . 14 (((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
156155anasss 678 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
15763, 66mndass 17230 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
158146, 157sylan 488 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15972ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ‘1))
1607ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴𝐵)
161 frn 6015 . . . . . . . . . . . . . 14 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
162160, 161syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹𝐵)
163 simprr 795 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))
164 isof1o 6533 . . . . . . . . . . . . . . . . 17 (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻)
165163, 164syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻)
166144oveq2d 6626 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(#‘ran 𝐻)))
167 f1oeq2 6090 . . . . . . . . . . . . . . . . 17 ((1...𝑀) = (1...(#‘ran 𝐻)) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻))
168166, 167syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻))
169165, 168mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
170 f1ocnv 6111 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:ran 𝐻1-1-onto→(1...𝑀))
171169, 170syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻1-1-onto→(1...𝑀))
17215ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
173 f1oco 6121 . . . . . . . . . . . . . 14 ((𝑓:ran 𝐻1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
174171, 172, 173syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
175 ffn 6007 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
176 dffn4 6083 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
177175, 176sylib 208 . . . . . . . . . . . . . . . 16 (𝐹:𝐴𝐵𝐹:𝐴onto→ran 𝐹)
178 fof 6077 . . . . . . . . . . . . . . . 16 (𝐹:𝐴onto→ran 𝐹𝐹:𝐴⟶ran 𝐹)
179160, 177, 1783syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
180 f1of 6099 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...𝑀)⟶ran 𝐻)
181169, 180syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
182113ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻𝐴)
183181, 182fssd 6019 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
184 fco 6020 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ran 𝐹𝑓:(1...𝑀)⟶𝐴) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
185179, 183, 184syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
186185ffvelrnda 6320 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝑓)‘𝑥) ∈ ran 𝐹)
187 f1ococnv2 6125 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓𝑓) = ( I ↾ ran 𝐻))
188169, 187syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓𝑓) = ( I ↾ ran 𝐻))
189188coeq1d 5248 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝑓𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
190 f1of 6099 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:(1...𝑀)⟶ran 𝐻)
191 fcoi2 6041 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
192172, 190, 1913syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
193189, 192eqtr2d 2656 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓𝑓) ∘ 𝐻))
194 coass 5618 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑓) ∘ 𝐻) = (𝑓 ∘ (𝑓𝐻))
195193, 194syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (𝑓𝐻)))
196195coeq2d 5249 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻))))
197 coass 5618 . . . . . . . . . . . . . . . . 17 ((𝐹𝑓) ∘ (𝑓𝐻)) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻)))
198196, 197syl6eqr 2673 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = ((𝐹𝑓) ∘ (𝑓𝐻)))
199198fveq1d 6155 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
200199adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
201 f1of 6099 . . . . . . . . . . . . . . . . 17 (𝑓:ran 𝐻1-1-onto→(1...𝑀) → 𝑓:ran 𝐻⟶(1...𝑀))
202169, 170, 2013syl 18 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻⟶(1...𝑀))
203172, 190syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
204 fco 6020 . . . . . . . . . . . . . . . 16 ((𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
205202, 203, 204syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
206 fvco3 6237 . . . . . . . . . . . . . . 15 (((𝑓𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
207205, 206sylan 488 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
208200, 207eqtrd 2655 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
209149, 156, 158, 159, 162, 174, 186, 208seqf1o 12789 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹𝑓))‘𝑀))
21063, 66, 3mndlid 17239 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
211146, 210sylan 488 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
21263, 66, 3mndrid 17240 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
213146, 212sylan 488 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
214146, 64syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 0𝐵)
215 fdm 6013 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
21610, 11, 2153syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = (1...𝑀))
217 eluzfz1 12297 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
218 ne0i 3902 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
21972, 217, 2183syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ≠ ∅)
220216, 219eqnetrd 2857 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐻 ≠ ∅)
221 dm0rn0 5307 . . . . . . . . . . . . . . . 16 (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
222221necon3bii 2842 . . . . . . . . . . . . . . 15 (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
223220, 222sylib 208 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻 ≠ ∅)
224223ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
225115adantrr 752 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
226 simprl 793 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
227226eleq2d 2684 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥𝐴𝑥 ∈ (𝑚...𝑛)))
228227biimpar 502 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥𝐴)
229160ffvelrnda 6320 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
230228, 229syldan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹𝑥) ∈ 𝐵)
231226difeq1d 3710 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
232231eleq2d 2684 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
233232biimpar 502 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
234 simpll 789 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝜑)
235234, 53sylan 488 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
236233, 235syldan 487 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
237 f1of 6099 . . . . . . . . . . . . . . 15 (𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran 𝐻𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻)
238163, 164, 2373syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻)
239 fvco3 6237 . . . . . . . . . . . . . 14 ((𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
240238, 239sylan 488 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
241211, 213, 149, 214, 163, 224, 225, 230, 236, 240seqcoll2 13194 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹𝑓))‘(#‘ran 𝐻)))
242145, 209, 2413eqtr4d 2665 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
243242expr 642 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
244243exlimdv 1858 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
245136, 244mpd 15 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
246111, 245eqtr4d 2658 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
247246ex 450 . . . . . 6 ((𝜑𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
248247rexlimdvw 3028 . . . . 5 ((𝜑𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
249248rexlimdvw 3028 . . . 4 ((𝜑𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
25083, 249syl5bi 232 . . 3 ((𝜑𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
251 suppssdm 7260 . . . . . . . . . . 11 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
25232, 251eqsstri 3619 . . . . . . . . . 10 𝑊 ⊆ dom (𝐹𝐻)
253 fdm 6013 . . . . . . . . . . 11 ((𝐹𝐻):(1...𝑀)⟶𝐵 → dom (𝐹𝐻) = (1...𝑀))
25430, 253syl 17 . . . . . . . . . 10 (𝜑 → dom (𝐹𝐻) = (1...𝑀))
255252, 254syl5sseq 3637 . . . . . . . . 9 (𝜑𝑊 ⊆ (1...𝑀))
256 fzssuz 12331 . . . . . . . . . . 11 (1...𝑀) ⊆ (ℤ‘1)
257256, 71sseqtr4i 3622 . . . . . . . . . 10 (1...𝑀) ⊆ ℕ
258 nnssre 10975 . . . . . . . . . 10 ℕ ⊆ ℝ
259257, 258sstri 3596 . . . . . . . . 9 (1...𝑀) ⊆ ℝ
260255, 259syl6ss 3599 . . . . . . . 8 (𝜑𝑊 ⊆ ℝ)
261 soss 5018 . . . . . . . 8 (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
262260, 122, 261mpisyl 21 . . . . . . 7 (𝜑 → < Or 𝑊)
263 ssfi 8131 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
264125, 255, 263sylancr 694 . . . . . . 7 (𝜑𝑊 ∈ Fin)
265 fz1iso 13191 . . . . . . 7 (( < Or 𝑊𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
266262, 264, 265syl2anc 692 . . . . . 6 (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
267266ad2antrr 761 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
26863, 3, 66, 153, 1, 2, 7, 150, 70, 10, 51, 32gsumval3lem2 18235 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(#‘𝑊)))
2691ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
270269, 210sylan 488 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
271269, 212sylan 488 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
272269, 148sylan 488 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
273269, 64syl 17 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 0𝐵)
274 simprr 795 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))
275 simplr 791 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
276255ad2antrr 761 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
27730ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐹𝐻):(1...𝑀)⟶𝐵)
278277ffvelrnda 6320 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) ∈ 𝐵)
27933a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
28035a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
28138a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 0 ∈ V)
282277, 279, 280, 281suppssr 7278 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
283 coass 5618 . . . . . . . . . . 11 ((𝐹𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻𝑓))
284283fveq1i 6154 . . . . . . . . . 10 (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻𝑓))‘𝑦)
285 isof1o 6533 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → 𝑓:(1...(#‘𝑊))–1-1-onto𝑊)
286 f1of 6099 . . . . . . . . . . . 12 (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑓:(1...(#‘𝑊))⟶𝑊)
287274, 285, 2863syl 18 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝑊)
288 fvco3 6237 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝑊))⟶𝑊𝑦 ∈ (1...(#‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
289287, 288sylan 488 . . . . . . . . . 10 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
290284, 289syl5eqr 2669 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ (𝐻𝑓))‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
291270, 271, 272, 273, 274, 275, 276, 278, 282, 290seqcoll2 13194 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(#‘𝑊)))
292268, 291eqtr4d 2658 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
293292expr 642 . . . . . 6 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
294293exlimdv 1858 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
295267, 294mpd 15 . . . 4 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
296295ex 450 . . 3 ((𝜑𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
297250, 296pm2.61d 170 . 2 ((𝜑𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
29879, 297pm2.61dane 2877 1 (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wrex 2908  Vcvv 3189  cdif 3556  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153   class class class wbr 4618  cmpt 4678   I cid 4989   Or wor 4999   × cxp 5077  ccnv 5078  dom cdm 5079  ran crn 5080  cres 5081  ccom 5083  Rel wrel 5084   Fn wfn 5847  wf 5848  1-1wf1 5849  ontowfo 5850  1-1-ontowf1o 5851  cfv 5852   Isom wiso 5853  (class class class)co 6610   supp csupp 7247  cen 7903  Fincfn 7906  cr 9886  1c1 9888   < clt 10025  cn 10971  0cn0 11243  cz 11328  cuz 11638  ...cfz 12275  seqcseq 12748  #chash 13064  Basecbs 15788  +gcplusg 15869  0gc0g 16028   Σg cgsu 16029  Mndcmnd 17222  Cntzccntz 17676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-oi 8366  df-card 8716  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-fz 12276  df-fzo 12414  df-seq 12749  df-hash 13065  df-0g 16030  df-gsum 16031  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-cntz 17678
This theorem is referenced by:  gsumzres  18238  gsumzcl2  18239  gsumzf1o  18241  gsumzaddlem  18249  gsumconst  18262  gsumzmhm  18265  gsumzoppg  18272  gsumfsum  19741  wilthlem3  24709
  Copyright terms: Public domain W3C validator