Step | Hyp | Ref
| Expression |
1 | | gsumval2.b |
. . . 4
β’ π΅ = (BaseβπΊ) |
2 | | eqid 2732 |
. . . 4
β’
(0gβπΊ) = (0gβπΊ) |
3 | | gsumval2.p |
. . . 4
β’ + =
(+gβπΊ) |
4 | | gsumval2a.o |
. . . 4
β’ π = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ + π¦) = π¦ β§ (π¦ + π₯) = π¦)} |
5 | | eqidd 2733 |
. . . 4
β’ (π β (β‘πΉ β (V β π)) = (β‘πΉ β (V β π))) |
6 | | gsumval2.g |
. . . 4
β’ (π β πΊ β π) |
7 | | ovexd 7446 |
. . . 4
β’ (π β (π...π) β V) |
8 | | gsumval2.f |
. . . 4
β’ (π β πΉ:(π...π)βΆπ΅) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | gsumval 18598 |
. . 3
β’ (π β (πΊ Ξ£g πΉ) = if(ran πΉ β π, (0gβπΊ), if((π...π) β ran ..., (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))), (β©π§βπ(π:(1...(β―β(β‘πΉ β (V β π))))β1-1-ontoβ(β‘πΉ β (V β π)) β§ π§ = (seq1( + , (πΉ β π))β(β―β(β‘πΉ β (V β π))))))))) |
10 | | gsumval2a.f |
. . . . 5
β’ (π β Β¬ ran πΉ β π) |
11 | 10 | iffalsed 4539 |
. . . 4
β’ (π β if(ran πΉ β π, (0gβπΊ), if((π...π) β ran ..., (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))), (β©π§βπ(π:(1...(β―β(β‘πΉ β (V β π))))β1-1-ontoβ(β‘πΉ β (V β π)) β§ π§ = (seq1( + , (πΉ β π))β(β―β(β‘πΉ β (V β π)))))))) = if((π...π) β ran ..., (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))), (β©π§βπ(π:(1...(β―β(β‘πΉ β (V β π))))β1-1-ontoβ(β‘πΉ β (V β π)) β§ π§ = (seq1( + , (πΉ β π))β(β―β(β‘πΉ β (V β π)))))))) |
12 | | fzf 13490 |
. . . . . . 7
β’
...:(β€ Γ β€)βΆπ« β€ |
13 | | ffn 6717 |
. . . . . . 7
β’
(...:(β€ Γ β€)βΆπ« β€ β ... Fn
(β€ Γ β€)) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
β’ ... Fn
(β€ Γ β€) |
15 | | gsumval2.n |
. . . . . . 7
β’ (π β π β (β€β₯βπ)) |
16 | | eluzel2 12829 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
17 | 15, 16 | syl 17 |
. . . . . 6
β’ (π β π β β€) |
18 | | eluzelz 12834 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
19 | 15, 18 | syl 17 |
. . . . . 6
β’ (π β π β β€) |
20 | | fnovrn 7584 |
. . . . . 6
β’ ((... Fn
(β€ Γ β€) β§ π β β€ β§ π β β€) β (π...π) β ran ...) |
21 | 14, 17, 19, 20 | mp3an2i 1466 |
. . . . 5
β’ (π β (π...π) β ran ...) |
22 | 21 | iftrued 4536 |
. . . 4
β’ (π β if((π...π) β ran ..., (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))), (β©π§βπ(π:(1...(β―β(β‘πΉ β (V β π))))β1-1-ontoβ(β‘πΉ β (V β π)) β§ π§ = (seq1( + , (πΉ β π))β(β―β(β‘πΉ β (V β π))))))) = (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
23 | 11, 22 | eqtrd 2772 |
. . 3
β’ (π β if(ran πΉ β π, (0gβπΊ), if((π...π) β ran ..., (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))), (β©π§βπ(π:(1...(β―β(β‘πΉ β (V β π))))β1-1-ontoβ(β‘πΉ β (V β π)) β§ π§ = (seq1( + , (πΉ β π))β(β―β(β‘πΉ β (V β π)))))))) = (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
24 | 9, 23 | eqtrd 2772 |
. 2
β’ (π β (πΊ Ξ£g πΉ) = (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
25 | | fvex 6904 |
. . 3
β’ (seqπ( + , πΉ)βπ) β V |
26 | | fzopth 13540 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β ((π...π) = (π...π) β (π = π β§ π = π))) |
27 | 15, 26 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π...π) = (π...π) β (π = π β§ π = π))) |
28 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = π) β π = π) |
29 | 28 | seqeq1d 13974 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β seqπ( + , πΉ) = seqπ( + , πΉ)) |
30 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β π = π) |
31 | 29, 30 | fveq12d 6898 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ)) |
32 | 31 | eqcomd 2738 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ)) |
33 | | eqeq1 2736 |
. . . . . . . . . . 11
β’ (π§ = (seqπ( + , πΉ)βπ) β (π§ = (seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ))) |
34 | 32, 33 | syl5ibrcom 246 |
. . . . . . . . . 10
β’ ((π = π β§ π = π) β (π§ = (seqπ( + , πΉ)βπ) β π§ = (seqπ( + , πΉ)βπ))) |
35 | 27, 34 | syl6bi 252 |
. . . . . . . . 9
β’ (π β ((π...π) = (π...π) β (π§ = (seqπ( + , πΉ)βπ) β π§ = (seqπ( + , πΉ)βπ)))) |
36 | 35 | impd 411 |
. . . . . . . 8
β’ (π β (((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β π§ = (seqπ( + , πΉ)βπ))) |
37 | 36 | rexlimdvw 3160 |
. . . . . . 7
β’ (π β (βπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β π§ = (seqπ( + , πΉ)βπ))) |
38 | 37 | exlimdv 1936 |
. . . . . 6
β’ (π β (βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β π§ = (seqπ( + , πΉ)βπ))) |
39 | 17 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π§ = (seqπ( + , πΉ)βπ)) β π β β€) |
40 | | oveq2 7419 |
. . . . . . . . . . . . 13
β’ (π = π β (π...π) = (π...π)) |
41 | 40 | eqcomd 2738 |
. . . . . . . . . . . 12
β’ (π = π β (π...π) = (π...π)) |
42 | 41 | biantrurd 533 |
. . . . . . . . . . 11
β’ (π = π β (π§ = (seqπ( + , πΉ)βπ) β ((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
43 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π = π β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ)) |
44 | 43 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ (π = π β (π§ = (seqπ( + , πΉ)βπ) β π§ = (seqπ( + , πΉ)βπ))) |
45 | 42, 44 | bitr3d 280 |
. . . . . . . . . 10
β’ (π = π β (((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β π§ = (seqπ( + , πΉ)βπ))) |
46 | 45 | rspcev 3612 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π§ = (seqπ( + , πΉ)βπ)) β βπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))) |
47 | 15, 46 | sylan 580 |
. . . . . . . 8
β’ ((π β§ π§ = (seqπ( + , πΉ)βπ)) β βπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))) |
48 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
49 | | oveq1 7418 |
. . . . . . . . . . . 12
β’ (π = π β (π...π) = (π...π)) |
50 | 49 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ (π = π β ((π...π) = (π...π) β (π...π) = (π...π))) |
51 | | seqeq1 13971 |
. . . . . . . . . . . . 13
β’ (π = π β seqπ( + , πΉ) = seqπ( + , πΉ)) |
52 | 51 | fveq1d 6893 |
. . . . . . . . . . . 12
β’ (π = π β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ)) |
53 | 52 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ (π = π β (π§ = (seqπ( + , πΉ)βπ) β π§ = (seqπ( + , πΉ)βπ))) |
54 | 50, 53 | anbi12d 631 |
. . . . . . . . . 10
β’ (π = π β (((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β ((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
55 | 48, 54 | rexeqbidv 3343 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β βπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
56 | 55 | spcegv 3587 |
. . . . . . . 8
β’ (π β β€ β
(βπ β
(β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
57 | 39, 47, 56 | sylc 65 |
. . . . . . 7
β’ ((π β§ π§ = (seqπ( + , πΉ)βπ)) β βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))) |
58 | 57 | ex 413 |
. . . . . 6
β’ (π β (π§ = (seqπ( + , πΉ)βπ) β βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)))) |
59 | 38, 58 | impbid 211 |
. . . . 5
β’ (π β (βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β π§ = (seqπ( + , πΉ)βπ))) |
60 | 59 | adantr 481 |
. . . 4
β’ ((π β§ (seqπ( + , πΉ)βπ) β V) β (βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ)) β π§ = (seqπ( + , πΉ)βπ))) |
61 | 60 | iota5 6526 |
. . 3
β’ ((π β§ (seqπ( + , πΉ)βπ) β V) β (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))) = (seqπ( + , πΉ)βπ)) |
62 | 25, 61 | mpan2 689 |
. 2
β’ (π β (β©π§βπβπ β (β€β₯βπ)((π...π) = (π...π) β§ π§ = (seqπ( + , πΉ)βπ))) = (seqπ( + , πΉ)βπ)) |
63 | 24, 62 | eqtrd 2772 |
1
β’ (π β (πΊ Ξ£g πΉ) = (seqπ( + , πΉ)βπ)) |