Step | Hyp | Ref
| Expression |
1 | | fveq1 6891 |
. . . . 5
β’ (π = πΉ β (πβ0) = (πΉβ0)) |
2 | 1 | eleq1d 2819 |
. . . 4
β’ (π = πΉ β ((πβ0) β π· β (πΉβ0) β π·)) |
3 | | fveq2 6892 |
. . . . . 6
β’ (π = πΉ β (β―βπ) = (β―βπΉ)) |
4 | 3 | oveq2d 7425 |
. . . . 5
β’ (π = πΉ β (1..^(β―βπ)) = (1..^(β―βπΉ))) |
5 | | fveq1 6891 |
. . . . . 6
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
6 | | fveq1 6891 |
. . . . . . . 8
β’ (π = πΉ β (πβ(π β 1)) = (πΉβ(π β 1))) |
7 | 6 | fveq2d 6896 |
. . . . . . 7
β’ (π = πΉ β (πβ(πβ(π β 1))) = (πβ(πΉβ(π β 1)))) |
8 | 7 | rneqd 5938 |
. . . . . 6
β’ (π = πΉ β ran (πβ(πβ(π β 1))) = ran (πβ(πΉβ(π β 1)))) |
9 | 5, 8 | eleq12d 2828 |
. . . . 5
β’ (π = πΉ β ((πβπ) β ran (πβ(πβ(π β 1))) β (πΉβπ) β ran (πβ(πΉβ(π β 1))))) |
10 | 4, 9 | raleqbidv 3343 |
. . . 4
β’ (π = πΉ β (βπ β (1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))) β βπ β
(1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1))))) |
11 | 2, 10 | anbi12d 632 |
. . 3
β’ (π = πΉ β (((πβ0) β π· β§ βπ β (1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1)))) β ((πΉβ0) β π· β§ βπ β (1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1)))))) |
12 | | efgval.w |
. . . . . 6
β’ π = ( I βWord (πΌ Γ
2o)) |
13 | | efgval.r |
. . . . . 6
β’ βΌ = (
~FG βπΌ) |
14 | | efgval2.m |
. . . . . 6
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
15 | | efgval2.t |
. . . . . 6
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
16 | | efgred.d |
. . . . . 6
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
17 | | efgred.s |
. . . . . 6
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
18 | 12, 13, 14, 15, 16, 17 | efgsf 19597 |
. . . . 5
β’ π:{π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))}βΆπ |
19 | 18 | fdmi 6730 |
. . . 4
β’ dom π = {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} |
20 | | fveq1 6891 |
. . . . . . 7
β’ (π‘ = π β (π‘β0) = (πβ0)) |
21 | 20 | eleq1d 2819 |
. . . . . 6
β’ (π‘ = π β ((π‘β0) β π· β (πβ0) β π·)) |
22 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π β (π‘βπ) = (π‘βπ)) |
23 | | fvoveq1 7432 |
. . . . . . . . . . 11
β’ (π = π β (π‘β(π β 1)) = (π‘β(π β 1))) |
24 | 23 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π = π β (πβ(π‘β(π β 1))) = (πβ(π‘β(π β 1)))) |
25 | 24 | rneqd 5938 |
. . . . . . . . 9
β’ (π = π β ran (πβ(π‘β(π β 1))) = ran (πβ(π‘β(π β 1)))) |
26 | 22, 25 | eleq12d 2828 |
. . . . . . . 8
β’ (π = π β ((π‘βπ) β ran (πβ(π‘β(π β 1))) β (π‘βπ) β ran (πβ(π‘β(π β 1))))) |
27 | 26 | cbvralvw 3235 |
. . . . . . 7
β’
(βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))) β βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1)))) |
28 | | fveq2 6892 |
. . . . . . . . 9
β’ (π‘ = π β (β―βπ‘) = (β―βπ)) |
29 | 28 | oveq2d 7425 |
. . . . . . . 8
β’ (π‘ = π β (1..^(β―βπ‘)) = (1..^(β―βπ))) |
30 | | fveq1 6891 |
. . . . . . . . 9
β’ (π‘ = π β (π‘βπ) = (πβπ)) |
31 | | fveq1 6891 |
. . . . . . . . . . 11
β’ (π‘ = π β (π‘β(π β 1)) = (πβ(π β 1))) |
32 | 31 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π‘ = π β (πβ(π‘β(π β 1))) = (πβ(πβ(π β 1)))) |
33 | 32 | rneqd 5938 |
. . . . . . . . 9
β’ (π‘ = π β ran (πβ(π‘β(π β 1))) = ran (πβ(πβ(π β 1)))) |
34 | 30, 33 | eleq12d 2828 |
. . . . . . . 8
β’ (π‘ = π β ((π‘βπ) β ran (πβ(π‘β(π β 1))) β (πβπ) β ran (πβ(πβ(π β 1))))) |
35 | 29, 34 | raleqbidv 3343 |
. . . . . . 7
β’ (π‘ = π β (βπ β (1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))) β βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))) |
36 | 27, 35 | bitrid 283 |
. . . . . 6
β’ (π‘ = π β (βπ β (1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))) β βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))) |
37 | 21, 36 | anbi12d 632 |
. . . . 5
β’ (π‘ = π β (((π‘β0) β π· β§ βπ β (1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1)))) β ((πβ0) β π· β§ βπ β (1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1)))))) |
38 | 37 | cbvrabv 3443 |
. . . 4
β’ {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} = {π β (Word π β {β
}) β£ ((πβ0) β π· β§ βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))} |
39 | 19, 38 | eqtri 2761 |
. . 3
β’ dom π = {π β (Word π β {β
}) β£ ((πβ0) β π· β§ βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))} |
40 | 11, 39 | elrab2 3687 |
. 2
β’ (πΉ β dom π β (πΉ β (Word π β {β
}) β§ ((πΉβ0) β π· β§ βπ β
(1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1)))))) |
41 | | 3anass 1096 |
. 2
β’ ((πΉ β (Word π β {β
}) β§ (πΉβ0) β π· β§ βπ β (1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1)))) β (πΉ β (Word π β {β
}) β§ ((πΉβ0) β π· β§ βπ β
(1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1)))))) |
42 | 40, 41 | bitr4i 278 |
1
β’ (πΉ β dom π β (πΉ β (Word π β {β
}) β§ (πΉβ0) β π· β§ βπ β (1..^(β―βπΉ))(πΉβπ) β ran (πβ(πΉβ(π β 1))))) |