Step | Hyp | Ref
| Expression |
1 | | gsumval3.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumval3.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | gsumval3.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
4 | 3 | gsumz 18262 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
6 | 5 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
7 | | gsumval3.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
8 | 7 | feqmptd 6780 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
10 | | gsumval3.h |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
11 | | f1f 6615 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
13 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴) |
14 | | f1f1orn 6672 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
16 | 15 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
17 | | f1ocnv 6673 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀)) |
18 | | f1of 6661 |
. . . . . . . . . . . . . 14
⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
20 | 19 | ffvelrnda 6904 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀)) |
21 | | fvco3 6810 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
22 | 13, 20, 21 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
23 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅) |
24 | 23 | difeq2d 4037 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅)) |
25 | | dif0 4287 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∖
∅) = (1...𝑀) |
26 | 24, 25 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
28 | 20, 27 | eleqtrrd 2841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) |
29 | | fco 6569 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
30 | 7, 12, 29 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
32 | | gsumval3.w |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
33 | 32 | eqimss2i 3960 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊 |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
35 | | ovexd 7248 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V) |
36 | 3 | fvexi 6731 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V) |
38 | 31, 34, 35, 37 | suppssr 7938 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
39 | 28, 38 | syldan 594 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
40 | | f1ocnvfv2 7088 |
. . . . . . . . . . . . 13
⊢ ((𝐻:(1...𝑀)–1-1-onto→ran
𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
41 | 16, 40 | sylan 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
42 | 41 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥)) |
43 | 22, 39, 42 | 3eqtr3rd 2786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 ) |
44 | | fvex 6730 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
45 | 44 | elsn 4556 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 ) |
46 | 43, 45 | sylibr 237 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
47 | 46 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
48 | | eldif 3876 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) |
49 | | gsumval3.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
50 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ V) |
51 | 7, 49, 2, 50 | suppssr 7938 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
52 | 51, 45 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
53 | 48, 52 | sylan2br 598 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
54 | 53 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
55 | 54 | anassrs 471 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
56 | 47, 55 | pm2.61dan 813 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 }) |
57 | 56, 45 | sylib 221 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 ) |
58 | 57 | mpteq2dva 5150 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 )) |
59 | 9, 58 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
60 | 59 | oveq2d 7229 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
61 | | gsumval3.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
62 | 61, 3 | mndidcl 18188 |
. . . . . 6
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
63 | | gsumval3.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
64 | 61, 63, 3 | mndlid 18193 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
65 | 1, 62, 64 | syl2anc2 588 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
66 | 65 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
67 | | gsumval3.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
68 | | nnuz 12477 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
69 | 67, 68 | eleqtrdi 2848 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
70 | 69 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈
(ℤ≥‘1)) |
71 | 26 | eleq2d 2823 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀))) |
72 | 71 | biimpar 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) |
73 | 31, 34, 35, 37 | suppssr 7938 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
74 | 72, 73 | syldan 594 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
75 | 66, 70, 74 | seqid3 13620 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 ) |
76 | 6, 60, 75 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
77 | | fzf 13099 |
. . . . 5
⊢
...:(ℤ × ℤ)⟶𝒫 ℤ |
78 | | ffn 6545 |
. . . . 5
⊢
(...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn
(ℤ × ℤ)) |
79 | | ovelrn 7384 |
. . . . 5
⊢ (... Fn
(ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))) |
80 | 77, 78, 79 | mp2b 10 |
. . . 4
⊢ (𝐴 ∈ ran ... ↔
∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
𝐴 = (𝑚...𝑛)) |
81 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd) |
82 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛)) |
83 | | frel 6550 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
84 | | reldm0 5797 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
85 | 7, 83, 84 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
86 | 7 | fdmd 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐴) |
87 | 86 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅)) |
88 | 85, 87 | bitrd 282 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅)) |
89 | | coeq1 5726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻)) |
90 | | co01 6125 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
∘ 𝐻) =
∅ |
91 | 89, 90 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅) |
92 | 91 | oveq1d 7228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0
)) |
93 | | supp0 7908 |
. . . . . . . . . . . . . . . . . 18
⊢ ( 0 ∈ V
→ (∅ supp 0 ) =
∅) |
94 | 36, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
supp 0 )
= ∅ |
95 | 92, 94 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅) |
96 | 32, 95 | syl5eq 2790 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = ∅ → 𝑊 = ∅) |
97 | 88, 96 | syl6bir 257 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅)) |
98 | 97 | necon3d 2961 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅)) |
99 | 98 | imp 410 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅) |
100 | 99 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅) |
101 | 82, 100 | eqnetrrd 3009 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅) |
102 | | fzn0 13126 |
. . . . . . . . . 10
⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚)) |
103 | 101, 102 | sylib 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚)) |
104 | 7 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵) |
105 | 82 | feq2d 6531 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵)) |
106 | 104, 105 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵) |
107 | 61, 63, 81, 103, 106 | gsumval2 18158 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛)) |
108 | | frn 6552 |
. . . . . . . . . . . . . . 15
⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴) |
109 | 10, 11, 108 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) |
110 | 109 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴) |
111 | 110, 82 | sseqtrd 3941 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛)) |
112 | | fzssuz 13153 |
. . . . . . . . . . . . 13
⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚) |
113 | | uzssz 12459 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑚) ⊆ ℤ |
114 | | zssre 12183 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
115 | 113, 114 | sstri 3910 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑚) ⊆ ℝ |
116 | 112, 115 | sstri 3910 |
. . . . . . . . . . . 12
⊢ (𝑚...𝑛) ⊆ ℝ |
117 | 111, 116 | sstrdi 3913 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ) |
118 | | ltso 10913 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
119 | | soss 5488 |
. . . . . . . . . . 11
⊢ (ran
𝐻 ⊆ ℝ → (
< Or ℝ → < Or ran 𝐻)) |
120 | 117, 118,
119 | mpisyl 21 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻) |
121 | | fzfi 13545 |
. . . . . . . . . . . 12
⊢
(1...𝑀) ∈
Fin |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
123 | 12, 122 | fexd 7043 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ V) |
124 | | f1oen3g 8644 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) |
125 | 123, 15, 124 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) |
126 | | enfi 8865 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
128 | 121, 127 | mpbii 236 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
129 | 128 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin) |
130 | | fz1iso 14028 |
. . . . . . . . . 10
⊢ (( <
Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
131 | 120, 129,
130 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
132 | 67 | nnnn0d 12150 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
133 | | hashfz1 13912 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
135 | 122, 15 | hasheqf1od 13920 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻)) |
136 | 134, 135 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻)) |
137 | 136 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻)) |
138 | 137 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻))) |
139 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd) |
140 | 61, 63 | mndcl 18181 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
141 | 140 | 3expb 1122 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
142 | 139, 141 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
143 | | gsumval3.c |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
144 | 143 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
145 | 144 | sselda 3901 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹)) |
146 | | gsumval3.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 = (Cntz‘𝐺) |
147 | 63, 146 | cntzi 18723 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
148 | 145, 147 | sylan 583 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
149 | 148 | anasss 470 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
150 | 61, 63 | mndass 18182 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
151 | 139, 150 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
152 | 69 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑀 ∈
(ℤ≥‘1)) |
153 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵) |
154 | 153 | frnd 6553 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵) |
155 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
156 | | isof1o 7132 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Isom < , <
((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻) |
157 | 155, 156 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻) |
158 | 137 | oveq2d 7229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻))) |
159 | 158 | f1oeq2d 6657 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻)) |
160 | 157, 159 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran
𝐻) |
161 | | f1ocnv 6673 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
163 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
164 | | f1oco 6683 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
165 | 162, 163,
164 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
166 | | ffn 6545 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
167 | | dffn4 6639 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
168 | 166, 167 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
169 | | fof 6633 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹) |
170 | 153, 168,
169 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹) |
171 | | f1of 6661 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻) |
172 | 160, 171 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻) |
173 | 109 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴) |
174 | 172, 173 | fssd 6563 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴) |
175 | | fco 6569 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
176 | 170, 174,
175 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
177 | 176 | ffvelrnda 6904 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹) |
178 | | f1ococnv2 6687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
179 | 160, 178 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
180 | 179 | coeq1d 5730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻)) |
181 | | f1of 6661 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻) |
182 | | fcoi2 6594 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
183 | 163, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
184 | 180, 183 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻)) |
185 | | coass 6129 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻)) |
186 | 184, 185 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
187 | 186 | coeq2d 5731 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))) |
188 | | coass 6129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
189 | 187, 188 | eqtr4di 2796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))) |
190 | 189 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
191 | 190 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
192 | | f1of 6661 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
193 | 160, 161,
192 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
194 | 163, 181 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻) |
195 | | fco 6569 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
196 | 193, 194,
195 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
197 | | fvco3 6810 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
198 | 196, 197 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
199 | 191, 198 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
200 | 142, 149,
151, 152, 154, 165, 177, 199 | seqf1o 13617 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀)) |
201 | 61, 63, 3 | mndlid 18193 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
202 | 139, 201 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
203 | 61, 63, 3 | mndrid 18194 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
204 | 139, 203 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
205 | 139, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 0 ∈ 𝐵) |
206 | | fdm 6554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀)) |
207 | 10, 11, 206 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = (1...𝑀)) |
208 | | eluzfz1 13119 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
209 | | ne0i 4249 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
(1...𝑀) → (1...𝑀) ≠ ∅) |
210 | 69, 208, 209 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ≠ ∅) |
211 | 207, 210 | eqnetrd 3008 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐻 ≠ ∅) |
212 | | dm0rn0 5794 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐻 = ∅ ↔ ran
𝐻 =
∅) |
213 | 212 | necon3bii 2993 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐻 ≠ ∅ ↔ ran
𝐻 ≠
∅) |
214 | 211, 213 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ≠ ∅) |
215 | 214 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅) |
216 | 111 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛)) |
217 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛)) |
218 | 217 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛))) |
219 | 218 | biimpar 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴) |
220 | 153 | ffvelrnda 6904 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
221 | 219, 220 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵) |
222 | 217 | difeq1d 4036 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻)) |
223 | 222 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻))) |
224 | 223 | biimpar 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻)) |
225 | 51 | ad4ant14 752 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
226 | 224, 225 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
227 | | f1of 6661 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻 → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻) |
228 | 155, 156,
227 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻) |
229 | | fvco3 6810 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
230 | 228, 229 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
231 | 202, 204,
142, 205, 155, 215, 216, 221, 226, 230 | seqcoll2 14031 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻))) |
232 | 138, 200,
231 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
233 | 232 | expr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
234 | 233 | exlimdv 1941 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
235 | 131, 234 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
236 | 107, 235 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
237 | 236 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
238 | 237 | rexlimdvw 3209 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
239 | 238 | rexlimdvw 3209 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
240 | 80, 239 | syl5bi 245 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
241 | | suppssdm 7919 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
242 | 32, 241 | eqsstri 3935 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
243 | 242, 30 | fssdm 6565 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
244 | | fz1ssnn 13143 |
. . . . . . . . . 10
⊢
(1...𝑀) ⊆
ℕ |
245 | | nnssre 11834 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ |
246 | 244, 245 | sstri 3910 |
. . . . . . . . 9
⊢
(1...𝑀) ⊆
ℝ |
247 | 243, 246 | sstrdi 3913 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ ℝ) |
248 | | soss 5488 |
. . . . . . . 8
⊢ (𝑊 ⊆ ℝ → ( <
Or ℝ → < Or 𝑊)) |
249 | 247, 118,
248 | mpisyl 21 |
. . . . . . 7
⊢ (𝜑 → < Or 𝑊) |
250 | | ssfi 8851 |
. . . . . . . 8
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
251 | 121, 243,
250 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) |
252 | | fz1iso 14028 |
. . . . . . 7
⊢ (( <
Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
253 | 249, 251,
252 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
254 | 253 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
255 | 61, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32 | gsumval3lem2 19291 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |
256 | 1 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐺 ∈ Mnd) |
257 | 256, 201 | sylan 583 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
258 | 256, 203 | sylan 583 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
259 | 256, 141 | sylan 583 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
260 | 256, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 0 ∈ 𝐵) |
261 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊)) |
262 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ≠ ∅) |
263 | 243 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) |
264 | 30 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
265 | 264 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵) |
266 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
267 | | ovexd 7248 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (1...𝑀) ∈ V) |
268 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 0 ∈
V) |
269 | 264, 266,
267, 268 | suppssr 7938 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
270 | | coass 6129 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓)) |
271 | 270 | fveq1i 6718 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) |
272 | | isof1o 7132 |
. . . . . . . . . . . 12
⊢ (𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
273 | | f1of 6661 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
274 | 261, 272,
273 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
275 | | fvco3 6810 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
276 | 274, 275 | sylan 583 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑦 ∈
(1...(♯‘𝑊)))
→ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
277 | 271, 276 | eqtr3id 2792 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑦 ∈
(1...(♯‘𝑊)))
→ ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
278 | 257, 258,
259, 260, 261, 262, 263, 265, 269, 277 | seqcoll2 14031 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |
279 | 255, 278 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
280 | 279 | expr 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
281 | 280 | exlimdv 1941 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
282 | 254, 281 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
283 | 282 | ex 416 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
284 | 240, 283 | pm2.61d 182 |
. 2
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
285 | 76, 284 | pm2.61dane 3029 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |