Proof of Theorem gsumval3lem1
| Step | Hyp | Ref
| Expression |
| 1 | | gsumval3.h |
. . . . . . 7
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
| 2 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐻:(1...𝑀)–1-1→𝐴) |
| 3 | | gsumval3.w |
. . . . . . . . 9
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
| 4 | | suppssdm 8202 |
. . . . . . . . 9
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
| 5 | 3, 4 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
| 6 | | gsumval3.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 7 | | f1f 6804 |
. . . . . . . . . 10
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
| 8 | 1, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
| 9 | | fco 6760 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
| 10 | 6, 8, 9 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
| 11 | 5, 10 | fssdm 6755 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
| 12 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) |
| 13 | | f1ores 6862 |
. . . . . 6
⊢ ((𝐻:(1...𝑀)–1-1→𝐴 ∧ 𝑊 ⊆ (1...𝑀)) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
| 14 | 2, 12, 13 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
| 15 | 3 | imaeq2i 6076 |
. . . . . . 7
⊢ (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) |
| 16 | | gsumval3.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 17 | 6, 16 | fexd 7247 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) |
| 18 | | ovex 7464 |
. . . . . . . . . . . 12
⊢
(1...𝑀) ∈
V |
| 19 | | fex 7246 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐻 ∈ V) |
| 20 | 7, 18, 19 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻 ∈ V) |
| 21 | 1, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ V) |
| 22 | | f1fun 6806 |
. . . . . . . . . . . 12
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → Fun 𝐻) |
| 23 | 1, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐻) |
| 24 | | gsumval3.n |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
| 25 | 23, 24 | jca 511 |
. . . . . . . . . 10
⊢ (𝜑 → (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) |
| 26 | 17, 21, 25 | jca31 514 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
| 27 | 26 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
| 28 | | imacosupp 8234 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 ))) |
| 29 | 28 | imp 406 |
. . . . . . . 8
⊢ (((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
| 30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
| 31 | 15, 30 | eqtrid 2789 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
| 32 | 31 | f1oeq3d 6845 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
| 33 | 14, 32 | mpbid 232 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) |
| 34 | | isof1o 7343 |
. . . . 5
⊢ (𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
| 35 | 34 | ad2antll 729 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
| 36 | | f1oco 6871 |
. . . 4
⊢ (((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ) ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) → ((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 )) |
| 37 | 33, 35, 36 | syl2anc 584 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 )) |
| 38 | | f1of 6848 |
. . . . 5
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
| 39 | | frn 6743 |
. . . . 5
⊢ (𝑓:(1...(♯‘𝑊))⟶𝑊 → ran 𝑓 ⊆ 𝑊) |
| 40 | 35, 38, 39 | 3syl 18 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ran 𝑓 ⊆ 𝑊) |
| 41 | | cores 6269 |
. . . 4
⊢ (ran
𝑓 ⊆ 𝑊 → ((𝐻 ↾ 𝑊) ∘ 𝑓) = (𝐻 ∘ 𝑓)) |
| 42 | | f1oeq1 6836 |
. . . 4
⊢ (((𝐻 ↾ 𝑊) ∘ 𝑓) = (𝐻 ∘ 𝑓) → (((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ))) |
| 43 | 40, 41, 42 | 3syl 18 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ))) |
| 44 | 37, 43 | mpbid 232 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 )) |
| 45 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑀) ∈
Fin |
| 46 | | ssfi 9213 |
. . . . . . 7
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
| 47 | 45, 11, 46 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Fin) |
| 48 | 47 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ∈ Fin) |
| 49 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )) |
| 50 | 49 | imaeq2d 6078 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 ))) |
| 51 | 45 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 52 | 8, 51 | fexd 7247 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ V) |
| 53 | 17, 52, 25 | jca31 514 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
| 54 | 53 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
| 55 | 54, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
| 56 | 50, 55 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
| 57 | 56 | f1oeq3d 6845 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
| 58 | 14, 57 | mpbid 232 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) |
| 59 | 48, 58 | hasheqf1od 14392 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) →
(♯‘𝑊) =
(♯‘(𝐹 supp
0
))) |
| 60 | 59 | oveq2d 7447 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) →
(1...(♯‘𝑊)) =
(1...(♯‘(𝐹 supp
0
)))) |
| 61 | 60 | f1oeq2d 6844 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) |
| 62 | 44, 61 | mpbid 232 |
1
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) |