Step | Hyp | Ref
| Expression |
1 | | ovex 7394 |
. . 3
β’
(0..^((β―βπ) β 1)) β V |
2 | | mptexg 7175 |
. . 3
β’
((0..^((β―βπ) β 1)) β V β (π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β V) |
3 | 1, 2 | mp1i 13 |
. 2
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β V) |
4 | | eqid 2733 |
. . . . 5
β’ (π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) |
5 | 4 | clwlkclwwlklem2a 28991 |
. . . 4
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β (((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ β§ π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ β§ βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))))) |
6 | 5 | adantr 482 |
. . 3
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β (((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ β§ π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ β§ βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))))) |
7 | | eleq1 2822 |
. . . . . . 7
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (π β Word dom πΈ β (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ)) |
8 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (β―βπ) = (β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))))) |
9 | 8 | oveq2d 7377 |
. . . . . . . 8
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β
(0...(β―βπ)) =
(0...(β―β(π₯
β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))) |
10 | 9 | feq2d 6658 |
. . . . . . 7
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (π:(0...(β―βπ))βΆπ β π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ)) |
11 | 8 | oveq2d 7377 |
. . . . . . . 8
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β
(0..^(β―βπ)) =
(0..^(β―β(π₯
β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))) |
12 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (πβπ) = ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) |
13 | 12 | fveqeq2d 6854 |
. . . . . . . 8
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β ((πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β (πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))})) |
14 | 11, 13 | raleqbidv 3318 |
. . . . . . 7
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (βπ β
(0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))})) |
15 | 7, 10, 14 | 3anbi123d 1437 |
. . . . . 6
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ β§ π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ β§ βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))}))) |
16 | | 2fveq3 6851 |
. . . . . . 7
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (πβ(β―βπ)) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))) |
17 | 16 | eqeq2d 2744 |
. . . . . 6
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β ((πβ0) = (πβ(β―βπ)) β (πβ0) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))))))) |
18 | 15, 17 | anbi12d 632 |
. . . . 5
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β (((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ β§ π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ β§ βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))))) |
19 | 18 | imbi2d 341 |
. . . 4
β’ (π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β ((((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β (((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ β§ π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ β§ βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))))))))) |
20 | 19 | adantl 483 |
. . 3
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))) β ((((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β (((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β Word dom πΈ β§ π:(0...(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))βΆπ β§ βπ β (0..^(β―β(π₯ β
(0..^((β―βπ)
β 1)) β¦ if(π₯
< ((β―βπ)
β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))))(πΈβ((π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))βπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―β(π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))))))))) |
21 | 6, 20 | mpbird 257 |
. 2
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ π = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)})))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
22 | 3, 21 | spcimedv 3556 |
1
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |