Step | Hyp | Ref
| Expression |
1 | | gsumval3.h |
. . . . . . 7
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
2 | | f1f 6014 |
. . . . . . 7
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
4 | | fzfid 12634 |
. . . . . 6
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
5 | | gsumval3.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | | fex2 7014 |
. . . . . 6
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
7 | 3, 4, 5, 6 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ V) |
8 | | vex 3176 |
. . . . 5
⊢ 𝑓 ∈ V |
9 | | coexg 7010 |
. . . . 5
⊢ ((𝐻 ∈ V ∧ 𝑓 ∈ V) → (𝐻 ∘ 𝑓) ∈ V) |
10 | 7, 8, 9 | sylancl 693 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ 𝑓) ∈ V) |
11 | 10 | ad2antrr 758 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐻 ∘ 𝑓) ∈ V) |
12 | | gsumval3.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
13 | | gsumval3.0 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
14 | | gsumval3.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
15 | | gsumval3.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝐺) |
16 | | gsumval3.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) |
17 | | gsumval3.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
18 | | gsumval3.c |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
19 | | gsumval3.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) |
20 | | gsumval3.n |
. . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
21 | | gsumval3.w |
. . . . 5
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
22 | 12, 13, 14, 15, 16, 5, 17, 18, 19, 1, 20, 21 | gsumval3lem1 18129 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐻 ∘ 𝑓):(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) |
23 | | resexg 5362 |
. . . . . . . . 9
⊢ (𝐻 ∈ V → (𝐻 ↾ 𝑊) ∈ V) |
24 | 7, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 ↾ 𝑊) ∈ V) |
25 | 24 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐻 ↾ 𝑊) ∈ V) |
26 | 1 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝐻:(1...𝑀)–1-1→𝐴) |
27 | | suppssdm 7195 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
28 | 21, 27 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
29 | | fco 5971 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
30 | 17, 3, 29 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
31 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵 → dom (𝐹 ∘ 𝐻) = (1...𝑀)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝐹 ∘ 𝐻) = (1...𝑀)) |
33 | 28, 32 | syl5sseq 3616 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
34 | 33 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑊 ⊆ (1...𝑀)) |
35 | | f1ores 6064 |
. . . . . . . . 9
⊢ ((𝐻:(1...𝑀)–1-1→𝐴 ∧ 𝑊 ⊆ (1...𝑀)) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
36 | 26, 34, 35 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
37 | 21 | imaeq2i 5383 |
. . . . . . . . . . 11
⊢ (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) |
38 | | fex 6394 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
39 | 17, 5, 38 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ V) |
40 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑀) ∈
V |
41 | | fex 6394 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐻 ∈ V) |
42 | 3, 40, 41 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ V) |
43 | 39, 42 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐻 ∈ V)) |
44 | | f1fun 6016 |
. . . . . . . . . . . . . . 15
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → Fun 𝐻) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Fun 𝐻) |
46 | 45, 20 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) |
47 | | imacosupp 7222 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 ))) |
48 | 43, 46, 47 | sylc 63 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
49 | 48 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
50 | 37, 49 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
52 | | f1oeq3 6042 |
. . . . . . . . 9
⊢ ((𝐻 “ 𝑊) = (𝐹 supp 0 ) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
54 | 36, 53 | mpbid 221 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) |
55 | | f1oen3g 7857 |
. . . . . . 7
⊢ (((𝐻 ↾ 𝑊) ∈ V ∧ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) → 𝑊 ≈ (𝐹 supp 0 )) |
56 | 25, 54, 55 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑊 ≈ (𝐹 supp 0 )) |
57 | | fzfi 12633 |
. . . . . . . . 9
⊢
(1...𝑀) ∈
Fin |
58 | | ssfi 8065 |
. . . . . . . . 9
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
59 | 57, 33, 58 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Fin) |
60 | 59 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝑊 ∈ Fin) |
61 | | f1f1orn 6061 |
. . . . . . . . . . . . 13
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
62 | 1, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
63 | | f1oen3g 7857 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) |
64 | 7, 62, 63 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) |
65 | | enfi 8061 |
. . . . . . . . . . 11
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
67 | 57, 66 | mpbii 222 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
68 | | ssfi 8065 |
. . . . . . . . 9
⊢ ((ran
𝐻 ∈ Fin ∧ (𝐹 supp 0 ) ⊆ ran 𝐻) → (𝐹 supp 0 ) ∈
Fin) |
69 | 67, 20, 68 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
70 | 69 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐹 supp 0 ) ∈
Fin) |
71 | | hashen 12997 |
. . . . . . 7
⊢ ((𝑊 ∈ Fin ∧ (𝐹 supp 0 ) ∈ Fin) →
((#‘𝑊) =
(#‘(𝐹 supp 0 )) ↔
𝑊 ≈ (𝐹 supp 0 ))) |
72 | 60, 70, 71 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ((#‘𝑊) = (#‘(𝐹 supp 0 )) ↔ 𝑊 ≈ (𝐹 supp 0 ))) |
73 | 56, 72 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (#‘𝑊) = (#‘(𝐹 supp 0 ))) |
74 | 73 | fveq2d 6107 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘(𝐹 supp 0 )))) |
75 | 22, 74 | jca 553 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ((𝐻 ∘ 𝑓):(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘(𝐹 supp 0 ))))) |
76 | | f1oeq1 6040 |
. . . . 5
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) |
77 | | coeq2 5202 |
. . . . . . . 8
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝐻 ∘ 𝑓))) |
78 | 77 | seqeq3d 12671 |
. . . . . . 7
⊢ (𝑔 = (𝐻 ∘ 𝑓) → seq1( + , (𝐹 ∘ 𝑔)) = seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))) |
79 | 78 | fveq1d 6105 |
. . . . . 6
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘(𝐹 supp 0 )))) |
80 | 79 | eqeq2d 2620 |
. . . . 5
⊢ (𝑔 = (𝐻 ∘ 𝑓) → ((seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))) ↔ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘(𝐹 supp 0 ))))) |
81 | 76, 80 | anbi12d 743 |
. . . 4
⊢ (𝑔 = (𝐻 ∘ 𝑓) → ((𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ ((𝐻 ∘ 𝑓):(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘(𝐹 supp 0 )))))) |
82 | 81 | spcegv 3267 |
. . 3
⊢ ((𝐻 ∘ 𝑓) ∈ V → (((𝐻 ∘ 𝑓):(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘(𝐹 supp 0 )))) → ∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))))) |
83 | 11, 75, 82 | sylc 63 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))))) |
84 | 16 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝐺 ∈ Mnd) |
85 | 5 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝐴 ∈ 𝑉) |
86 | 17 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → 𝐹:𝐴⟶𝐵) |
87 | 18 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
88 | 21 | neeq1i 2846 |
. . . . . . . . . 10
⊢ (𝑊 ≠ ∅ ↔ ((𝐹 ∘ 𝐻) supp 0 ) ≠
∅) |
89 | | supp0cosupp0 7221 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((𝐹 supp 0 ) = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅)) |
90 | 89 | necon3d 2803 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → (((𝐹 ∘ 𝐻) supp 0 ) ≠ ∅ →
(𝐹 supp 0 ) ≠
∅)) |
91 | 39, 42, 90 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐹 ∘ 𝐻) supp 0 ) ≠ ∅ →
(𝐹 supp 0 ) ≠
∅)) |
92 | 88, 91 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 ≠ ∅ → (𝐹 supp 0 ) ≠
∅)) |
93 | 92 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐹 supp 0 ) ≠
∅) |
94 | 93 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐹 supp 0 ) ≠
∅) |
95 | 20 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐹 supp 0 ) ⊆ ran 𝐻) |
96 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐻:(1...𝑀)⟶𝐴 → ran 𝐻 ⊆ 𝐴) |
97 | 3, 96 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) |
98 | 97 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ran 𝐻 ⊆ 𝐴) |
99 | 95, 98 | sstrd 3578 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐹 supp 0 ) ⊆ 𝐴) |
100 | 12, 13, 14, 15, 84, 85, 86, 87, 70, 94, 99 | gsumval3eu 18128 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ∃!𝑥∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))))) |
101 | | iota1 5782 |
. . . . . 6
⊢
(∃!𝑥∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) → (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (℩𝑥∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))))) = 𝑥)) |
102 | 100, 101 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (℩𝑥∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))))) = 𝑥)) |
103 | | eqid 2610 |
. . . . . . 7
⊢ (𝐹 supp 0 ) = (𝐹 supp 0 ) |
104 | | simprl 790 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ¬ 𝐴 ∈ ran
...) |
105 | 12, 13, 14, 15, 84, 85, 86, 87, 70, 94, 103, 104 | gsumval3a 18127 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (℩𝑥∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))))) |
106 | 105 | eqeq1d 2612 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ((𝐺 Σg 𝐹) = 𝑥 ↔ (℩𝑥∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))))) = 𝑥)) |
107 | 102, 106 | bitr4d 270 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥)) |
108 | 107 | alrimiv 1842 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → ∀𝑥(∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥)) |
109 | | fvex 6113 |
. . . 4
⊢ (seq1(
+ ,
(𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) ∈ V |
110 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) → (𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))) ↔ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 ))))) |
111 | 110 | anbi2d 736 |
. . . . . 6
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) → ((𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))))) |
112 | 111 | exbidv 1837 |
. . . . 5
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) → (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ ∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))))) |
113 | | eqeq2 2621 |
. . . . 5
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) → ((𝐺 Σg 𝐹) = 𝑥 ↔ (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)))) |
114 | 112, 113 | bibi12d 334 |
. . . 4
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) → ((∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥) ↔ (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊))))) |
115 | 109, 114 | spcv 3272 |
. . 3
⊢
(∀𝑥(∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥) → (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)))) |
116 | 108, 115 | syl 17 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (∃𝑔(𝑔:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(#‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊)))) |
117 | 83, 116 | mpbid 221 |
1
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊))) |