Step | Hyp | Ref
| Expression |
1 | | gsumval3.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumval3.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | gsumval3.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
4 | 3 | gsumz 17854 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 576 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
6 | 5 | adantr 473 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
7 | | gsumval3.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
8 | 7 | feqmptd 6560 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
9 | 8 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
10 | | gsumval3.h |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
11 | | f1f 6401 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
13 | 12 | ad2antrr 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴) |
14 | | f1f1orn 6452 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
16 | 15 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
17 | | f1ocnv 6453 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀)) |
18 | | f1of 6441 |
. . . . . . . . . . . . . 14
⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
20 | 19 | ffvelrnda 6674 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀)) |
21 | | fvco3 6586 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
22 | 13, 20, 21 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
23 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅) |
24 | 23 | difeq2d 3982 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅)) |
25 | | dif0 4212 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∖
∅) = (1...𝑀) |
26 | 24, 25 | syl6eq 2823 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
27 | 26 | adantr 473 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
28 | 20, 27 | eleqtrrd 2862 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) |
29 | | fco 6358 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
30 | 7, 12, 29 | syl2anc 576 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
31 | 30 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
32 | | gsumval3.w |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
33 | 32 | eqimss2i 3909 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊 |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
35 | | ovexd 7008 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V) |
36 | 3 | fvexi 6510 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V) |
38 | 31, 34, 35, 37 | suppssr 7662 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
39 | 28, 38 | syldan 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
40 | | f1ocnvfv2 6857 |
. . . . . . . . . . . . 13
⊢ ((𝐻:(1...𝑀)–1-1-onto→ran
𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
41 | 16, 40 | sylan 572 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
42 | 41 | fveq2d 6500 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥)) |
43 | 22, 39, 42 | 3eqtr3rd 2816 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 ) |
44 | | fvex 6509 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
45 | 44 | elsn 4450 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 ) |
46 | 43, 45 | sylibr 226 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
47 | 46 | adantlr 703 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
48 | | eldif 3832 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) |
49 | | gsumval3.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
50 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ V) |
51 | 7, 49, 2, 50 | suppssr 7662 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
52 | 51, 45 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
53 | 48, 52 | sylan2br 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
54 | 53 | adantlr 703 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
55 | 54 | anassrs 460 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
56 | 47, 55 | pm2.61dan 801 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 }) |
57 | 56, 45 | sylib 210 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 ) |
58 | 57 | mpteq2dva 5018 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 )) |
59 | 9, 58 | eqtrd 2807 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
60 | 59 | oveq2d 6990 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
61 | | gsumval3.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
62 | 61, 3 | mndidcl 17788 |
. . . . . 6
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
63 | | gsumval3.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
64 | 61, 63, 3 | mndlid 17791 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
65 | 1, 62, 64 | syl2anc2 577 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
66 | 65 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
67 | | gsumval3.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
68 | | nnuz 12093 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
69 | 67, 68 | syl6eleq 2869 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
70 | 69 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈
(ℤ≥‘1)) |
71 | 26 | eleq2d 2844 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀))) |
72 | 71 | biimpar 470 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) |
73 | 31, 34, 35, 37 | suppssr 7662 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
74 | 72, 73 | syldan 583 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
75 | 66, 70, 74 | seqid3 13227 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 ) |
76 | 6, 60, 75 | 3eqtr4d 2817 |
. 2
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
77 | | fzf 12710 |
. . . . 5
⊢
...:(ℤ × ℤ)⟶𝒫 ℤ |
78 | | ffn 6341 |
. . . . 5
⊢
(...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn
(ℤ × ℤ)) |
79 | | ovelrn 7138 |
. . . . 5
⊢ (... Fn
(ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))) |
80 | 77, 78, 79 | mp2b 10 |
. . . 4
⊢ (𝐴 ∈ ran ... ↔
∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
𝐴 = (𝑚...𝑛)) |
81 | 1 | ad2antrr 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd) |
82 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛)) |
83 | | frel 6346 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
84 | | reldm0 5638 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
85 | 7, 83, 84 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
86 | 7 | fdmd 6350 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐴) |
87 | 86 | eqeq1d 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅)) |
88 | 85, 87 | bitrd 271 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅)) |
89 | | coeq1 5574 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻)) |
90 | | co01 5950 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
∘ 𝐻) =
∅ |
91 | 89, 90 | syl6eq 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅) |
92 | 91 | oveq1d 6989 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0
)) |
93 | | supp0 7636 |
. . . . . . . . . . . . . . . . . 18
⊢ ( 0 ∈ V
→ (∅ supp 0 ) =
∅) |
94 | 36, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
supp 0 )
= ∅ |
95 | 92, 94 | syl6eq 2823 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅) |
96 | 32, 95 | syl5eq 2819 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = ∅ → 𝑊 = ∅) |
97 | 88, 96 | syl6bir 246 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅)) |
98 | 97 | necon3d 2981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅)) |
99 | 98 | imp 398 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅) |
100 | 99 | adantr 473 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅) |
101 | 82, 100 | eqnetrrd 3028 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅) |
102 | | fzn0 12735 |
. . . . . . . . . 10
⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚)) |
103 | 101, 102 | sylib 210 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚)) |
104 | 7 | ad2antrr 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵) |
105 | 82 | feq2d 6327 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵)) |
106 | 104, 105 | mpbid 224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵) |
107 | 61, 63, 81, 103, 106 | gsumval2 17760 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛)) |
108 | | frn 6347 |
. . . . . . . . . . . . . . 15
⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴) |
109 | 10, 11, 108 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) |
110 | 109 | ad2antrr 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴) |
111 | 110, 82 | sseqtrd 3890 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛)) |
112 | | fzssuz 12762 |
. . . . . . . . . . . . 13
⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚) |
113 | | uzssz 12076 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑚) ⊆ ℤ |
114 | | zssre 11798 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
115 | 113, 114 | sstri 3860 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑚) ⊆ ℝ |
116 | 112, 115 | sstri 3860 |
. . . . . . . . . . . 12
⊢ (𝑚...𝑛) ⊆ ℝ |
117 | 111, 116 | syl6ss 3863 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ) |
118 | | ltso 10519 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
119 | | soss 5341 |
. . . . . . . . . . 11
⊢ (ran
𝐻 ⊆ ℝ → (
< Or ℝ → < Or ran 𝐻)) |
120 | 117, 118,
119 | mpisyl 21 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻) |
121 | | fzfi 13153 |
. . . . . . . . . . . 12
⊢
(1...𝑀) ∈
Fin |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
123 | | fex2 7451 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
124 | 12, 122, 2, 123 | syl3anc 1352 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ V) |
125 | | f1oen3g 8320 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) |
126 | 124, 15, 125 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) |
127 | | enfi 8527 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
129 | 121, 128 | mpbii 225 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
130 | 129 | ad2antrr 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin) |
131 | | fz1iso 13631 |
. . . . . . . . . 10
⊢ (( <
Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
132 | 120, 130,
131 | syl2anc 576 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
133 | 67 | nnnn0d 11765 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
134 | | hashfz1 13519 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
136 | 122, 15 | hasheqf1od 13527 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻)) |
137 | 135, 136 | eqtr3d 2809 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻)) |
138 | 137 | ad2antrr 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻)) |
139 | 138 | fveq2d 6500 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻))) |
140 | 1 | ad2antrr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd) |
141 | 61, 63 | mndcl 17781 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
142 | 141 | 3expb 1101 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
143 | 140, 142 | sylan 572 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
144 | | gsumval3.c |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
145 | 144 | ad2antrr 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
146 | 145 | sselda 3851 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹)) |
147 | | gsumval3.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 = (Cntz‘𝐺) |
148 | 63, 147 | cntzi 18242 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
149 | 146, 148 | sylan 572 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
150 | 149 | anasss 459 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
151 | 61, 63 | mndass 17782 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
152 | 140, 151 | sylan 572 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
153 | 69 | ad2antrr 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑀 ∈
(ℤ≥‘1)) |
154 | 7 | ad2antrr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵) |
155 | 154 | frnd 6348 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵) |
156 | | simprr 761 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
157 | | isof1o 6897 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Isom < , <
((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻) |
159 | 138 | oveq2d 6990 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻))) |
160 | 159 | f1oeq2d 6437 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻)) |
161 | 158, 160 | mpbird 249 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran
𝐻) |
162 | | f1ocnv 6453 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
164 | 15 | ad2antrr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
165 | | f1oco 6463 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
166 | 163, 164,
165 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
167 | | ffn 6341 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
168 | | dffn4 6422 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
169 | 167, 168 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
170 | | fof 6416 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹) |
171 | 154, 169,
170 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹) |
172 | | f1of 6441 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻) |
173 | 161, 172 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻) |
174 | 109 | ad2antrr 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴) |
175 | 173, 174 | fssd 6355 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴) |
176 | | fco 6358 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
177 | 171, 175,
176 | syl2anc 576 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
178 | 177 | ffvelrnda 6674 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹) |
179 | | f1ococnv2 6467 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
180 | 161, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
181 | 180 | coeq1d 5578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻)) |
182 | | f1of 6441 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻) |
183 | | fcoi2 6379 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
184 | 164, 182,
183 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
185 | 181, 184 | eqtr2d 2808 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻)) |
186 | | coass 5954 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻)) |
187 | 185, 186 | syl6eq 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
188 | 187 | coeq2d 5579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))) |
189 | | coass 5954 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
190 | 188, 189 | syl6eqr 2825 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))) |
191 | 190 | fveq1d 6498 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
192 | 191 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
193 | | f1of 6441 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
194 | 161, 162,
193 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
195 | 164, 182 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻) |
196 | | fco 6358 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
197 | 194, 195,
196 | syl2anc 576 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
198 | | fvco3 6586 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
199 | 197, 198 | sylan 572 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
200 | 192, 199 | eqtrd 2807 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
201 | 143, 150,
152, 153, 155, 166, 178, 200 | seqf1o 13224 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀)) |
202 | 61, 63, 3 | mndlid 17791 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
203 | 140, 202 | sylan 572 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
204 | 61, 63, 3 | mndrid 17792 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
205 | 140, 204 | sylan 572 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
206 | 140, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 0 ∈ 𝐵) |
207 | | fdm 6349 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀)) |
208 | 10, 11, 207 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = (1...𝑀)) |
209 | | eluzfz1 12728 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
210 | | ne0i 4180 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
(1...𝑀) → (1...𝑀) ≠ ∅) |
211 | 69, 209, 210 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ≠ ∅) |
212 | 208, 211 | eqnetrd 3027 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐻 ≠ ∅) |
213 | | dm0rn0 5637 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐻 = ∅ ↔ ran
𝐻 =
∅) |
214 | 213 | necon3bii 3012 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐻 ≠ ∅ ↔ ran
𝐻 ≠
∅) |
215 | 212, 214 | sylib 210 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ≠ ∅) |
216 | 215 | ad2antrr 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅) |
217 | 111 | adantrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛)) |
218 | | simprl 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛)) |
219 | 218 | eleq2d 2844 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛))) |
220 | 219 | biimpar 470 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴) |
221 | 154 | ffvelrnda 6674 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
222 | 220, 221 | syldan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵) |
223 | 218 | difeq1d 3981 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻)) |
224 | 223 | eleq2d 2844 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻))) |
225 | 224 | biimpar 470 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻)) |
226 | 51 | ad4ant14 740 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
227 | 225, 226 | syldan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
228 | | f1of 6441 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻 → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻) |
229 | 156, 157,
228 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻) |
230 | | fvco3 6586 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
231 | 229, 230 | sylan 572 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
232 | 203, 205,
143, 206, 156, 216, 217, 222, 227, 231 | seqcoll2 13634 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻))) |
233 | 139, 201,
232 | 3eqtr4d 2817 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
234 | 233 | expr 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
235 | 234 | exlimdv 1893 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
236 | 132, 235 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
237 | 107, 236 | eqtr4d 2810 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
238 | 237 | ex 405 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
239 | 238 | rexlimdvw 3228 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
240 | 239 | rexlimdvw 3228 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
241 | 80, 240 | syl5bi 234 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
242 | | suppssdm 7644 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
243 | 32, 242 | eqsstri 3884 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
244 | 243, 30 | fssdm 6357 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
245 | | fz1ssnn 12752 |
. . . . . . . . . 10
⊢
(1...𝑀) ⊆
ℕ |
246 | | nnssre 11441 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ |
247 | 245, 246 | sstri 3860 |
. . . . . . . . 9
⊢
(1...𝑀) ⊆
ℝ |
248 | 244, 247 | syl6ss 3863 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ ℝ) |
249 | | soss 5341 |
. . . . . . . 8
⊢ (𝑊 ⊆ ℝ → ( <
Or ℝ → < Or 𝑊)) |
250 | 248, 118,
249 | mpisyl 21 |
. . . . . . 7
⊢ (𝜑 → < Or 𝑊) |
251 | | ssfi 8531 |
. . . . . . . 8
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
252 | 121, 244,
251 | sylancr 579 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) |
253 | | fz1iso 13631 |
. . . . . . 7
⊢ (( <
Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
254 | 250, 252,
253 | syl2anc 576 |
. . . . . 6
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
255 | 254 | ad2antrr 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
256 | 61, 3, 63, 147, 1, 2, 7, 144, 67, 10, 49, 32 | gsumval3lem2 18792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |
257 | 1 | ad2antrr 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐺 ∈ Mnd) |
258 | 257, 202 | sylan 572 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
259 | 257, 204 | sylan 572 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
260 | 257, 142 | sylan 572 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
261 | 257, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 0 ∈ 𝐵) |
262 | | simprr 761 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊)) |
263 | | simplr 757 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ≠ ∅) |
264 | 244 | ad2antrr 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) |
265 | 30 | ad2antrr 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
266 | 265 | ffvelrnda 6674 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵) |
267 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
268 | | ovexd 7008 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (1...𝑀) ∈ V) |
269 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 0 ∈
V) |
270 | 265, 267,
268, 269 | suppssr 7662 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
271 | | coass 5954 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓)) |
272 | 271 | fveq1i 6497 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) |
273 | | isof1o 6897 |
. . . . . . . . . . . 12
⊢ (𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
274 | | f1of 6441 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
275 | 262, 273,
274 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
276 | | fvco3 6586 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
277 | 275, 276 | sylan 572 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑦 ∈
(1...(♯‘𝑊)))
→ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
278 | 272, 277 | syl5eqr 2821 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑦 ∈
(1...(♯‘𝑊)))
→ ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
279 | 258, 259,
260, 261, 262, 263, 264, 266, 270, 278 | seqcoll2 13634 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |
280 | 256, 279 | eqtr4d 2810 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
281 | 280 | expr 449 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
282 | 281 | exlimdv 1893 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
283 | 255, 282 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
284 | 283 | ex 405 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
285 | 241, 284 | pm2.61d 172 |
. 2
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
286 | 76, 285 | pm2.61dane 3048 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |