Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . 6
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . . . . 6
β’ βΌ = (
~FG βπΌ) |
3 | | efgval2.m |
. . . . . 6
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
4 | | efgval2.t |
. . . . . 6
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
5 | | efgred.d |
. . . . . 6
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
6 | | efgred.s |
. . . . . 6
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsdm 19639 |
. . . . 5
β’ (πΉ β dom π β (πΉ β (Word π β {β
}) β§ (πΉβ0) β π· β§ βπ β (1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1))))) |
8 | 7 | simp1bi 1145 |
. . . 4
β’ (πΉ β dom π β πΉ β (Word π β {β
})) |
9 | | eldifsn 4790 |
. . . . 5
β’ (πΉ β (Word π β {β
}) β (πΉ β Word π β§ πΉ β β
)) |
10 | | lennncl 14488 |
. . . . 5
β’ ((πΉ β Word π β§ πΉ β β
) β (β―βπΉ) β
β) |
11 | 9, 10 | sylbi 216 |
. . . 4
β’ (πΉ β (Word π β {β
}) β
(β―βπΉ) β
β) |
12 | | fzo0end 13728 |
. . . 4
β’
((β―βπΉ)
β β β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
13 | 8, 11, 12 | 3syl 18 |
. . 3
β’ (πΉ β dom π β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
14 | | nnm1nn0 12517 |
. . . . 5
β’
((β―βπΉ)
β β β ((β―βπΉ) β 1) β
β0) |
15 | 8, 11, 14 | 3syl 18 |
. . . 4
β’ (πΉ β dom π β ((β―βπΉ) β 1) β
β0) |
16 | | eleq1 2821 |
. . . . . . 7
β’ (π = 0 β (π β (0..^(β―βπΉ)) β 0 β (0..^(β―βπΉ)))) |
17 | | fveq2 6891 |
. . . . . . . 8
β’ (π = 0 β (πΉβπ) = (πΉβ0)) |
18 | 17 | breq2d 5160 |
. . . . . . 7
β’ (π = 0 β ((πΉβ0) βΌ (πΉβπ) β (πΉβ0) βΌ (πΉβ0))) |
19 | 16, 18 | imbi12d 344 |
. . . . . 6
β’ (π = 0 β ((π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ)) β (0 β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ0)))) |
20 | 19 | imbi2d 340 |
. . . . 5
β’ (π = 0 β ((πΉ β dom π β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ))) β (πΉ β dom π β (0 β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ0))))) |
21 | | eleq1 2821 |
. . . . . . 7
β’ (π = π β (π β (0..^(β―βπΉ)) β π β (0..^(β―βπΉ)))) |
22 | | fveq2 6891 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
23 | 22 | breq2d 5160 |
. . . . . . 7
β’ (π = π β ((πΉβ0) βΌ (πΉβπ) β (πΉβ0) βΌ (πΉβπ))) |
24 | 21, 23 | imbi12d 344 |
. . . . . 6
β’ (π = π β ((π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ)) β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ)))) |
25 | 24 | imbi2d 340 |
. . . . 5
β’ (π = π β ((πΉ β dom π β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ))) β (πΉ β dom π β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ))))) |
26 | | eleq1 2821 |
. . . . . . 7
β’ (π = (π + 1) β (π β (0..^(β―βπΉ)) β (π + 1) β (0..^(β―βπΉ)))) |
27 | | fveq2 6891 |
. . . . . . . 8
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
28 | 27 | breq2d 5160 |
. . . . . . 7
β’ (π = (π + 1) β ((πΉβ0) βΌ (πΉβπ) β (πΉβ0) βΌ (πΉβ(π + 1)))) |
29 | 26, 28 | imbi12d 344 |
. . . . . 6
β’ (π = (π + 1) β ((π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ)) β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ(π + 1))))) |
30 | 29 | imbi2d 340 |
. . . . 5
β’ (π = (π + 1) β ((πΉ β dom π β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ))) β (πΉ β dom π β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ(π + 1)))))) |
31 | | eleq1 2821 |
. . . . . . 7
β’ (π = ((β―βπΉ) β 1) β (π β
(0..^(β―βπΉ))
β ((β―βπΉ)
β 1) β (0..^(β―βπΉ)))) |
32 | | fveq2 6891 |
. . . . . . . 8
β’ (π = ((β―βπΉ) β 1) β (πΉβπ) = (πΉβ((β―βπΉ) β 1))) |
33 | 32 | breq2d 5160 |
. . . . . . 7
β’ (π = ((β―βπΉ) β 1) β ((πΉβ0) βΌ (πΉβπ) β (πΉβ0) βΌ (πΉβ((β―βπΉ) β 1)))) |
34 | 31, 33 | imbi12d 344 |
. . . . . 6
β’ (π = ((β―βπΉ) β 1) β ((π β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβπ)) β (((β―βπΉ) β 1) β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβ((β―βπΉ) β
1))))) |
35 | 34 | imbi2d 340 |
. . . . 5
β’ (π = ((β―βπΉ) β 1) β ((πΉ β dom π β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ))) β (πΉ β dom π β (((β―βπΉ) β 1) β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβ((β―βπΉ) β
1)))))) |
36 | 1, 2 | efger 19627 |
. . . . . . . 8
β’ βΌ Er
π |
37 | 36 | a1i 11 |
. . . . . . 7
β’ ((πΉ β dom π β§ 0 β (0..^(β―βπΉ))) β βΌ Er π) |
38 | | eldifi 4126 |
. . . . . . . . 9
β’ (πΉ β (Word π β {β
}) β πΉ β Word π) |
39 | | wrdf 14473 |
. . . . . . . . 9
β’ (πΉ β Word π β πΉ:(0..^(β―βπΉ))βΆπ) |
40 | 8, 38, 39 | 3syl 18 |
. . . . . . . 8
β’ (πΉ β dom π β πΉ:(0..^(β―βπΉ))βΆπ) |
41 | 40 | ffvelcdmda 7086 |
. . . . . . 7
β’ ((πΉ β dom π β§ 0 β (0..^(β―βπΉ))) β (πΉβ0) β π) |
42 | 37, 41 | erref 8725 |
. . . . . 6
β’ ((πΉ β dom π β§ 0 β (0..^(β―βπΉ))) β (πΉβ0) βΌ (πΉβ0)) |
43 | 42 | ex 413 |
. . . . 5
β’ (πΉ β dom π β (0 β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ0))) |
44 | | elnn0uz 12871 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
(β€β₯β0)) |
45 | | peano2fzor 13743 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β0) β§ (π + 1) β (0..^(β―βπΉ))) β π β (0..^(β―βπΉ))) |
46 | 44, 45 | sylanb 581 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π + 1) β
(0..^(β―βπΉ)))
β π β
(0..^(β―βπΉ))) |
47 | 46 | 3adant1 1130 |
. . . . . . . . . 10
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β π β
(0..^(β―βπΉ))) |
48 | 47 | 3expia 1121 |
. . . . . . . . 9
β’ ((πΉ β dom π β§ π β β0) β ((π + 1) β
(0..^(β―βπΉ))
β π β
(0..^(β―βπΉ)))) |
49 | 48 | imim1d 82 |
. . . . . . . 8
β’ ((πΉ β dom π β§ π β β0) β ((π β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβπ)) β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ)))) |
50 | 40 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β πΉ:(0..^(β―βπΉ))βΆπ) |
51 | 50, 47 | ffvelcdmd 7087 |
. . . . . . . . . . . 12
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (πΉβπ) β π) |
52 | | fvoveq1 7434 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (πΉβ(π β 1)) = (πΉβ((π + 1) β 1))) |
53 | 52 | fveq2d 6895 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβ(πΉβ(π β 1))) = (πβ(πΉβ((π + 1) β 1)))) |
54 | 53 | rneqd 5937 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ran (πβ(πΉβ(π β 1))) = ran (πβ(πΉβ((π + 1) β 1)))) |
55 | 27, 54 | eleq12d 2827 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((πΉβπ) β ran (πβ(πΉβ(π β 1))) β (πΉβ(π + 1)) β ran (πβ(πΉβ((π + 1) β 1))))) |
56 | 7 | simp3bi 1147 |
. . . . . . . . . . . . . . 15
β’ (πΉ β dom π β βπ β (1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1)))) |
57 | 56 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β βπ β
(1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1)))) |
58 | | nn0p1nn 12515 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π + 1) β
β) |
59 | 58 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (π + 1) β
β) |
60 | | nnuz 12869 |
. . . . . . . . . . . . . . . 16
β’ β =
(β€β₯β1) |
61 | 59, 60 | eleqtrdi 2843 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (π + 1) β
(β€β₯β1)) |
62 | | elfzolt2b 13647 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β
(0..^(β―βπΉ))
β (π + 1) β
((π +
1)..^(β―βπΉ))) |
63 | 62 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (π + 1) β
((π +
1)..^(β―βπΉ))) |
64 | | elfzo3 13653 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β
(1..^(β―βπΉ))
β ((π + 1) β
(β€β₯β1) β§ (π + 1) β ((π + 1)..^(β―βπΉ)))) |
65 | 61, 63, 64 | sylanbrc 583 |
. . . . . . . . . . . . . 14
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (π + 1) β
(1..^(β―βπΉ))) |
66 | 55, 57, 65 | rspcdva 3613 |
. . . . . . . . . . . . 13
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (πΉβ(π + 1)) β ran (πβ(πΉβ((π + 1) β 1)))) |
67 | | nn0cn 12486 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β π β
β) |
68 | 67 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β π β
β) |
69 | | ax-1cn 11170 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
70 | | pncan 11470 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
71 | 68, 69, 70 | sylancl 586 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β ((π + 1) β 1)
= π) |
72 | 71 | fveq2d 6895 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (πΉβ((π + 1) β 1)) = (πΉβπ)) |
73 | 72 | fveq2d 6895 |
. . . . . . . . . . . . . 14
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (πβ(πΉβ((π + 1) β 1))) = (πβ(πΉβπ))) |
74 | 73 | rneqd 5937 |
. . . . . . . . . . . . 13
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β ran (πβ(πΉβ((π + 1) β 1))) = ran (πβ(πΉβπ))) |
75 | 66, 74 | eleqtrd 2835 |
. . . . . . . . . . . 12
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (πΉβ(π + 1)) β ran (πβ(πΉβπ))) |
76 | 1, 2, 3, 4 | efgi2 19634 |
. . . . . . . . . . . 12
β’ (((πΉβπ) β π β§ (πΉβ(π + 1)) β ran (πβ(πΉβπ))) β (πΉβπ) βΌ (πΉβ(π + 1))) |
77 | 51, 75, 76 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (πΉβπ) βΌ (πΉβ(π + 1))) |
78 | 36 | a1i 11 |
. . . . . . . . . . . 12
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β βΌ Er π) |
79 | 78 | ertr 8720 |
. . . . . . . . . . 11
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β (((πΉβ0) βΌ (πΉβπ) β§ (πΉβπ) βΌ (πΉβ(π + 1))) β (πΉβ0) βΌ (πΉβ(π + 1)))) |
80 | 77, 79 | mpan2d 692 |
. . . . . . . . . 10
β’ ((πΉ β dom π β§ π β β0 β§ (π + 1) β
(0..^(β―βπΉ)))
β ((πΉβ0) βΌ (πΉβπ) β (πΉβ0) βΌ (πΉβ(π + 1)))) |
81 | 80 | 3expia 1121 |
. . . . . . . . 9
β’ ((πΉ β dom π β§ π β β0) β ((π + 1) β
(0..^(β―βπΉ))
β ((πΉβ0) βΌ (πΉβπ) β (πΉβ0) βΌ (πΉβ(π + 1))))) |
82 | 81 | a2d 29 |
. . . . . . . 8
β’ ((πΉ β dom π β§ π β β0) β (((π + 1) β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβπ)) β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ(π + 1))))) |
83 | 49, 82 | syld 47 |
. . . . . . 7
β’ ((πΉ β dom π β§ π β β0) β ((π β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβπ)) β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ(π + 1))))) |
84 | 83 | expcom 414 |
. . . . . 6
β’ (π β β0
β (πΉ β dom π β ((π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ)) β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ(π + 1)))))) |
85 | 84 | a2d 29 |
. . . . 5
β’ (π β β0
β ((πΉ β dom π β (π β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβπ))) β (πΉ β dom π β ((π + 1) β (0..^(β―βπΉ)) β (πΉβ0) βΌ (πΉβ(π + 1)))))) |
86 | 20, 25, 30, 35, 43, 85 | nn0ind 12661 |
. . . 4
β’
(((β―βπΉ)
β 1) β β0 β (πΉ β dom π β (((β―βπΉ) β 1) β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβ((β―βπΉ) β
1))))) |
87 | 15, 86 | mpcom 38 |
. . 3
β’ (πΉ β dom π β (((β―βπΉ) β 1) β
(0..^(β―βπΉ))
β (πΉβ0) βΌ (πΉβ((β―βπΉ) β 1)))) |
88 | 13, 87 | mpd 15 |
. 2
β’ (πΉ β dom π β (πΉβ0) βΌ (πΉβ((β―βπΉ) β 1))) |
89 | 1, 2, 3, 4, 5, 6 | efgsval 19640 |
. 2
β’ (πΉ β dom π β (πβπΉ) = (πΉβ((β―βπΉ) β 1))) |
90 | 88, 89 | breqtrrd 5176 |
1
β’ (πΉ β dom π β (πΉβ0) βΌ (πβπΉ)) |