Step | Hyp | Ref
| Expression |
1 | | gsumval3.h |
. . . . . . 7
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
2 | | f1f 6568 |
. . . . . . 7
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
4 | | fzfid 13329 |
. . . . . 6
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
5 | | gsumval3.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | | fex2 7627 |
. . . . . 6
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
7 | 3, 4, 5, 6 | syl3anc 1363 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ V) |
8 | | vex 3495 |
. . . . 5
⊢ 𝑓 ∈ V |
9 | | coexg 7623 |
. . . . 5
⊢ ((𝐻 ∈ V ∧ 𝑓 ∈ V) → (𝐻 ∘ 𝑓) ∈ V) |
10 | 7, 8, 9 | sylancl 586 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ 𝑓) ∈ V) |
11 | 10 | ad2antrr 722 |
. . 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 18954 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) |
23 | | fzfi 13328 |
. . . . . . . 8
⊢
(1...𝑀) ∈
Fin |
24 | | suppssdm 7832 |
. . . . . . . . . 10
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
25 | 21, 24 | eqsstri 3998 |
. . . . . . . . 9
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
26 | | fco 6524 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
27 | 17, 3, 26 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
28 | 25, 27 | fssdm 6523 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
29 | | ssfi 8726 |
. . . . . . . 8
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
30 | 23, 28, 29 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) |
31 | 30 | ad2antrr 722 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ∈ Fin) |
32 | 1 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐻:(1...𝑀)–1-1→𝐴) |
33 | 28 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) |
34 | | f1ores 6622 |
. . . . . . . 8
⊢ ((𝐻:(1...𝑀)–1-1→𝐴 ∧ 𝑊 ⊆ (1...𝑀)) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
35 | 32, 33, 34 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
36 | 21 | imaeq2i 5920 |
. . . . . . . . . 10
⊢ (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) |
37 | | fex 6980 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
38 | 17, 5, 37 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
39 | | ovex 7178 |
. . . . . . . . . . . . . 14
⊢
(1...𝑀) ∈
V |
40 | | fex 6980 |
. . . . . . . . . . . . . 14
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐻 ∈ V) |
41 | 3, 39, 40 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ V) |
42 | 38, 41 | jca 512 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐻 ∈ V)) |
43 | | f1fun 6570 |
. . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → Fun 𝐻) |
44 | 1, 43 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐻) |
45 | 44, 20 | jca 512 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) |
46 | | imacosupp 7863 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 ))) |
47 | 42, 45, 46 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
48 | 47 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
49 | 36, 48 | syl5eq 2865 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
50 | 49 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
51 | 50 | f1oeq3d 6605 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
52 | 35, 51 | mpbid 233 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) |
53 | 31, 52 | hasheqf1od 13702 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) →
(♯‘𝑊) =
(♯‘(𝐹 supp
0
))) |
54 | 53 | fveq2d 6667 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))) |
55 | 22, 54 | jca 512 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 ))))) |
56 | | f1oeq1 6597 |
. . . 4
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) |
57 | | coeq2 5722 |
. . . . . . 7
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝐻 ∘ 𝑓))) |
58 | 57 | seqeq3d 13365 |
. . . . . 6
⊢ (𝑔 = (𝐻 ∘ 𝑓) → seq1( + , (𝐹 ∘ 𝑔)) = seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))) |
59 | 58 | fveq1d 6665 |
. . . . 5
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))) |
60 | 59 | eqeq2d 2829 |
. . . 4
⊢ (𝑔 = (𝐻 ∘ 𝑓) → ((seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))) ↔ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 ))))) |
61 | 56, 60 | anbi12d 630 |
. . 3
⊢ (𝑔 = (𝐻 ∘ 𝑓) → ((𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ ((𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))))) |
62 | 11, 55, 61 | spcedv 3596 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) |
63 | 16 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐺 ∈ Mnd) |
64 | 5 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐴 ∈ 𝑉) |
65 | 17 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐹:𝐴⟶𝐵) |
66 | 18 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
67 | | f1f1orn 6619 |
. . . . . . . . . . . . 13
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
68 | 1, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) |
69 | | f1oen3g 8513 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) |
70 | 7, 68, 69 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) |
71 | | enfi 8722 |
. . . . . . . . . . 11
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) |
73 | 23, 72 | mpbii 234 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
74 | 73, 20 | ssfid 8729 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
75 | 74 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ∈
Fin) |
76 | 21 | neeq1i 3077 |
. . . . . . . . . 10
⊢ (𝑊 ≠ ∅ ↔ ((𝐹 ∘ 𝐻) supp 0 ) ≠
∅) |
77 | | supp0cosupp0 7861 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((𝐹 supp 0 ) = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅)) |
78 | 77 | necon3d 3034 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → (((𝐹 ∘ 𝐻) supp 0 ) ≠ ∅ →
(𝐹 supp 0 ) ≠
∅)) |
79 | 38, 41, 78 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐹 ∘ 𝐻) supp 0 ) ≠ ∅ →
(𝐹 supp 0 ) ≠
∅)) |
80 | 76, 79 | syl5bi 243 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 ≠ ∅ → (𝐹 supp 0 ) ≠
∅)) |
81 | 80 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐹 supp 0 ) ≠
∅) |
82 | 81 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ≠
∅) |
83 | 20 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ⊆ ran 𝐻) |
84 | 3 | frnd 6514 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) |
85 | 84 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ran 𝐻 ⊆ 𝐴) |
86 | 83, 85 | sstrd 3974 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ⊆ 𝐴) |
87 | 12, 13, 14, 15, 63, 64, 65, 66, 75, 82, 86 | gsumval3eu 18953 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ∃!𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) |
88 | | iota1 6325 |
. . . . . 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 ))))) = 𝑥)) |
89 | 87, 88 | 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 ))))) = 𝑥)) |
90 | | eqid 2818 |
. . . . . . 7
⊢ (𝐹 supp 0 ) = (𝐹 supp 0 ) |
91 | | simprl 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ¬ 𝐴 ∈ ran
...) |
92 | 12, 13, 14, 15, 63, 64, 65, 66, 75, 82, 90, 91 | gsumval3a 18952 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (℩𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))))) |
93 | 92 | eqeq1d 2820 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐺 Σg
𝐹) = 𝑥 ↔ (℩𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) = 𝑥)) |
94 | 89, 93 | bitr4d 283 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥)) |
95 | 94 | alrimiv 1919 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ∀𝑥(∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥)) |
96 | | fvex 6676 |
. . . 4
⊢ (seq1(
+ ,
(𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) ∈ V |
97 | | eqeq1 2822 |
. . . . . . 7
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → (𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))) ↔ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) |
98 | 97 | anbi2d 628 |
. . . . . 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 )))))) |
99 | 98 | exbidv 1913 |
. . . . 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 )))))) |
100 | | eqeq2 2830 |
. . . . 5
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → ((𝐺 Σg 𝐹) = 𝑥 ↔ (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))) |
101 | 99, 100 | bibi12d 347 |
. . . 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( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))))) |
102 | 96, 101 | spcv 3603 |
. . 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( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))) |
103 | 95, 102 | syl 17 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))) |
104 | 62, 103 | mpbid 233 |
1
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |