Step | Hyp | Ref
| Expression |
1 | | gsumval3.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumval3.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | gsumval3.0 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
4 | 3 | gsumz 17374 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
7 | | gsumval3.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
8 | 7 | feqmptd 6249 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
10 | | gsumval3.h |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
11 | | f1f 6101 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
13 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → 𝐻:(1...𝑀)⟶𝐴) |
14 | | f1f1orn 6148 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
17 | | f1ocnv 6149 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝐻:ran 𝐻–1-1-onto→(1...𝑀)) |
18 | | f1of 6137 |
. . . . . . . . . . . . . 14
⊢ (◡𝐻:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ◡𝐻:ran 𝐻⟶(1...𝑀)) |
20 | 19 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ (1...𝑀)) |
21 | | fvco3 6275 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (◡𝐻‘𝑥) ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
22 | 13, 20, 21 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = (𝐹‘(𝐻‘(◡𝐻‘𝑥)))) |
23 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑊 = ∅) |
24 | 23 | difeq2d 3728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = ((1...𝑀) ∖ ∅)) |
25 | | dif0 3950 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∖
∅) = (1...𝑀) |
26 | 24, 25 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((1...𝑀) ∖ 𝑊) = (1...𝑀)) |
28 | 20, 27 | eleqtrrd 2704 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) |
29 | | fco 6058 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
30 | 7, 12, 29 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
32 | | gsumval3.w |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
33 | 32 | eqimss2i 3660 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊 |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
35 | | ovexd 6680 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → (1...𝑀) ∈ V) |
36 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) ∈ V |
37 | 3, 36 | eqeltri 2697 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
38 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 = ∅) → 0 ∈ V) |
39 | 31, 34, 35, 38 | suppssr 7326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (◡𝐻‘𝑥) ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
40 | 28, 39 | syldan 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑥)) = 0 ) |
41 | | f1ocnvfv2 6533 |
. . . . . . . . . . . . 13
⊢ ((𝐻:(1...𝑀)–1-1-onto→ran
𝐻 ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
42 | 16, 41 | sylan 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐻‘(◡𝐻‘𝑥)) = 𝑥) |
43 | 42 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘(𝐻‘(◡𝐻‘𝑥))) = (𝐹‘𝑥)) |
44 | 22, 40, 43 | 3eqtr3rd 2665 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) = 0 ) |
45 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
46 | 45 | elsn 4192 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ { 0 } ↔ (𝐹‘𝑥) = 0 ) |
47 | 44, 46 | sylibr 224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
48 | 47 | adantlr 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
49 | | eldif 3584 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) |
50 | | gsumval3.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
51 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ V) |
52 | 7, 50, 2, 51 | suppssr 7326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
53 | 52, 46 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
54 | 49, 53 | sylan2br 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
55 | 54 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐻)) → (𝐹‘𝑥) ∈ { 0 }) |
56 | 55 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ ran 𝐻) → (𝐹‘𝑥) ∈ { 0 }) |
57 | 48, 56 | pm2.61dan 832 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ { 0 }) |
58 | 57, 46 | sylib 208 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 0 ) |
59 | 58 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ 0 )) |
60 | 9, 59 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
61 | 60 | oveq2d 6666 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
62 | | gsumval3.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
63 | 62, 3 | mndidcl 17308 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
64 | 1, 63 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
65 | | gsumval3.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
66 | 62, 65, 3 | mndlid 17311 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
67 | 1, 64, 66 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
68 | 67 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
69 | | gsumval3.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
70 | | nnuz 11723 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
71 | 69, 70 | syl6eleq 2711 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
72 | 71 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑀 ∈
(ℤ≥‘1)) |
73 | 26 | eleq2d 2687 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ ((1...𝑀) ∖ 𝑊) ↔ 𝑥 ∈ (1...𝑀))) |
74 | 73 | biimpar 502 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) |
75 | 31, 34, 35, 38 | suppssr 7326 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
76 | 74, 75 | syldan 487 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
77 | 68, 72, 76 | seqid3 12845 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = 0 ) |
78 | 6, 61, 77 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
79 | | fzf 12330 |
. . . . 5
⊢
...:(ℤ × ℤ)⟶𝒫 ℤ |
80 | | ffn 6045 |
. . . . 5
⊢
(...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn
(ℤ × ℤ)) |
81 | | ovelrn 6810 |
. . . . 5
⊢ (... Fn
(ℤ × ℤ) → (𝐴 ∈ ran ... ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛))) |
82 | 79, 80, 81 | mp2b 10 |
. . . 4
⊢ (𝐴 ∈ ran ... ↔
∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
𝐴 = (𝑚...𝑛)) |
83 | 1 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐺 ∈ Mnd) |
84 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 = (𝑚...𝑛)) |
85 | | frel 6050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
86 | | reldm0 5343 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
87 | 7, 85, 86 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
88 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
89 | 7, 88 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐴) |
90 | 89 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (dom 𝐹 = ∅ ↔ 𝐴 = ∅)) |
91 | 87, 90 | bitrd 268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 = ∅ ↔ 𝐴 = ∅)) |
92 | | coeq1 5279 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = (∅ ∘ 𝐻)) |
93 | | co01 5650 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
∘ 𝐻) =
∅ |
94 | 92, 93 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 = ∅ → (𝐹 ∘ 𝐻) = ∅) |
95 | 94 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) = (∅ supp 0
)) |
96 | | supp0 7300 |
. . . . . . . . . . . . . . . . . 18
⊢ ( 0 ∈ V
→ (∅ supp 0 ) =
∅) |
97 | 37, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
supp 0 )
= ∅ |
98 | 95, 97 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅) |
99 | 32, 98 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = ∅ → 𝑊 = ∅) |
100 | 91, 99 | syl6bir 244 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 = ∅ → 𝑊 = ∅)) |
101 | 100 | necon3d 2815 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ≠ ∅ → 𝐴 ≠ ∅)) |
102 | 101 | imp 445 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → 𝐴 ≠ ∅) |
103 | 102 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐴 ≠ ∅) |
104 | 84, 103 | eqnetrrd 2862 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑚...𝑛) ≠ ∅) |
105 | | fzn0 12355 |
. . . . . . . . . 10
⊢ ((𝑚...𝑛) ≠ ∅ ↔ 𝑛 ∈ (ℤ≥‘𝑚)) |
106 | 104, 105 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝑛 ∈ (ℤ≥‘𝑚)) |
107 | 7 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:𝐴⟶𝐵) |
108 | 84 | feq2d 6031 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:(𝑚...𝑛)⟶𝐵)) |
109 | 107, 108 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → 𝐹:(𝑚...𝑛)⟶𝐵) |
110 | 62, 65, 83, 106, 109 | gsumval2 17280 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq𝑚( + , 𝐹)‘𝑛)) |
111 | | frn 6053 |
. . . . . . . . . . . . . . 15
⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴) |
112 | 10, 11, 111 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) |
113 | 112 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ 𝐴) |
114 | 113, 84 | sseqtrd 3641 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ (𝑚...𝑛)) |
115 | | fzssuz 12382 |
. . . . . . . . . . . . 13
⊢ (𝑚...𝑛) ⊆ (ℤ≥‘𝑚) |
116 | | uzssz 11707 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑚) ⊆ ℤ |
117 | | zssre 11384 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
118 | 116, 117 | sstri 3612 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑚) ⊆ ℝ |
119 | 115, 118 | sstri 3612 |
. . . . . . . . . . . 12
⊢ (𝑚...𝑛) ⊆ ℝ |
120 | 114, 119 | syl6ss 3615 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ⊆ ℝ) |
121 | | ltso 10118 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
122 | | soss 5053 |
. . . . . . . . . . 11
⊢ (ran
𝐻 ⊆ ℝ → (
< Or ℝ → < Or ran 𝐻)) |
123 | 120, 121,
122 | mpisyl 21 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → < Or ran 𝐻) |
124 | | fzfi 12771 |
. . . . . . . . . . . 12
⊢
(1...𝑀) ∈
Fin |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
126 | | fex2 7121 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
127 | 12, 125, 2, 126 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ V) |
128 | | f1oen3g 7971 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) |
129 | 127, 15, 128 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) |
130 | | enfi 8176 |
. . . . . . . . . . . . 13
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
132 | 124, 131 | mpbii 223 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
133 | 132 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ran 𝐻 ∈ Fin) |
134 | | fz1iso 13246 |
. . . . . . . . . 10
⊢ (( <
Or ran 𝐻 ∧ ran 𝐻 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻)) |
135 | 123, 133,
134 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → ∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻)) |
136 | 69 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
137 | | hashfz1 13134 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘(1...𝑀)) = 𝑀) |
139 | | hashen 13135 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...𝑀) ∈ Fin
∧ ran 𝐻 ∈ Fin)
→ ((#‘(1...𝑀)) =
(#‘ran 𝐻) ↔
(1...𝑀) ≈ ran 𝐻)) |
140 | 124, 132,
139 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((#‘(1...𝑀)) = (#‘ran 𝐻) ↔ (1...𝑀) ≈ ran 𝐻)) |
141 | 129, 140 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘(1...𝑀)) = (#‘ran 𝐻)) |
142 | 138, 141 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 = (#‘ran 𝐻)) |
143 | 142 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 = (#‘ran 𝐻)) |
144 | 143 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘ran 𝐻))) |
145 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐺 ∈ Mnd) |
146 | 62, 65 | mndcl 17301 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
147 | 146 | 3expb 1266 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
148 | 145, 147 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
149 | | gsumval3.c |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
150 | 149 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
151 | 150 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) → 𝑥 ∈ (𝑍‘ran 𝐹)) |
152 | | gsumval3.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 = (Cntz‘𝐺) |
153 | 65, 152 | cntzi 17762 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑍‘ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
154 | 151, 153 | sylan 488 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ran 𝐹) ∧ 𝑦 ∈ ran 𝐹) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
155 | 154 | anasss 679 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
156 | 62, 65 | mndass 17302 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
157 | 145, 156 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
158 | 71 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑀 ∈
(ℤ≥‘1)) |
159 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶𝐵) |
160 | | frn 6053 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐹 ⊆ 𝐵) |
162 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻)) |
163 | | isof1o 6573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Isom < , <
((1...(#‘ran 𝐻)), ran
𝐻) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran
𝐻) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran
𝐻) |
165 | 143 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (1...𝑀) = (1...(#‘ran 𝐻))) |
166 | | f1oeq2 6128 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑀) =
(1...(#‘ran 𝐻))
→ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 ↔ 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran
𝐻)) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 ↔ 𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran
𝐻)) |
168 | 164, 167 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)–1-1-onto→ran
𝐻) |
169 | | f1ocnv 6149 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻–1-1-onto→(1...𝑀)) |
171 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
172 | | f1oco 6159 |
. . . . . . . . . . . . . 14
⊢ ((◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
173 | 170, 171,
172 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)–1-1-onto→(1...𝑀)) |
174 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
175 | | dffn4 6121 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
176 | 174, 175 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→ran 𝐹) |
177 | | fof 6115 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴–onto→ran 𝐹 → 𝐹:𝐴⟶ran 𝐹) |
178 | 159, 176,
177 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐹:𝐴⟶ran 𝐹) |
179 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → 𝑓:(1...𝑀)⟶ran 𝐻) |
180 | 168, 179 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶ran 𝐻) |
181 | 112 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ 𝐴) |
182 | 180, 181 | fssd 6057 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...𝑀)⟶𝐴) |
183 | | fco 6058 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝑓:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
184 | 178, 182,
183 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝑓):(1...𝑀)⟶ran 𝐹) |
185 | 184 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝑓)‘𝑥) ∈ ran 𝐹) |
186 | | f1ococnv2 6163 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:(1...𝑀)–1-1-onto→ran
𝐻 → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
187 | 168, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑓 ∘ ◡𝑓) = ( I ↾ ran 𝐻)) |
188 | 187 | coeq1d 5283 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (( I ↾ ran 𝐻) ∘ 𝐻)) |
189 | | f1of 6137 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)–1-1-onto→ran
𝐻 → 𝐻:(1...𝑀)⟶ran 𝐻) |
190 | | fcoi2 6079 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻:(1...𝑀)⟶ran 𝐻 → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
191 | 171, 189,
190 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (( I ↾ ran 𝐻) ∘ 𝐻) = 𝐻) |
192 | 188, 191 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = ((𝑓 ∘ ◡𝑓) ∘ 𝐻)) |
193 | | coass 5654 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∘ ◡𝑓) ∘ 𝐻) = (𝑓 ∘ (◡𝑓 ∘ 𝐻)) |
194 | 192, 193 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻 = (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
195 | 194 | coeq2d 5284 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻)))) |
196 | | coass 5654 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻)) = (𝐹 ∘ (𝑓 ∘ (◡𝑓 ∘ 𝐻))) |
197 | 195, 196 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐹 ∘ 𝐻) = ((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))) |
198 | 197 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
199 | 198 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘)) |
200 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑓:ran 𝐻–1-1-onto→(1...𝑀) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
201 | 168, 169,
200 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ◡𝑓:ran 𝐻⟶(1...𝑀)) |
202 | 171, 189 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐻:(1...𝑀)⟶ran 𝐻) |
203 | | fco 6058 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑓:ran 𝐻⟶(1...𝑀) ∧ 𝐻:(1...𝑀)⟶ran 𝐻) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
204 | 201, 202,
203 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀)) |
205 | | fvco3 6275 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓 ∘ 𝐻):(1...𝑀)⟶(1...𝑀) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
206 | 204, 205 | sylan 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → (((𝐹 ∘ 𝑓) ∘ (◡𝑓 ∘ 𝐻))‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
207 | 199, 206 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑘) = ((𝐹 ∘ 𝑓)‘((◡𝑓 ∘ 𝐻)‘𝑘))) |
208 | 148, 155,
157, 158, 161, 173, 185, 207 | seqf1o 12842 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ 𝑓))‘𝑀)) |
209 | 62, 65, 3 | mndlid 17311 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
210 | 145, 209 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
211 | 62, 65, 3 | mndrid 17312 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
212 | 145, 211 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
213 | 145, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 0 ∈ 𝐵) |
214 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻:(1...𝑀)⟶𝐴 → dom 𝐻 = (1...𝑀)) |
215 | 10, 11, 214 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = (1...𝑀)) |
216 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
217 | | ne0i 3921 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
(1...𝑀) → (1...𝑀) ≠ ∅) |
218 | 71, 216, 217 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ≠ ∅) |
219 | 215, 218 | eqnetrd 2861 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐻 ≠ ∅) |
220 | | dm0rn0 5342 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐻 = ∅ ↔ ran
𝐻 =
∅) |
221 | 220 | necon3bii 2846 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐻 ≠ ∅ ↔ ran
𝐻 ≠
∅) |
222 | 219, 221 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐻 ≠ ∅) |
223 | 222 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ≠ ∅) |
224 | 114 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → ran 𝐻 ⊆ (𝑚...𝑛)) |
225 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝐴 = (𝑚...𝑛)) |
226 | 225 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑚...𝑛))) |
227 | 226 | biimpar 502 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → 𝑥 ∈ 𝐴) |
228 | 159 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
229 | 227, 228 | syldan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝑚...𝑛)) → (𝐹‘𝑥) ∈ 𝐵) |
230 | 225 | difeq1d 3727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝐴 ∖ ran 𝐻) = ((𝑚...𝑛) ∖ ran 𝐻)) |
231 | 230 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (𝑥 ∈ (𝐴 ∖ ran 𝐻) ↔ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻))) |
232 | 231 | biimpar 502 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → 𝑥 ∈ (𝐴 ∖ ran 𝐻)) |
233 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝜑) |
234 | 233, 52 | sylan 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
235 | 232, 234 | syldan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑥 ∈ ((𝑚...𝑛) ∖ ran 𝐻)) → (𝐹‘𝑥) = 0 ) |
236 | | f1of 6137 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(#‘ran 𝐻))–1-1-onto→ran
𝐻 → 𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻) |
237 | 162, 163,
236 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → 𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻) |
238 | | fvco3 6275 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(#‘ran 𝐻))⟶ran 𝐻 ∧ 𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
239 | 237, 238 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) ∧ 𝑦 ∈ (1...(#‘ran 𝐻))) → ((𝐹 ∘ 𝑓)‘𝑦) = (𝐹‘(𝑓‘𝑦))) |
240 | 210, 212,
148, 213, 162, 223, 224, 229, 235, 239 | seqcoll2 13249 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘ran 𝐻))) |
241 | 144, 208,
240 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (𝐴 = (𝑚...𝑛) ∧ 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
242 | 241 | expr 643 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
243 | 242 | exlimdv 1861 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (∃𝑓 𝑓 Isom < , < ((1...(#‘ran 𝐻)), ran 𝐻) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛))) |
244 | 135, 243 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq𝑚( + , 𝐹)‘𝑛)) |
245 | 110, 244 | eqtr4d 2659 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ 𝐴 = (𝑚...𝑛)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
246 | 245 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
247 | 246 | rexlimdvw 3034 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
248 | 247 | rexlimdvw 3034 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ 𝐴 = (𝑚...𝑛) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
249 | 82, 248 | syl5bi 232 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐴 ∈ ran ... → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
250 | | suppssdm 7308 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
251 | 32, 250 | eqsstri 3635 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
252 | | fdm 6051 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵 → dom (𝐹 ∘ 𝐻) = (1...𝑀)) |
253 | 30, 252 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝐹 ∘ 𝐻) = (1...𝑀)) |
254 | 251, 253 | syl5sseq 3653 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
255 | | fzssuz 12382 |
. . . . . . . . . . 11
⊢
(1...𝑀) ⊆
(ℤ≥‘1) |
256 | 255, 70 | sseqtr4i 3638 |
. . . . . . . . . 10
⊢
(1...𝑀) ⊆
ℕ |
257 | | nnssre 11024 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ |
258 | 256, 257 | sstri 3612 |
. . . . . . . . 9
⊢
(1...𝑀) ⊆
ℝ |
259 | 254, 258 | syl6ss 3615 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ ℝ) |
260 | | soss 5053 |
. . . . . . . 8
⊢ (𝑊 ⊆ ℝ → ( <
Or ℝ → < Or 𝑊)) |
261 | 259, 121,
260 | mpisyl 21 |
. . . . . . 7
⊢ (𝜑 → < Or 𝑊) |
262 | | ssfi 8180 |
. . . . . . . 8
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
263 | 124, 254,
262 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) |
264 | | fz1iso 13246 |
. . . . . . 7
⊢ (( <
Or 𝑊 ∧ 𝑊 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊)) |
265 | 261, 263,
264 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊)) |
266 | 265 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊)) |
267 | 62, 3, 65, 152, 1, 2, 7, 149, 69, 10, 50, 32 | gsumval3lem2 18307 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊))) |
268 | 1 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd) |
269 | 268, 209 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
270 | 268, 211 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
271 | 268, 147 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
272 | 268, 63 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 0 ∈ 𝐵) |
273 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊)) |
274 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑊 ≠ ∅) |
275 | 254 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀)) |
276 | 30 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
277 | 276 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ (1...𝑀)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵) |
278 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ 𝑊) |
279 | | ovexd 6680 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (1...𝑀) ∈ V) |
280 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 0 ∈ V) |
281 | 276, 278,
279, 280 | suppssr 7326 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ 𝑥 ∈ ((1...𝑀) ∖ 𝑊)) → ((𝐹 ∘ 𝐻)‘𝑥) = 0 ) |
282 | | coass 5654 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐻) ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ 𝑓)) |
283 | 282 | fveq1i 6192 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) |
284 | | isof1o 6573 |
. . . . . . . . . . . 12
⊢ (𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊) → 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊) |
285 | | f1of 6137 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))⟶𝑊) |
286 | 273, 284,
285 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝑊) |
287 | | fvco3 6275 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘𝑊))⟶𝑊 ∧ 𝑦 ∈ (1...(#‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
288 | 286, 287 | sylan 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → (((𝐹 ∘ 𝐻) ∘ 𝑓)‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
289 | 283, 288 | syl5eqr 2670 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) ∧ 𝑦 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ (𝐻 ∘ 𝑓))‘𝑦) = ((𝐹 ∘ 𝐻)‘(𝑓‘𝑦))) |
290 | 269, 270,
271, 272, 273, 274, 275, 277, 281, 289 | seqcoll2 13249 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ 𝐻))‘𝑀) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊))) |
291 | 267, 290 | eqtr4d 2659 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
292 | 291 | expr 643 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
293 | 292 | exlimdv 1861 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (∃𝑓 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
294 | 266, 293 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ ¬ 𝐴 ∈ ran ...) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
295 | 294 | ex 450 |
. . 3
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (¬ 𝐴 ∈ ran ... → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀))) |
296 | 249, 295 | pm2.61d 170 |
. 2
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |
297 | 78, 296 | pm2.61dane 2881 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) |