Proof of Theorem gsumval3lem1
Step | Hyp | Ref
| Expression |
1 | | gsumval3.h |
. . . . . . 7
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) |
2 | 1 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐻:(1...𝑀)–1-1→𝐴) |
3 | | gsumval3.w |
. . . . . . . . 9
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) |
4 | | suppssdm 7843 |
. . . . . . . . 9
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) |
5 | 3, 4 | eqsstri 4001 |
. . . . . . . 8
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) |
6 | | gsumval3.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
7 | | f1f 6575 |
. . . . . . . . . 10
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) |
8 | 1, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) |
9 | | fco 6531 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:(1...𝑀)⟶𝐴) → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
10 | 6, 8, 9 | syl2anc 586 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) |
11 | 5, 10 | fssdm 6530 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) |
12 | 11 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) |
13 | | f1ores 6629 |
. . . . . 6
⊢ ((𝐻:(1...𝑀)–1-1→𝐴 ∧ 𝑊 ⊆ (1...𝑀)) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
14 | 2, 12, 13 | syl2anc 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) |
15 | 3 | imaeq2i 5927 |
. . . . . . 7
⊢ (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) |
16 | | gsumval3.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
17 | | fex 6989 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
18 | 6, 16, 17 | syl2anc 586 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) |
19 | | ovex 7189 |
. . . . . . . . . . . 12
⊢
(1...𝑀) ∈
V |
20 | | fex 6989 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐻 ∈ V) |
21 | 7, 19, 20 | sylancl 588 |
. . . . . . . . . . 11
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻 ∈ V) |
22 | 1, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ V) |
23 | | f1fun 6577 |
. . . . . . . . . . . 12
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → Fun 𝐻) |
24 | 1, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐻) |
25 | | gsumval3.n |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) |
26 | 24, 25 | jca 514 |
. . . . . . . . . 10
⊢ (𝜑 → (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) |
27 | 18, 22, 26 | jca31 517 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
28 | 27 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
29 | | imacosupp 7874 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 ))) |
30 | 29 | imp 409 |
. . . . . . . 8
⊢ (((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
31 | 28, 30 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
32 | 15, 31 | syl5eq 2868 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
33 | 32 | f1oeq3d 6612 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
34 | 14, 33 | mpbid 234 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) |
35 | | isof1o 7076 |
. . . . 5
⊢ (𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
36 | 35 | ad2antll 727 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) |
37 | | f1oco 6637 |
. . . 4
⊢ (((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ) ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) → ((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 )) |
38 | 34, 36, 37 | syl2anc 586 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 )) |
39 | | f1of 6615 |
. . . . 5
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))⟶𝑊) |
40 | | frn 6520 |
. . . . 5
⊢ (𝑓:(1...(♯‘𝑊))⟶𝑊 → ran 𝑓 ⊆ 𝑊) |
41 | 36, 39, 40 | 3syl 18 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ran 𝑓 ⊆ 𝑊) |
42 | | cores 6102 |
. . . 4
⊢ (ran
𝑓 ⊆ 𝑊 → ((𝐻 ↾ 𝑊) ∘ 𝑓) = (𝐻 ∘ 𝑓)) |
43 | | f1oeq1 6604 |
. . . 4
⊢ (((𝐻 ↾ 𝑊) ∘ 𝑓) = (𝐻 ∘ 𝑓) → (((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ))) |
44 | 41, 42, 43 | 3syl 18 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (((𝐻 ↾ 𝑊) ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ))) |
45 | 38, 44 | mpbid 234 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 )) |
46 | | fzfi 13341 |
. . . . . . 7
⊢
(1...𝑀) ∈
Fin |
47 | | ssfi 8738 |
. . . . . . 7
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) |
48 | 46, 11, 47 | sylancr 589 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Fin) |
49 | 48 | ad2antrr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ∈ Fin) |
50 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 = ((𝐹 ∘ 𝐻) supp 0 )) |
51 | 50 | imaeq2d 5929 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 ))) |
52 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
53 | | fex2 7638 |
. . . . . . . . . . . 12
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
54 | 8, 52, 16, 53 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ V) |
55 | 18, 54, 26 | jca31 517 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
56 | 55 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐹 ∈ V ∧ 𝐻 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻))) |
57 | 56, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) |
58 | 51, 57 | eqtrd 2856 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) |
59 | 58 | f1oeq3d 6612 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) |
60 | 14, 59 | mpbid 234 |
. . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) |
61 | 49, 60 | hasheqf1od 13715 |
. . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) →
(♯‘𝑊) =
(♯‘(𝐹 supp
0
))) |
62 | 61 | oveq2d 7172 |
. . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) →
(1...(♯‘𝑊)) =
(1...(♯‘(𝐹 supp
0
)))) |
63 | 62 | f1oeq2d 6611 |
. 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ∘ 𝑓):(1...(♯‘𝑊))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) |
64 | 45, 63 | mpbid 234 |
1
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) |