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

Theorem gsumval3 19684
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 18646 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝐴𝑉) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
51, 2, 4syl2anc 584 . . . 4 (𝜑 → (𝐺 Σg (𝑥𝐴0 )) = 0 )
65adantr 481 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg (𝑥𝐴0 )) = 0 )
7 gsumval3.f . . . . . . 7 (𝜑𝐹:𝐴𝐵)
87feqmptd 6910 . . . . . 6 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
98adantr 481 . . . . 5 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
10 gsumval3.h . . . . . . . . . . . . . 14 (𝜑𝐻:(1...𝑀)–1-1𝐴)
11 f1f 6738 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1𝐴𝐻:(1...𝑀)⟶𝐴)
1210, 11syl 17 . . . . . . . . . . . . 13 (𝜑𝐻:(1...𝑀)⟶𝐴)
1312ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴)
14 f1f1orn 6795 . . . . . . . . . . . . . . . 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 6796 . . . . . . . . . . . . . 14 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:ran 𝐻1-1-onto→(1...𝑀))
18 f1of 6784 . . . . . . . . . . . . . 14 (𝐻:ran 𝐻1-1-onto→(1...𝑀) → 𝐻:ran 𝐻⟶(1...𝑀))
1916, 17, 183syl 18 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 𝐻:ran 𝐻⟶(1...𝑀))
2019ffvelcdmda 7035 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ (1...𝑀))
21 fvco3 6940 . . . . . . . . . . . 12 ((𝐻:(1...𝑀)⟶𝐴 ∧ (𝐻𝑥) ∈ (1...𝑀)) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
2213, 20, 21syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = (𝐹‘(𝐻‘(𝐻𝑥))))
23 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑊 = ∅) → 𝑊 = ∅)
2423difeq2d 4082 . . . . . . . . . . . . . . 15 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅))
25 dif0 4332 . . . . . . . . . . . . . . 15 ((1...𝑀) ∖ ∅) = (1...𝑀)
2624, 25eqtrdi 2792 . . . . . . . . . . . . . 14 ((𝜑𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2726adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀))
2820, 27eleqtrrd 2841 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊))
29 fco 6692 . . . . . . . . . . . . . . 15 ((𝐹:𝐴𝐵𝐻:(1...𝑀)⟶𝐴) → (𝐹𝐻):(1...𝑀)⟶𝐵)
307, 12, 29syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐻):(1...𝑀)⟶𝐵)
3130adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (𝐹𝐻):(1...𝑀)⟶𝐵)
32 gsumval3.w . . . . . . . . . . . . . . 15 𝑊 = ((𝐹𝐻) supp 0 )
3332eqimss2i 4003 . . . . . . . . . . . . . 14 ((𝐹𝐻) supp 0 ) ⊆ 𝑊
3433a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
35 ovexd 7392 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → (1...𝑀) ∈ V)
363fvexi 6856 . . . . . . . . . . . . . 14 0 ∈ V
3736a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑊 = ∅) → 0 ∈ V)
3831, 34, 35, 37suppssr 8127 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ (𝐻𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
3928, 38syldan 591 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹𝐻)‘(𝐻𝑥)) = 0 )
40 f1ocnvfv2 7223 . . . . . . . . . . . . 13 ((𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4116, 40sylan 580 . . . . . . . . . . . 12 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(𝐻𝑥)) = 𝑥)
4241fveq2d 6846 . . . . . . . . . . 11 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(𝐻𝑥))) = (𝐹𝑥))
4322, 39, 423eqtr3rd 2785 . . . . . . . . . 10 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) = 0 )
44 fvex 6855 . . . . . . . . . . 11 (𝐹𝑥) ∈ V
4544elsn 4601 . . . . . . . . . 10 ((𝐹𝑥) ∈ { 0 } ↔ (𝐹𝑥) = 0 )
4643, 45sylibr 233 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
4746adantlr 713 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
48 eldif 3920 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻))
49 gsumval3.n . . . . . . . . . . . . 13 (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻)
5036a1i 11 . . . . . . . . . . . . 13 (𝜑0 ∈ V)
517, 49, 2, 50suppssr 8127 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
5251, 45sylibr 233 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5348, 52sylan2br 595 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5453adantlr 713 . . . . . . . . 9 (((𝜑𝑊 = ∅) ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹𝑥) ∈ { 0 })
5554anassrs 468 . . . . . . . 8 ((((𝜑𝑊 = ∅) ∧ 𝑥𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹𝑥) ∈ { 0 })
5647, 55pm2.61dan 811 . . . . . . 7 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ { 0 })
5756, 45sylib 217 . . . . . 6 (((𝜑𝑊 = ∅) ∧ 𝑥𝐴) → (𝐹𝑥) = 0 )
5857mpteq2dva 5205 . . . . 5 ((𝜑𝑊 = ∅) → (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴0 ))
599, 58eqtrd 2776 . . . 4 ((𝜑𝑊 = ∅) → 𝐹 = (𝑥𝐴0 ))
6059oveq2d 7373 . . 3 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝐴0 )))
61 gsumval3.b . . . . . . 7 𝐵 = (Base‘𝐺)
6261, 3mndidcl 18571 . . . . . 6 (𝐺 ∈ Mnd → 0𝐵)
63 gsumval3.p . . . . . . 7 + = (+g𝐺)
6461, 63, 3mndlid 18576 . . . . . 6 ((𝐺 ∈ Mnd ∧ 0𝐵) → ( 0 + 0 ) = 0 )
651, 62, 64syl2anc2 585 . . . . 5 (𝜑 → ( 0 + 0 ) = 0 )
6665adantr 481 . . . 4 ((𝜑𝑊 = ∅) → ( 0 + 0 ) = 0 )
67 gsumval3.m . . . . . 6 (𝜑𝑀 ∈ ℕ)
68 nnuz 12806 . . . . . 6 ℕ = (ℤ‘1)
6967, 68eleqtrdi 2848 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
7069adantr 481 . . . 4 ((𝜑𝑊 = ∅) → 𝑀 ∈ (ℤ‘1))
7126eleq2d 2823 . . . . . 6 ((𝜑𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀)))
7271biimpar 478 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊))
7331, 34, 35, 37suppssr 8127 . . . . 5 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
7472, 73syldan 591 . . . 4 (((𝜑𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) = 0 )
7566, 70, 74seqid3 13952 . . 3 ((𝜑𝑊 = ∅) → (seq1( + , (𝐹𝐻))‘𝑀) = 0 )
766, 60, 753eqtr4d 2786 . 2 ((𝜑𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
77 fzf 13428 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
78 ffn 6668 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
79 ovelrn 7530 . . . . 5 (... Fn (ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛)))
8077, 78, 79mp2b 10 . . . 4 (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))
811ad2antrr 724 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd)
82 simpr 485 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛))
83 frel 6673 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵 → Rel 𝐹)
84 reldm0 5883 . . . . . . . . . . . . . . . . 17 (Rel 𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
857, 83, 843syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅))
867fdmd 6679 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐴)
8786eqeq1d 2738 . . . . . . . . . . . . . . . 16 (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅))
8885, 87bitrd 278 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅))
89 coeq1 5813 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ∅ → (𝐹𝐻) = (∅ ∘ 𝐻))
90 co01 6213 . . . . . . . . . . . . . . . . . . 19 (∅ ∘ 𝐻) = ∅
9189, 90eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 (𝐹 = ∅ → (𝐹𝐻) = ∅)
9291oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = (∅ supp 0 ))
93 supp0 8097 . . . . . . . . . . . . . . . . . 18 ( 0 ∈ V → (∅ supp 0 ) = ∅)
9436, 93ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ supp 0 ) = ∅
9592, 94eqtrdi 2792 . . . . . . . . . . . . . . . 16 (𝐹 = ∅ → ((𝐹𝐻) supp 0 ) = ∅)
9632, 95eqtrid 2788 . . . . . . . . . . . . . . 15 (𝐹 = ∅ → 𝑊 = ∅)
9788, 96syl6bir 253 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑊 = ∅))
9897necon3d 2964 . . . . . . . . . . . . 13 (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅))
9998imp 407 . . . . . . . . . . . 12 ((𝜑𝑊 ≠ ∅) → 𝐴 ≠ ∅)
10099adantr 481 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅)
10182, 100eqnetrrd 3012 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅)
102 fzn0 13455 . . . . . . . . . 10 ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ𝑚))
103101, 102sylib 217 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ𝑚))
1047ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴𝐵)
10582feq2d 6654 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴𝐵𝐹:(𝑚...𝑛)⟶𝐵))
106104, 105mpbid 231 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵)
10761, 63, 81, 103, 106gsumval2 18541 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛))
108 frn 6675 . . . . . . . . . . . . . . 15 (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻𝐴)
10910, 11, 1083syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻𝐴)
110109ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻𝐴)
111110, 82sseqtrd 3984 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛))
112 fzssuz 13482 . . . . . . . . . . . . 13 (𝑚...𝑛) ⊆ (ℤ𝑚)
113 uzssz 12784 . . . . . . . . . . . . . 14 (ℤ𝑚) ⊆ ℤ
114 zssre 12506 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
115113, 114sstri 3953 . . . . . . . . . . . . 13 (ℤ𝑚) ⊆ ℝ
116112, 115sstri 3953 . . . . . . . . . . . 12 (𝑚...𝑛) ⊆ ℝ
117111, 116sstrdi 3956 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ)
118 ltso 11235 . . . . . . . . . . 11 < Or ℝ
119 soss 5565 . . . . . . . . . . 11 (ran 𝐻 ⊆ ℝ → ( < Or ℝ → < Or ran 𝐻))
120117, 118, 119mpisyl 21 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻)
121 fzfi 13877 . . . . . . . . . . . 12 (1...𝑀) ∈ Fin
122121a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑀) ∈ Fin)
12312, 122fexd 7177 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ V)
124 f1oen3g 8906 . . . . . . . . . . . . . 14 ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (1...𝑀) ≈ ran 𝐻)
125123, 15, 124syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ≈ ran 𝐻)
126 enfi 9134 . . . . . . . . . . . . 13 ((1...𝑀) ≈ ran 𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
127125, 126syl 17 . . . . . . . . . . . 12 (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin))
128121, 127mpbii 232 . . . . . . . . . . 11 (𝜑 → ran 𝐻 ∈ Fin)
129128ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin)
130 fz1iso 14361 . . . . . . . . . 10 (( < Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
131120, 129, 130syl2anc 584 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
13267nnnn0d 12473 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℕ0)
133 hashfz1 14246 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
134132, 133syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(1...𝑀)) = 𝑀)
135122, 15hasheqf1od 14253 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻))
136134, 135eqtr3d 2778 . . . . . . . . . . . . . 14 (𝜑𝑀 = (♯‘ran 𝐻))
137136ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻))
138137fveq2d 6846 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝑓))‘𝑀) = (seq1( + , (𝐹𝑓))‘(♯‘ran 𝐻)))
1391ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd)
14061, 63mndcl 18564 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
1411403expb 1120 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
142139, 141sylan 580 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
143 gsumval3.c . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
144143ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
145144sselda 3944 . . . . . . . . . . . . . . 15 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹))
146 gsumval3.z . . . . . . . . . . . . . . . 16 𝑍 = (Cntz‘𝐺)
14763, 146cntzi 19109 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
148145, 147sylan 580 . . . . . . . . . . . . . 14 (((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
149148anasss 467 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
15061, 63mndass 18565 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
151139, 150sylan 580 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15269ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈ (ℤ‘1))
1537ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴𝐵)
154153frnd 6676 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐹𝐵)
155 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))
156 isof1o 7268 . . . . . . . . . . . . . . . . 17 (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
157155, 156syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻)
158137oveq2d 7373 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻)))
159158f1oeq2d 6780 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻))
160157, 159mpbird 256 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran 𝐻)
161 f1ocnv 6796 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:ran 𝐻1-1-onto→(1...𝑀))
162160, 161syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻1-1-onto→(1...𝑀))
16315ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran 𝐻)
164 f1oco 6807 . . . . . . . . . . . . . 14 ((𝑓:ran 𝐻1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran 𝐻) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
165162, 163, 164syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)–1-1-onto→(1...𝑀))
166 ffn 6668 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
167 dffn4 6762 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴𝐹:𝐴onto→ran 𝐹)
168166, 167sylib 217 . . . . . . . . . . . . . . . 16 (𝐹:𝐴𝐵𝐹:𝐴onto→ran 𝐹)
169 fof 6756 . . . . . . . . . . . . . . . 16 (𝐹:𝐴onto→ran 𝐹𝐹:𝐴⟶ran 𝐹)
170153, 168, 1693syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹)
171 f1of 6784 . . . . . . . . . . . . . . . . 17 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻𝑓:(1...𝑀)⟶ran 𝐻)
172160, 171syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻)
173109ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻𝐴)
174172, 173fssd 6686 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴)
175 fco 6692 . . . . . . . . . . . . . . 15 ((𝐹:𝐴⟶ran 𝐹𝑓:(1...𝑀)⟶𝐴) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
176170, 174, 175syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝑓):(1...𝑀)⟶ran 𝐹)
177176ffvelcdmda 7035 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝑓)‘𝑥) ∈ ran 𝐹)
178 f1ococnv2 6811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:(1...𝑀)–1-1-onto→ran 𝐻 → (𝑓𝑓) = ( I ↾ ran 𝐻))
179160, 178syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝑓) = ( I ↾ ran 𝐻))
180179coeq1d 5817 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝑓𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻))
181 f1of 6784 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)–1-1-onto→ran 𝐻𝐻:(1...𝑀)⟶ran 𝐻)
182 fcoi2 6717 . . . . . . . . . . . . . . . . . . . . 21 (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
183163, 181, 1823syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻)
184180, 183eqtr2d 2777 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓𝑓) ∘ 𝐻))
185 coass 6217 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑓) ∘ 𝐻) = (𝑓 ∘ (𝑓𝐻))
186184, 185eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (𝑓𝐻)))
187186coeq2d 5818 . . . . . . . . . . . . . . . . 17 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻))))
188 coass 6217 . . . . . . . . . . . . . . . . 17 ((𝐹𝑓) ∘ (𝑓𝐻)) = (𝐹 ∘ (𝑓 ∘ (𝑓𝐻)))
189187, 188eqtr4di 2794 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐹𝐻) = ((𝐹𝑓) ∘ (𝑓𝐻)))
190189fveq1d 6844 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
191190adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘))
192 f1of 6784 . . . . . . . . . . . . . . . . 17 (𝑓:ran 𝐻1-1-onto→(1...𝑀) → 𝑓:ran 𝐻⟶(1...𝑀))
193160, 161, 1923syl 18 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:ran 𝐻⟶(1...𝑀))
194163, 181syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻)
195 fco 6692 . . . . . . . . . . . . . . . 16 ((𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
196193, 194, 195syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑓𝐻):(1...𝑀)⟶(1...𝑀))
197 fvco3 6940 . . . . . . . . . . . . . . 15 (((𝑓𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
198196, 197sylan 580 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹𝑓) ∘ (𝑓𝐻))‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
199191, 198eqtrd 2776 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑘) = ((𝐹𝑓)‘((𝑓𝐻)‘𝑘)))
200142, 149, 151, 152, 154, 165, 177, 199seqf1o 13949 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹𝑓))‘𝑀))
20161, 63, 3mndlid 18576 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
202139, 201sylan 580 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
20361, 63, 3mndrid 18577 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
204139, 203sylan 580 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
205139, 62syl 17 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 0𝐵)
206 fdm 6677 . . . . . . . . . . . . . . . . 17 (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀))
20710, 11, 2063syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐻 = (1...𝑀))
208 eluzfz1 13448 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
209 ne0i 4294 . . . . . . . . . . . . . . . . 17 (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
21069, 208, 2093syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ≠ ∅)
211207, 210eqnetrd 3011 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐻 ≠ ∅)
212 dm0rn0 5880 . . . . . . . . . . . . . . . 16 (dom 𝐻 = ∅ ↔ ran 𝐻 = ∅)
213212necon3bii 2996 . . . . . . . . . . . . . . 15 (dom 𝐻 ≠ ∅ ↔ ran 𝐻 ≠ ∅)
214211, 213sylib 217 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐻 ≠ ∅)
215214ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅)
216111adantrr 715 . . . . . . . . . . . . 13 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛))
217 simprl 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛))
218217eleq2d 2823 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥𝐴𝑥 ∈ (𝑚...𝑛)))
219218biimpar 478 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥𝐴)
220153ffvelcdmda 7035 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
221219, 220syldan 591 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹𝑥) ∈ 𝐵)
222217difeq1d 4081 . . . . . . . . . . . . . . . 16 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻))
223222eleq2d 2823 . . . . . . . . . . . . . . 15 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)))
224223biimpar 478 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻))
22551ad4ant14 750 . . . . . . . . . . . . . 14 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
226224, 225syldan 591 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹𝑥) = 0 )
227 f1of 6784 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran 𝐻𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
228155, 156, 2273syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻)
229 fvco3 6940 . . . . . . . . . . . . . 14 ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
230228, 229sylan 580 . . . . . . . . . . . . 13 ((((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹𝑓)‘𝑦) = (𝐹‘(𝑓𝑦)))
231202, 204, 142, 205, 155, 215, 216, 221, 226, 230seqcoll2 14364 . . . . . . . . . . . 12 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹𝑓))‘(♯‘ran 𝐻)))
232138, 200, 2313eqtr4d 2786 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
233232expr 457 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
234233exlimdv 1936 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)))
235131, 234mpd 15 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))
236107, 235eqtr4d 2779 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
237236ex 413 . . . . . 6 ((𝜑𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
238237rexlimdvw 3157 . . . . 5 ((𝜑𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
239238rexlimdvw 3157 . . . 4 ((𝜑𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
24080, 239biimtrid 241 . . 3 ((𝜑𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
241 suppssdm 8108 . . . . . . . . . . 11 ((𝐹𝐻) supp 0 ) ⊆ dom (𝐹𝐻)
24232, 241eqsstri 3978 . . . . . . . . . 10 𝑊 ⊆ dom (𝐹𝐻)
243242, 30fssdm 6688 . . . . . . . . 9 (𝜑𝑊 ⊆ (1...𝑀))
244 fz1ssnn 13472 . . . . . . . . . 10 (1...𝑀) ⊆ ℕ
245 nnssre 12157 . . . . . . . . . 10 ℕ ⊆ ℝ
246244, 245sstri 3953 . . . . . . . . 9 (1...𝑀) ⊆ ℝ
247243, 246sstrdi 3956 . . . . . . . 8 (𝜑𝑊 ⊆ ℝ)
248 soss 5565 . . . . . . . 8 (𝑊 ⊆ ℝ → ( < Or ℝ → < Or 𝑊))
249247, 118, 248mpisyl 21 . . . . . . 7 (𝜑 → < Or 𝑊)
250 ssfi 9117 . . . . . . . 8 (((1...𝑀) ∈ Fin ∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin)
251121, 243, 250sylancr 587 . . . . . . 7 (𝜑𝑊 ∈ Fin)
252 fz1iso 14361 . . . . . . 7 (( < Or 𝑊𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
253249, 251, 252syl2anc 584 . . . . . 6 (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
254253ad2antrr 724 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
25561, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32gsumval3lem2 19683 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(♯‘𝑊)))
2561ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd)
257256, 201sylan 580 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
258256, 203sylan 580 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥𝐵) → (𝑥 + 0 ) = 𝑥)
259256, 141sylan 580 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
260256, 62syl 17 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0𝐵)
261 simprr 771 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))
262 simplr 767 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ≠ ∅)
263243ad2antrr 724 . . . . . . . . 9 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀))
26430ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐹𝐻):(1...𝑀)⟶𝐵)
265264ffvelcdmda 7035 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹𝐻)‘𝑥) ∈ 𝐵)
26633a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → ((𝐹𝐻) supp 0 ) ⊆ 𝑊)
267 ovexd 7392 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (1...𝑀) ∈ V)
26836a1i 11 . . . . . . . . . 10 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 0 ∈ V)
269264, 266, 267, 268suppssr 8127 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹𝐻)‘𝑥) = 0 )
270 coass 6217 . . . . . . . . . . 11 ((𝐹𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻𝑓))
271270fveq1i 6843 . . . . . . . . . 10 (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻𝑓))‘𝑦)
272 isof1o 7268 . . . . . . . . . . . 12 (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto𝑊)
273 f1of 6784 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑓:(1...(♯‘𝑊))⟶𝑊)
274261, 272, 2733syl 18 . . . . . . . . . . 11 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊)
275 fvco3 6940 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝑊))⟶𝑊𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
276274, 275sylan 580 . . . . . . . . . 10 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹𝐻) ∘ 𝑓)‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
277271, 276eqtr3id 2790 . . . . . . . . 9 ((((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ (𝐻𝑓))‘𝑦) = ((𝐹𝐻)‘(𝑓𝑦)))
278257, 258, 259, 260, 261, 262, 263, 265, 269, 277seqcoll2 14364 . . . . . . . 8 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (seq1( + , (𝐹𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻𝑓)))‘(♯‘𝑊)))
279255, 278eqtr4d 2779 . . . . . . 7 (((𝜑𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
280279expr 457 . . . . . 6 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
281280exlimdv 1936 . . . . 5 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
282254, 281mpd 15 . . . 4 (((𝜑𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
283282ex 413 . . 3 ((𝜑𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀)))
284240, 283pm2.61d 179 . 2 ((𝜑𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
28576, 284pm2.61dane 3032 1 (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹𝐻))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wrex 3073  Vcvv 3445  cdif 3907  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   class class class wbr 5105  cmpt 5188   I cid 5530   Or wor 5544   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  ccom 5637  Rel wrel 5638   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496   Isom wiso 6497  (class class class)co 7357   supp csupp 8092  cen 8880  Fincfn 8883  cr 11050  1c1 11052   < clt 11189  cn 12153  0cn0 12413  cz 12499  cuz 12763  ...cfz 13424  seqcseq 13906  chash 14230  Basecbs 17083  +gcplusg 17133  0gc0g 17321   Σg cgsu 17322  Mndcmnd 18556  Cntzccntz 19095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-0g 17323  df-gsum 17324  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-cntz 19097
This theorem is referenced by:  gsumzres  19686  gsumzcl2  19687  gsumzf1o  19689  gsumzaddlem  19698  gsumconst  19711  gsumzmhm  19714  gsumzoppg  19721  gsumfsum  20864  wilthlem3  26419
  Copyright terms: Public domain W3C validator