Step | Hyp | Ref
| Expression |
1 | | gsumval3.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumval3.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | gsumval3.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
4 | 3 | gsumz 17575 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 573 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
6 | 5 | adantr 466 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
7 | | gsumval3.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
8 | 7 | feqmptd 6389 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
9 | 8 | adantr 466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
10 | | gsumval3.h |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
11 | | f1f 6239 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
13 | 12 | ad2antrr 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴) |
14 | | f1f1orn 6287 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
16 | 15 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
17 | | f1ocnv 6288 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀)) |
18 | | f1of 6276 |
. . . . . . . . . . . . . 14
⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
20 | 19 | ffvelrnda 6500 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀)) |
21 | | fvco3 6415 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
22 | 13, 20, 21 | syl2anc 573 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
23 | | simpr 471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅) |
24 | 23 | difeq2d 3879 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅)) |
25 | | dif0 4097 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∖
∅) = (1...𝑀) |
26 | 24, 25 | syl6eq 2821 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
27 | 26 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
28 | 20, 27 | eleqtrrd 2853 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) |
29 | | fco 6196 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
30 | 7, 12, 29 | syl2anc 573 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
31 | 30 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
32 | | gsumval3.w |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
33 | 32 | eqimss2i 3809 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊 |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
35 | | ovexd 6823 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V) |
36 | 3 | fvexi 6341 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V) |
38 | 31, 34, 35, 37 | suppssr 7476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
39 | 28, 38 | syldan 579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
40 | | f1ocnvfv2 6674 |
. . . . . . . . . . . . 13
⊢ ((𝐻:(1...𝑀)–1-1-onto→ran
𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
41 | 16, 40 | sylan 569 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
42 | 41 | fveq2d 6334 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥)) |
43 | 22, 39, 42 | 3eqtr3rd 2814 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 ) |
44 | | fvex 6340 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
45 | 44 | elsn 4331 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 ) |
46 | 43, 45 | sylibr 224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
47 | 46 | adantlr 694 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
48 | | eldif 3733 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) |
49 | | gsumval3.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
50 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ V) |
51 | 7, 49, 2, 50 | suppssr 7476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
52 | 51, 45 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
53 | 48, 52 | sylan2br 582 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
54 | 53 | adantlr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
55 | 54 | anassrs 453 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
56 | 47, 55 | pm2.61dan 814 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 }) |
57 | 56, 45 | sylib 208 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 ) |
58 | 57 | mpteq2dva 4878 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 )) |
59 | 9, 58 | eqtrd 2805 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
60 | 59 | oveq2d 6807 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
61 | | gsumval3.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
62 | 61, 3 | mndidcl 17509 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
63 | 1, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
64 | | gsumval3.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
65 | 61, 64, 3 | mndlid 17512 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
66 | 1, 63, 65 | syl2anc 573 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
67 | 66 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
68 | | gsumval3.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
69 | | nnuz 11923 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
70 | 68, 69 | syl6eleq 2860 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
71 | 70 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈
(ℤ≥‘1)) |
72 | 26 | eleq2d 2836 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀))) |
73 | 72 | biimpar 463 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) |
74 | 31, 34, 35, 37 | suppssr 7476 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
75 | 73, 74 | syldan 579 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
76 | 67, 71, 75 | seqid3 13045 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 ) |
77 | 6, 60, 76 | 3eqtr4d 2815 |
. 2
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
78 | | fzf 12530 |
. . . . 5
⊢
...:(ℤ × ℤ)⟶𝒫 ℤ |
79 | | ffn 6183 |
. . . . 5
⊢
(...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn
(ℤ × ℤ)) |
80 | | ovelrn 6955 |
. . . . 5
⊢ (... Fn
(ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))) |
81 | 78, 79, 80 | mp2b 10 |
. . . 4
⊢ (𝐴 ∈ ran ... ↔
∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
𝐴 = (𝑚...𝑛)) |
82 | 1 | ad2antrr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd) |
83 | | simpr 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛)) |
84 | | frel 6188 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
85 | | reldm0 5479 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
86 | 7, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
87 | | fdm 6189 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
88 | 7, 87 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐴) |
89 | 88 | eqeq1d 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅)) |
90 | 86, 89 | bitrd 268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅)) |
91 | | coeq1 5416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻)) |
92 | | co01 5792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
∘ 𝐻) =
∅ |
93 | 91, 92 | syl6eq 2821 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅) |
94 | 93 | oveq1d 6806 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0
)) |
95 | | supp0 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ ( 0 ∈ V
→ (∅ supp 0 ) =
∅) |
96 | 36, 95 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
supp 0 )
= ∅ |
97 | 94, 96 | syl6eq 2821 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅) |
98 | 32, 97 | syl5eq 2817 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = ∅ → 𝑊 = ∅) |
99 | 90, 98 | syl6bir 244 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅)) |
100 | 99 | necon3d 2964 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅)) |
101 | 100 | imp 393 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅) |
102 | 101 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅) |
103 | 83, 102 | eqnetrrd 3011 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅) |
104 | | fzn0 12555 |
. . . . . . . . . 10
⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚)) |
105 | 103, 104 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚)) |
106 | 7 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵) |
107 | 83 | feq2d 6169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵)) |
108 | 106, 107 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵) |
109 | 61, 64, 82, 105, 108 | gsumval2 17481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛)) |
110 | | frn 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴) |
111 | 10, 11, 110 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) |
112 | 111 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴) |
113 | 112, 83 | sseqtrd 3790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛)) |
114 | | fzssuz 12582 |
. . . . . . . . . . . . 13
⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚) |
115 | | uzssz 11906 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑚) ⊆ ℤ |
116 | | zssre 11584 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
117 | 115, 116 | sstri 3761 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑚) ⊆ ℝ |
118 | 114, 117 | sstri 3761 |
. . . . . . . . . . . 12
⊢ (𝑚...𝑛) ⊆ ℝ |
119 | 113, 118 | syl6ss 3764 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ) |
120 | | ltso 10318 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
121 | | soss 5188 |
. . . . . . . . . . 11
⊢ (ran
𝐻 ⊆ ℝ → (
< Or ℝ → < Or ran 𝐻)) |
122 | 119, 120,
121 | mpisyl 21 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻) |
123 | | fzfi 12972 |
. . . . . . . . . . . 12
⊢
(1...𝑀) ∈
Fin |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
125 | | fex2 7266 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
126 | 12, 124, 2, 125 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ V) |
127 | | f1oen3g 8123 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) |
128 | 126, 15, 127 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) |
129 | | enfi 8330 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
131 | 123, 130 | mpbii 223 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
132 | 131 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin) |
133 | | fz1iso 13441 |
. . . . . . . . . 10
⊢ (( <
Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
134 | 122, 132,
133 | syl2anc 573 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
135 | 68 | nnnn0d 11551 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
136 | | hashfz1 13331 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
138 | | hashen 13332 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...𝑀) ∈ Fin
∧ ran 𝐻 ∈ Fin)
→ ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻)) |
139 | 123, 131,
138 | sylancr 575 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((♯‘(1...𝑀)) = (♯‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻)) |
140 | 128, 139 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘ran 𝐻)) |
141 | 137, 140 | eqtr3d 2807 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 = (♯‘ran 𝐻)) |
142 | 141 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑀 = (♯‘ran 𝐻)) |
143 | 142 | fveq2d 6334 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻))) |
144 | 1 | ad2antrr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd) |
145 | 61, 64 | mndcl 17502 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
146 | 145 | 3expb 1113 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
147 | 144, 146 | sylan 569 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
148 | | gsumval3.c |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
149 | 148 | ad2antrr 705 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
150 | 149 | sselda 3752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹)) |
151 | | gsumval3.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 = (Cntz‘𝐺) |
152 | 64, 151 | cntzi 17962 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
153 | 150, 152 | sylan 569 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
154 | 153 | anasss 452 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
155 | 61, 64 | mndass 17503 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
156 | 144, 155 | sylan 569 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
157 | 70 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑀 ∈
(ℤ≥‘1)) |
158 | 7 | ad2antrr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵) |
159 | | frn 6191 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵) |
161 | | simprr 756 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻)) |
162 | | isof1o 6714 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Isom < , <
((1...(♯‘ran 𝐻)), ran 𝐻) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻) |
164 | 142 | oveq2d 6807 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (1...𝑀) = (1...(♯‘ran 𝐻))) |
165 | | f1oeq2 6267 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑀) =
(1...(♯‘ran 𝐻))
→ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻)) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 ↔ 𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻)) |
167 | 163, 166 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran
𝐻) |
168 | | f1ocnv 6288 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
170 | 15 | ad2antrr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
171 | | f1oco 6298 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
172 | 169, 170,
171 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
173 | | ffn 6183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
174 | | dffn4 6260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
175 | 173, 174 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
176 | | fof 6254 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹) |
177 | 158, 175,
176 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹) |
178 | | f1of 6276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻) |
179 | 167, 178 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻) |
180 | 111 | ad2antrr 705 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴) |
181 | 179, 180 | fssd 6195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴) |
182 | | fco 6196 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
183 | 177, 181,
182 | syl2anc 573 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
184 | 183 | ffvelrnda 6500 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹) |
185 | | f1ococnv2 6302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
186 | 167, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
187 | 186 | coeq1d 5420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻)) |
188 | | f1of 6276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻) |
189 | | fcoi2 6217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
190 | 170, 188,
189 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
191 | 187, 190 | eqtr2d 2806 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻)) |
192 | | coass 5796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻)) |
193 | 191, 192 | syl6eq 2821 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
194 | 193 | coeq2d 5421 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))) |
195 | | coass 5796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
196 | 194, 195 | syl6eqr 2823 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))) |
197 | 196 | fveq1d 6332 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
198 | 197 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
199 | | f1of 6276 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
200 | 167, 168,
199 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
201 | 170, 188 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻) |
202 | | fco 6196 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
203 | 200, 201,
202 | syl2anc 573 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
204 | | fvco3 6415 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
205 | 203, 204 | sylan 569 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
206 | 198, 205 | eqtrd 2805 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
207 | 147, 154,
156, 157, 160, 172, 184, 206 | seqf1o 13042 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀)) |
208 | 61, 64, 3 | mndlid 17512 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
209 | 144, 208 | sylan 569 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
210 | 61, 64, 3 | mndrid 17513 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
211 | 144, 210 | sylan 569 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
212 | 144, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 0 ∈ 𝐵) |
213 | | fdm 6189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀)) |
214 | 10, 11, 213 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = (1...𝑀)) |
215 | | eluzfz1 12548 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
216 | | ne0i 4069 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
(1...𝑀) → (1...𝑀) ≠ ∅) |
217 | 70, 215, 216 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ≠ ∅) |
218 | 214, 217 | eqnetrd 3010 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐻 ≠ ∅) |
219 | | dm0rn0 5478 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐻 = ∅ ↔ ran
𝐻 =
∅) |
220 | 219 | necon3bii 2995 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐻 ≠ ∅ ↔ ran
𝐻 ≠
∅) |
221 | 218, 220 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ≠ ∅) |
222 | 221 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅) |
223 | 113 | adantrr 696 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛)) |
224 | | simprl 754 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛)) |
225 | 224 | eleq2d 2836 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛))) |
226 | 225 | biimpar 463 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴) |
227 | 158 | ffvelrnda 6500 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
228 | 226, 227 | syldan 579 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵) |
229 | 224 | difeq1d 3878 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻)) |
230 | 229 | eleq2d 2836 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻))) |
231 | 230 | biimpar 463 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻)) |
232 | | simpll 750 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝜑) |
233 | 232, 51 | sylan 569 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
234 | 231, 233 | syldan 579 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
235 | | f1of 6276 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘ran 𝐻))–1-1-onto→ran
𝐻 → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻) |
236 | 161, 162,
235 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → 𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻) |
237 | | fvco3 6415 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
238 | 236, 237 | sylan 569 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(♯‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
239 | 209, 211,
147, 212, 161, 222, 223, 228, 234, 238 | seqcoll2 13444 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘ran 𝐻))) |
240 | 143, 207,
239 | 3eqtr4d 2815 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
241 | 240 | expr 444 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
242 | 241 | exlimdv 2013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘ran
𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
243 | 134, 242 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
244 | 109, 243 | eqtr4d 2808 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
245 | 244 | ex 397 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
246 | 245 | rexlimdvw 3182 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
247 | 246 | rexlimdvw 3182 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
248 | 81, 247 | syl5bi 232 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
249 | | suppssdm 7457 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
250 | 32, 249 | eqsstri 3784 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
251 | | fdm 6189 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵 → dom (𝐹 ∘ 𝐻) = (1...𝑀)) |
252 | 30, 251 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝐹 ∘ 𝐻) = (1...𝑀)) |
253 | 250, 252 | syl5sseq 3802 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
254 | | fzssuz 12582 |
. . . . . . . . . . 11
⊢
(1...𝑀) ⊆
(ℤ≥‘1) |
255 | 254, 69 | sseqtr4i 3787 |
. . . . . . . . . 10
⊢
(1...𝑀) ⊆
ℕ |
256 | | nnssre 11224 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ |
257 | 255, 256 | sstri 3761 |
. . . . . . . . 9
⊢
(1...𝑀) ⊆
ℝ |
258 | 253, 257 | syl6ss 3764 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ ℝ) |
259 | | soss 5188 |
. . . . . . . 8
⊢ (𝑊 ⊆ ℝ → ( <
Or ℝ → < Or 𝑊)) |
260 | 258, 120,
259 | mpisyl 21 |
. . . . . . 7
⊢ (𝜑 → < Or 𝑊) |
261 | | ssfi 8334 |
. . . . . . . 8
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
262 | 123, 253,
261 | sylancr 575 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) |
263 | | fz1iso 13441 |
. . . . . . 7
⊢ (( <
Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
264 | 260, 262,
263 | syl2anc 573 |
. . . . . 6
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
265 | 264 | ad2antrr 705 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊)) |
266 | 61, 3, 64, 151, 1, 2, 7, 148, 68, 10, 49, 32 | gsumval3lem2 18507 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |
267 | 1 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐺 ∈ Mnd) |
268 | 267, 208 | sylan 569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
269 | 267, 210 | sylan 569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
270 | 267, 146 | sylan 569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
271 | 267, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 0 ∈ 𝐵) |
272 | | simprr 756 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊)) |
273 | | simplr 752 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ≠ ∅) |
274 | 253 | ad2antrr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) |
275 | 30 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
276 | 275 | ffvelrnda 6500 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵) |
277 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
278 | | ovexd 6823 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (1...𝑀) ∈ V) |
279 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 0 ∈
V) |
280 | 275, 277,
278, 279 | suppssr 7476 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
281 | | coass 5796 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓)) |
282 | 281 | fveq1i 6331 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) |
283 | | isof1o 6714 |
. . . . . . . . . . . 12
⊢ (𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
284 | | f1of 6276 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
285 | 272, 283,
284 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
286 | | fvco3 6415 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
287 | 285, 286 | sylan 569 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑦 ∈
(1...(♯‘𝑊)))
→ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
288 | 282, 287 | syl5eqr 2819 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) ∧ 𝑦 ∈
(1...(♯‘𝑊)))
→ ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
289 | 268, 269,
270, 271, 272, 273, 274, 276, 280, 288 | seqcoll2 13444 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |
290 | 266, 289 | eqtr4d 2808 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
291 | 290 | expr 444 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
292 | 291 | exlimdv 2013 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
293 | 265, 292 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
294 | 293 | ex 397 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
295 | 248, 294 | pm2.61d 171 |
. 2
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
296 | 77, 295 | pm2.61dane 3030 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |