Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | fviss 6922 |
. . . . . . . . . 10
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
3 | 1, 2 | eqsstri 3982 |
. . . . . . . . 9
β’ π β Word (πΌ Γ 2o) |
4 | | efgredlem.2 |
. . . . . . . . . . . . 13
β’ (π β π΄ β dom π) |
5 | | efgval.r |
. . . . . . . . . . . . . . 15
β’ βΌ = (
~FG βπΌ) |
6 | | efgval2.m |
. . . . . . . . . . . . . . 15
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
7 | | efgval2.t |
. . . . . . . . . . . . . . 15
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
8 | | efgred.d |
. . . . . . . . . . . . . . 15
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
9 | | efgred.s |
. . . . . . . . . . . . . . 15
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
10 | 1, 5, 6, 7, 8, 9 | efgsdm 19520 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom π β (π΄ β (Word π β {β
}) β§ (π΄β0) β π· β§ βπ β (1..^(β―βπ΄))(π΄βπ) β ran (πβ(π΄β(π β 1))))) |
11 | 10 | simp1bi 1146 |
. . . . . . . . . . . . 13
β’ (π΄ β dom π β π΄ β (Word π β {β
})) |
12 | 4, 11 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π΄ β (Word π β {β
})) |
13 | 12 | eldifad 3926 |
. . . . . . . . . . 11
β’ (π β π΄ β Word π) |
14 | | wrdf 14416 |
. . . . . . . . . . 11
β’ (π΄ β Word π β π΄:(0..^(β―βπ΄))βΆπ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
β’ (π β π΄:(0..^(β―βπ΄))βΆπ) |
16 | | efgredlem.1 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β dom πβπ β dom π((β―β(πβπ)) < (β―β(πβπ΄)) β ((πβπ) = (πβπ) β (πβ0) = (πβ0)))) |
17 | | efgredlem.3 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β dom π) |
18 | | efgredlem.4 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ΄) = (πβπ΅)) |
19 | | efgredlem.5 |
. . . . . . . . . . . . . . 15
β’ (π β Β¬ (π΄β0) = (π΅β0)) |
20 | 1, 5, 6, 7, 8, 9, 16, 4, 17, 18, 19 | efgredlema 19530 |
. . . . . . . . . . . . . 14
β’ (π β (((β―βπ΄) β 1) β β
β§ ((β―βπ΅)
β 1) β β)) |
21 | 20 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β ((β―βπ΄) β 1) β
β) |
22 | | nnm1nn0 12462 |
. . . . . . . . . . . . 13
β’
(((β―βπ΄)
β 1) β β β (((β―βπ΄) β 1) β 1) β
β0) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (((β―βπ΄) β 1) β 1) β
β0) |
24 | 21 | nnred 12176 |
. . . . . . . . . . . . 13
β’ (π β ((β―βπ΄) β 1) β
β) |
25 | 24 | lem1d 12096 |
. . . . . . . . . . . 12
β’ (π β (((β―βπ΄) β 1) β 1) β€
((β―βπ΄) β
1)) |
26 | | eldifsni 4754 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (Word π β {β
}) β π΄ β β
) |
27 | 4, 11, 26 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β β
) |
28 | | wrdfin 14429 |
. . . . . . . . . . . . . . 15
β’ (π΄ β Word π β π΄ β Fin) |
29 | | hashnncl 14275 |
. . . . . . . . . . . . . . 15
β’ (π΄ β Fin β
((β―βπ΄) β
β β π΄ β
β
)) |
30 | 13, 28, 29 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β ((β―βπ΄) β β β π΄ β β
)) |
31 | 27, 30 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β (β―βπ΄) β
β) |
32 | | nnm1nn0 12462 |
. . . . . . . . . . . . 13
β’
((β―βπ΄)
β β β ((β―βπ΄) β 1) β
β0) |
33 | | fznn0 13542 |
. . . . . . . . . . . . 13
β’
(((β―βπ΄)
β 1) β β0 β ((((β―βπ΄) β 1) β 1) β
(0...((β―βπ΄)
β 1)) β ((((β―βπ΄) β 1) β 1) β
β0 β§ (((β―βπ΄) β 1) β 1) β€
((β―βπ΄) β
1)))) |
34 | 31, 32, 33 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β ((((β―βπ΄) β 1) β 1) β
(0...((β―βπ΄)
β 1)) β ((((β―βπ΄) β 1) β 1) β
β0 β§ (((β―βπ΄) β 1) β 1) β€
((β―βπ΄) β
1)))) |
35 | 23, 25, 34 | mpbir2and 712 |
. . . . . . . . . . 11
β’ (π β (((β―βπ΄) β 1) β 1) β
(0...((β―βπ΄)
β 1))) |
36 | | lencl 14430 |
. . . . . . . . . . . . . 14
β’ (π΄ β Word π β (β―βπ΄) β
β0) |
37 | 13, 36 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β―βπ΄) β
β0) |
38 | 37 | nn0zd 12533 |
. . . . . . . . . . . 12
β’ (π β (β―βπ΄) β
β€) |
39 | | fzoval 13582 |
. . . . . . . . . . . 12
β’
((β―βπ΄)
β β€ β (0..^(β―βπ΄)) = (0...((β―βπ΄) β 1))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
β’ (π β (0..^(β―βπ΄)) = (0...((β―βπ΄) β 1))) |
41 | 35, 40 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (π β (((β―βπ΄) β 1) β 1) β
(0..^(β―βπ΄))) |
42 | 15, 41 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (π΄β(((β―βπ΄) β 1) β 1)) β π) |
43 | 3, 42 | sselid 3946 |
. . . . . . . 8
β’ (π β (π΄β(((β―βπ΄) β 1) β 1)) β Word (πΌ Γ
2o)) |
44 | | lencl 14430 |
. . . . . . . 8
β’ ((π΄β(((β―βπ΄) β 1) β 1)) β
Word (πΌ Γ
2o) β (β―β(π΄β(((β―βπ΄) β 1) β 1))) β
β0) |
45 | 43, 44 | syl 17 |
. . . . . . 7
β’ (π β (β―β(π΄β(((β―βπ΄) β 1) β 1))) β
β0) |
46 | 45 | nn0red 12482 |
. . . . . 6
β’ (π β (β―β(π΄β(((β―βπ΄) β 1) β 1))) β
β) |
47 | | 2rp 12928 |
. . . . . 6
β’ 2 β
β+ |
48 | | ltaddrp 12960 |
. . . . . 6
β’
(((β―β(π΄β(((β―βπ΄) β 1) β 1))) β β
β§ 2 β β+) β (β―β(π΄β(((β―βπ΄) β 1) β 1))) <
((β―β(π΄β(((β―βπ΄) β 1) β 1))) +
2)) |
49 | 46, 47, 48 | sylancl 587 |
. . . . 5
β’ (π β (β―β(π΄β(((β―βπ΄) β 1) β 1))) <
((β―β(π΄β(((β―βπ΄) β 1) β 1))) +
2)) |
50 | 37 | nn0red 12482 |
. . . . . . . . . . 11
β’ (π β (β―βπ΄) β
β) |
51 | 50 | lem1d 12096 |
. . . . . . . . . 10
β’ (π β ((β―βπ΄) β 1) β€
(β―βπ΄)) |
52 | | fznn 13518 |
. . . . . . . . . . 11
β’
((β―βπ΄)
β β€ β (((β―βπ΄) β 1) β
(1...(β―βπ΄))
β (((β―βπ΄)
β 1) β β β§ ((β―βπ΄) β 1) β€ (β―βπ΄)))) |
53 | 38, 52 | syl 17 |
. . . . . . . . . 10
β’ (π β (((β―βπ΄) β 1) β
(1...(β―βπ΄))
β (((β―βπ΄)
β 1) β β β§ ((β―βπ΄) β 1) β€ (β―βπ΄)))) |
54 | 21, 51, 53 | mpbir2and 712 |
. . . . . . . . 9
β’ (π β ((β―βπ΄) β 1) β
(1...(β―βπ΄))) |
55 | 1, 5, 6, 7, 8, 9 | efgsres 19528 |
. . . . . . . . 9
β’ ((π΄ β dom π β§ ((β―βπ΄) β 1) β
(1...(β―βπ΄)))
β (π΄ βΎ
(0..^((β―βπ΄)
β 1))) β dom π) |
56 | 4, 54, 55 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄ βΎ (0..^((β―βπ΄) β 1))) β dom π) |
57 | 1, 5, 6, 7, 8, 9 | efgsval 19521 |
. . . . . . . 8
β’ ((π΄ βΎ
(0..^((β―βπ΄)
β 1))) β dom π
β (πβ(π΄ βΎ
(0..^((β―βπ΄)
β 1)))) = ((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β((β―β(π΄ βΎ (0..^((β―βπ΄) β 1)))) β
1))) |
58 | 56, 57 | syl 17 |
. . . . . . 7
β’ (π β (πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = ((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β((β―β(π΄ βΎ (0..^((β―βπ΄) β 1)))) β
1))) |
59 | | fz1ssfz0 13546 |
. . . . . . . . . . . 12
β’
(1...(β―βπ΄)) β (0...(β―βπ΄)) |
60 | 59, 54 | sselid 3946 |
. . . . . . . . . . 11
β’ (π β ((β―βπ΄) β 1) β
(0...(β―βπ΄))) |
61 | | pfxres 14576 |
. . . . . . . . . . 11
β’ ((π΄ β Word π β§ ((β―βπ΄) β 1) β
(0...(β―βπ΄)))
β (π΄ prefix
((β―βπ΄) β
1)) = (π΄ βΎ
(0..^((β―βπ΄)
β 1)))) |
62 | 13, 60, 61 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π΄ prefix ((β―βπ΄) β 1)) = (π΄ βΎ (0..^((β―βπ΄) β 1)))) |
63 | 62 | fveq2d 6850 |
. . . . . . . . 9
β’ (π β (β―β(π΄ prefix ((β―βπ΄) β 1))) =
(β―β(π΄ βΎ
(0..^((β―βπ΄)
β 1))))) |
64 | | pfxlen 14580 |
. . . . . . . . . 10
β’ ((π΄ β Word π β§ ((β―βπ΄) β 1) β
(0...(β―βπ΄)))
β (β―β(π΄
prefix ((β―βπ΄)
β 1))) = ((β―βπ΄) β 1)) |
65 | 13, 60, 64 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (β―β(π΄ prefix ((β―βπ΄) β 1))) =
((β―βπ΄) β
1)) |
66 | 63, 65 | eqtr3d 2775 |
. . . . . . . 8
β’ (π β (β―β(π΄ βΎ
(0..^((β―βπ΄)
β 1)))) = ((β―βπ΄) β 1)) |
67 | 66 | fvoveq1d 7383 |
. . . . . . 7
β’ (π β ((π΄ βΎ (0..^((β―βπ΄) β
1)))β((β―β(π΄ βΎ (0..^((β―βπ΄) β 1)))) β 1)) =
((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β(((β―βπ΄) β 1) β 1))) |
68 | | fzo0end 13673 |
. . . . . . . 8
β’
(((β―βπ΄)
β 1) β β β (((β―βπ΄) β 1) β 1) β
(0..^((β―βπ΄)
β 1))) |
69 | | fvres 6865 |
. . . . . . . 8
β’
((((β―βπ΄)
β 1) β 1) β (0..^((β―βπ΄) β 1)) β ((π΄ βΎ (0..^((β―βπ΄) β
1)))β(((β―βπ΄) β 1) β 1)) = (π΄β(((β―βπ΄) β 1) β
1))) |
70 | 21, 68, 69 | 3syl 18 |
. . . . . . 7
β’ (π β ((π΄ βΎ (0..^((β―βπ΄) β
1)))β(((β―βπ΄) β 1) β 1)) = (π΄β(((β―βπ΄) β 1) β
1))) |
71 | 58, 67, 70 | 3eqtrd 2777 |
. . . . . 6
β’ (π β (πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (π΄β(((β―βπ΄) β 1) β
1))) |
72 | 71 | fveq2d 6850 |
. . . . 5
β’ (π β (β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) =
(β―β(π΄β(((β―βπ΄) β 1) β 1)))) |
73 | 1, 5, 6, 7, 8, 9 | efgsdmi 19522 |
. . . . . . 7
β’ ((π΄ β dom π β§ ((β―βπ΄) β 1) β β) β (πβπ΄) β ran (πβ(π΄β(((β―βπ΄) β 1) β 1)))) |
74 | 4, 21, 73 | syl2anc 585 |
. . . . . 6
β’ (π β (πβπ΄) β ran (πβ(π΄β(((β―βπ΄) β 1) β 1)))) |
75 | 1, 5, 6, 7 | efgtlen 19516 |
. . . . . 6
β’ (((π΄β(((β―βπ΄) β 1) β 1)) β
π β§ (πβπ΄) β ran (πβ(π΄β(((β―βπ΄) β 1) β 1)))) β
(β―β(πβπ΄)) = ((β―β(π΄β(((β―βπ΄) β 1) β 1))) +
2)) |
76 | 42, 74, 75 | syl2anc 585 |
. . . . 5
β’ (π β (β―β(πβπ΄)) = ((β―β(π΄β(((β―βπ΄) β 1) β 1))) +
2)) |
77 | 49, 72, 76 | 3brtr4d 5141 |
. . . 4
β’ (π β (β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄))) |
78 | 1, 5, 6, 7 | efgtf 19512 |
. . . . . . . . . . . 12
β’ ((π΄β(((β―βπ΄) β 1) β 1)) β
π β ((πβ(π΄β(((β―βπ΄) β 1) β 1))) = (π β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))), π β (πΌ Γ 2o) β¦ ((π΄β(((β―βπ΄) β 1) β 1)) splice
β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ(π΄β(((β―βπ΄) β 1) β
1))):((0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ)) |
79 | 42, 78 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((πβ(π΄β(((β―βπ΄) β 1) β 1))) = (π β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))), π β (πΌ Γ 2o) β¦ ((π΄β(((β―βπ΄) β 1) β 1)) splice
β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ(π΄β(((β―βπ΄) β 1) β
1))):((0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ)) |
80 | 79 | simprd 497 |
. . . . . . . . . 10
β’ (π β (πβ(π΄β(((β―βπ΄) β 1) β
1))):((0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ) |
81 | | ffn 6672 |
. . . . . . . . . 10
β’ ((πβ(π΄β(((β―βπ΄) β 1) β
1))):((0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ
β (πβ(π΄β(((β―βπ΄) β 1) β 1))) Fn
((0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) Γ (πΌ Γ
2o))) |
82 | | ovelrn 7534 |
. . . . . . . . . 10
β’ ((πβ(π΄β(((β―βπ΄) β 1) β 1))) Fn
((0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) Γ (πΌ Γ 2o)) β
((πβπ΄) β ran (πβ(π΄β(((β―βπ΄) β 1) β 1))) β
βπ β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1))))βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π))) |
83 | 80, 81, 82 | 3syl 18 |
. . . . . . . . 9
β’ (π β ((πβπ΄) β ran (πβ(π΄β(((β―βπ΄) β 1) β 1))) β
βπ β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1))))βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π))) |
84 | 74, 83 | mpbid 231 |
. . . . . . . 8
β’ (π β βπ β (0...(β―β(π΄β(((β―βπ΄) β 1) β
1))))βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π)) |
85 | 20 | simprd 497 |
. . . . . . . . . 10
β’ (π β ((β―βπ΅) β 1) β
β) |
86 | 1, 5, 6, 7, 8, 9 | efgsdmi 19522 |
. . . . . . . . . 10
β’ ((π΅ β dom π β§ ((β―βπ΅) β 1) β β) β (πβπ΅) β ran (πβ(π΅β(((β―βπ΅) β 1) β 1)))) |
87 | 17, 85, 86 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβπ΅) β ran (πβ(π΅β(((β―βπ΅) β 1) β 1)))) |
88 | 1, 5, 6, 7, 8, 9 | efgsdm 19520 |
. . . . . . . . . . . . . . . . 17
β’ (π΅ β dom π β (π΅ β (Word π β {β
}) β§ (π΅β0) β π· β§ βπ β (1..^(β―βπ΅))(π΅βπ) β ran (πβ(π΅β(π β 1))))) |
89 | 88 | simp1bi 1146 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β dom π β π΅ β (Word π β {β
})) |
90 | 17, 89 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β (Word π β {β
})) |
91 | 90 | eldifad 3926 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β Word π) |
92 | | wrdf 14416 |
. . . . . . . . . . . . . 14
β’ (π΅ β Word π β π΅:(0..^(β―βπ΅))βΆπ) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΅:(0..^(β―βπ΅))βΆπ) |
94 | | fzo0end 13673 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ΅)
β 1) β β β (((β―βπ΅) β 1) β 1) β
(0..^((β―βπ΅)
β 1))) |
95 | | elfzofz 13597 |
. . . . . . . . . . . . . . 15
β’
((((β―βπ΅)
β 1) β 1) β (0..^((β―βπ΅) β 1)) β (((β―βπ΅) β 1) β 1) β
(0...((β―βπ΅)
β 1))) |
96 | 85, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (((β―βπ΅) β 1) β 1) β
(0...((β―βπ΅)
β 1))) |
97 | | lencl 14430 |
. . . . . . . . . . . . . . . . 17
β’ (π΅ β Word π β (β―βπ΅) β
β0) |
98 | 91, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―βπ΅) β
β0) |
99 | 98 | nn0zd 12533 |
. . . . . . . . . . . . . . 15
β’ (π β (β―βπ΅) β
β€) |
100 | | fzoval 13582 |
. . . . . . . . . . . . . . 15
β’
((β―βπ΅)
β β€ β (0..^(β―βπ΅)) = (0...((β―βπ΅) β 1))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (0..^(β―βπ΅)) = (0...((β―βπ΅) β 1))) |
102 | 96, 101 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ (π β (((β―βπ΅) β 1) β 1) β
(0..^(β―βπ΅))) |
103 | 93, 102 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ (π β (π΅β(((β―βπ΅) β 1) β 1)) β π) |
104 | 1, 5, 6, 7 | efgtf 19512 |
. . . . . . . . . . . 12
β’ ((π΅β(((β―βπ΅) β 1) β 1)) β
π β ((πβ(π΅β(((β―βπ΅) β 1) β 1))) = (π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))), π β (πΌ Γ 2o) β¦ ((π΅β(((β―βπ΅) β 1) β 1)) splice
β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ(π΅β(((β―βπ΅) β 1) β
1))):((0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((πβ(π΅β(((β―βπ΅) β 1) β 1))) = (π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))), π β (πΌ Γ 2o) β¦ ((π΅β(((β―βπ΅) β 1) β 1)) splice
β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ(π΅β(((β―βπ΅) β 1) β
1))):((0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ)) |
106 | 105 | simprd 497 |
. . . . . . . . . 10
β’ (π β (πβ(π΅β(((β―βπ΅) β 1) β
1))):((0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ) |
107 | | ffn 6672 |
. . . . . . . . . 10
β’ ((πβ(π΅β(((β―βπ΅) β 1) β
1))):((0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))) Γ (πΌ Γ
2o))βΆπ
β (πβ(π΅β(((β―βπ΅) β 1) β 1))) Fn
((0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))) Γ (πΌ Γ
2o))) |
108 | | ovelrn 7534 |
. . . . . . . . . 10
β’ ((πβ(π΅β(((β―βπ΅) β 1) β 1))) Fn
((0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))) Γ (πΌ Γ 2o)) β
((πβπ΅) β ran (πβ(π΅β(((β―βπ΅) β 1) β 1))) β
βπ β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1))))βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π ))) |
109 | 106, 107,
108 | 3syl 18 |
. . . . . . . . 9
β’ (π β ((πβπ΅) β ran (πβ(π΅β(((β―βπ΅) β 1) β 1))) β
βπ β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1))))βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π ))) |
110 | 87, 109 | mpbid 231 |
. . . . . . . 8
β’ (π β βπ β (0...(β―β(π΅β(((β―βπ΅) β 1) β
1))))βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) |
111 | | reeanv 3216 |
. . . . . . . . 9
β’
(βπ β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1))))βπ β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1))))(βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (βπ β (0...(β―β(π΄β(((β―βπ΄) β 1) β
1))))βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ βπ β (0...(β―β(π΅β(((β―βπ΅) β 1) β
1))))βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π ))) |
112 | | reeanv 3216 |
. . . . . . . . . . 11
β’
(βπ β
(πΌ Γ
2o)βπ
β (πΌ Γ
2o)((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π ))) |
113 | 16 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
βπ β dom πβπ β dom π((β―β(πβπ)) < (β―β(πβπ΄)) β ((πβπ) = (πβπ) β (πβ0) = (πβ0)))) |
114 | 4 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
π΄ β dom π) |
115 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
π΅ β dom π) |
116 | 18 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
(πβπ΄) = (πβπ΅)) |
117 | 19 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
Β¬ (π΄β0) = (π΅β0)) |
118 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ΄)
β 1) β 1) = (((β―βπ΄) β 1) β 1) |
119 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ΅)
β 1) β 1) = (((β―βπ΅) β 1) β 1) |
120 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
(π β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§ π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β
1)))))) |
121 | 120 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
π β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1))))) |
122 | 120 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1))))) |
123 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
(π β (πΌ Γ 2o) β§
π β (πΌ Γ 2o))) |
124 | 123 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
π β (πΌ Γ 2o)) |
125 | 123 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
π β (πΌ Γ 2o)) |
126 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π ))) |
127 | 126 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π)) |
128 | 126 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) |
129 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1))) |
130 | 1, 5, 6, 7, 8, 9, 113, 114, 115, 116, 117, 118, 119, 121, 122, 124, 125, 127, 128, 129 | efgredlemb 19536 |
. . . . . . . . . . . . . 14
β’ Β¬
(((π β§ (π β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§ π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1))) |
131 | | iman 403 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β 1))) β
Β¬ (((π β§ (π β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§ π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β§ Β¬ (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1)))) |
132 | 130, 131 | mpbir 230 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ ((π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β§ ((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )))) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1))) |
133 | 132 | expr 458 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β§ (π β (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1)))) |
134 | 133 | rexlimdvva 3202 |
. . . . . . . . . . 11
β’ ((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β
(βπ β (πΌ Γ
2o)βπ
β (πΌ Γ
2o)((πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ (πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1)))) |
135 | 112, 134 | biimtrrid 242 |
. . . . . . . . . 10
β’ ((π β§ (π β (0...(β―β(π΄β(((β―βπ΄) β 1) β 1)))) β§
π β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1)))))) β
((βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1)))) |
136 | 135 | rexlimdvva 3202 |
. . . . . . . . 9
β’ (π β (βπ β (0...(β―β(π΄β(((β―βπ΄) β 1) β
1))))βπ β
(0...(β―β(π΅β(((β―βπ΅) β 1) β 1))))(βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1)))) |
137 | 111, 136 | biimtrrid 242 |
. . . . . . . 8
β’ (π β ((βπ β
(0...(β―β(π΄β(((β―βπ΄) β 1) β 1))))βπ β (πΌ Γ 2o)(πβπ΄) = (π(πβ(π΄β(((β―βπ΄) β 1) β 1)))π) β§ βπ β (0...(β―β(π΅β(((β―βπ΅) β 1) β
1))))βπ β (πΌ Γ 2o)(πβπ΅) = (π(πβ(π΅β(((β―βπ΅) β 1) β 1)))π )) β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1)))) |
138 | 84, 110, 137 | mp2and 698 |
. . . . . . 7
β’ (π β (π΄β(((β―βπ΄) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1))) |
139 | | fvres 6865 |
. . . . . . . 8
β’
((((β―βπ΅)
β 1) β 1) β (0..^((β―βπ΅) β 1)) β ((π΅ βΎ (0..^((β―βπ΅) β
1)))β(((β―βπ΅) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1))) |
140 | 85, 94, 139 | 3syl 18 |
. . . . . . 7
β’ (π β ((π΅ βΎ (0..^((β―βπ΅) β
1)))β(((β―βπ΅) β 1) β 1)) = (π΅β(((β―βπ΅) β 1) β
1))) |
141 | 138, 70, 140 | 3eqtr4d 2783 |
. . . . . 6
β’ (π β ((π΄ βΎ (0..^((β―βπ΄) β
1)))β(((β―βπ΄) β 1) β 1)) = ((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β(((β―βπ΅) β 1) β 1))) |
142 | | fz1ssfz0 13546 |
. . . . . . . . . . 11
β’
(1...(β―βπ΅)) β (0...(β―βπ΅)) |
143 | 98 | nn0red 12482 |
. . . . . . . . . . . . 13
β’ (π β (β―βπ΅) β
β) |
144 | 143 | lem1d 12096 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ΅) β 1) β€
(β―βπ΅)) |
145 | | fznn 13518 |
. . . . . . . . . . . . 13
β’
((β―βπ΅)
β β€ β (((β―βπ΅) β 1) β
(1...(β―βπ΅))
β (((β―βπ΅)
β 1) β β β§ ((β―βπ΅) β 1) β€ (β―βπ΅)))) |
146 | 99, 145 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (((β―βπ΅) β 1) β
(1...(β―βπ΅))
β (((β―βπ΅)
β 1) β β β§ ((β―βπ΅) β 1) β€ (β―βπ΅)))) |
147 | 85, 144, 146 | mpbir2and 712 |
. . . . . . . . . . 11
β’ (π β ((β―βπ΅) β 1) β
(1...(β―βπ΅))) |
148 | 142, 147 | sselid 3946 |
. . . . . . . . . 10
β’ (π β ((β―βπ΅) β 1) β
(0...(β―βπ΅))) |
149 | | pfxres 14576 |
. . . . . . . . . 10
β’ ((π΅ β Word π β§ ((β―βπ΅) β 1) β
(0...(β―βπ΅)))
β (π΅ prefix
((β―βπ΅) β
1)) = (π΅ βΎ
(0..^((β―βπ΅)
β 1)))) |
150 | 91, 148, 149 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π΅ prefix ((β―βπ΅) β 1)) = (π΅ βΎ (0..^((β―βπ΅) β 1)))) |
151 | 150 | fveq2d 6850 |
. . . . . . . 8
β’ (π β (β―β(π΅ prefix ((β―βπ΅) β 1))) =
(β―β(π΅ βΎ
(0..^((β―βπ΅)
β 1))))) |
152 | | pfxlen 14580 |
. . . . . . . . 9
β’ ((π΅ β Word π β§ ((β―βπ΅) β 1) β
(0...(β―βπ΅)))
β (β―β(π΅
prefix ((β―βπ΅)
β 1))) = ((β―βπ΅) β 1)) |
153 | 91, 148, 152 | syl2anc 585 |
. . . . . . . 8
β’ (π β (β―β(π΅ prefix ((β―βπ΅) β 1))) =
((β―βπ΅) β
1)) |
154 | 151, 153 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (β―β(π΅ βΎ
(0..^((β―βπ΅)
β 1)))) = ((β―βπ΅) β 1)) |
155 | 154 | fvoveq1d 7383 |
. . . . . 6
β’ (π β ((π΅ βΎ (0..^((β―βπ΅) β
1)))β((β―β(π΅ βΎ (0..^((β―βπ΅) β 1)))) β 1)) =
((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β(((β―βπ΅) β 1) β 1))) |
156 | 141, 67, 155 | 3eqtr4d 2783 |
. . . . 5
β’ (π β ((π΄ βΎ (0..^((β―βπ΄) β
1)))β((β―β(π΄ βΎ (0..^((β―βπ΄) β 1)))) β 1)) =
((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β((β―β(π΅ βΎ (0..^((β―βπ΅) β 1)))) β
1))) |
157 | 1, 5, 6, 7, 8, 9 | efgsres 19528 |
. . . . . . 7
β’ ((π΅ β dom π β§ ((β―βπ΅) β 1) β
(1...(β―βπ΅)))
β (π΅ βΎ
(0..^((β―βπ΅)
β 1))) β dom π) |
158 | 17, 147, 157 | syl2anc 585 |
. . . . . 6
β’ (π β (π΅ βΎ (0..^((β―βπ΅) β 1))) β dom π) |
159 | 1, 5, 6, 7, 8, 9 | efgsval 19521 |
. . . . . 6
β’ ((π΅ βΎ
(0..^((β―βπ΅)
β 1))) β dom π
β (πβ(π΅ βΎ
(0..^((β―βπ΅)
β 1)))) = ((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β((β―β(π΅ βΎ (0..^((β―βπ΅) β 1)))) β
1))) |
160 | 158, 159 | syl 17 |
. . . . 5
β’ (π β (πβ(π΅ βΎ (0..^((β―βπ΅) β 1)))) = ((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β((β―β(π΅ βΎ (0..^((β―βπ΅) β 1)))) β
1))) |
161 | 156, 58, 160 | 3eqtr4d 2783 |
. . . 4
β’ (π β (πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβ(π΅ βΎ (0..^((β―βπ΅) β
1))))) |
162 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β (πβπ) = (πβ(π΄ βΎ (0..^((β―βπ΄) β
1))))) |
163 | 162 | fveq2d 6850 |
. . . . . . . 8
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β
(β―β(πβπ)) = (β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β
1)))))) |
164 | 163 | breq1d 5119 |
. . . . . . 7
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β
((β―β(πβπ)) < (β―β(πβπ΄)) β (β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄)))) |
165 | 162 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β ((πβπ) = (πβπ) β (πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβπ))) |
166 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β (πβ0) = ((π΄ βΎ (0..^((β―βπ΄) β
1)))β0)) |
167 | 166 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β ((πβ0) = (πβ0) β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) = (πβ0))) |
168 | 165, 167 | imbi12d 345 |
. . . . . . 7
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β (((πβπ) = (πβπ) β (πβ0) = (πβ0)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβπ) β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) = (πβ0)))) |
169 | 164, 168 | imbi12d 345 |
. . . . . 6
β’ (π = (π΄ βΎ (0..^((β―βπ΄) β 1))) β
(((β―β(πβπ)) < (β―β(πβπ΄)) β ((πβπ) = (πβπ) β (πβ0) = (πβ0))) β ((β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβπ) β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) = (πβ0))))) |
170 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = (π΅ βΎ (0..^((β―βπ΅) β 1))) β (πβπ) = (πβ(π΅ βΎ (0..^((β―βπ΅) β
1))))) |
171 | 170 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = (π΅ βΎ (0..^((β―βπ΅) β 1))) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβπ) β (πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβ(π΅ βΎ (0..^((β―βπ΅) β
1)))))) |
172 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = (π΅ βΎ (0..^((β―βπ΅) β 1))) β (πβ0) = ((π΅ βΎ (0..^((β―βπ΅) β
1)))β0)) |
173 | 172 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = (π΅ βΎ (0..^((β―βπ΅) β 1))) β (((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β0) = (πβ0) β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) =
((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β0))) |
174 | 171, 173 | imbi12d 345 |
. . . . . . 7
β’ (π = (π΅ βΎ (0..^((β―βπ΅) β 1))) β (((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβπ) β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) = (πβ0)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβ(π΅ βΎ (0..^((β―βπ΅) β 1)))) β ((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β0) = ((π΅
βΎ (0..^((β―βπ΅) β 1)))β0)))) |
175 | 174 | imbi2d 341 |
. . . . . 6
β’ (π = (π΅ βΎ (0..^((β―βπ΅) β 1))) β
(((β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβπ) β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) = (πβ0))) β
((β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβ(π΅ βΎ (0..^((β―βπ΅) β 1)))) β ((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β0) = ((π΅
βΎ (0..^((β―βπ΅) β 1)))β0))))) |
176 | 169, 175 | rspc2va 3593 |
. . . . 5
β’ ((((π΄ βΎ
(0..^((β―βπ΄)
β 1))) β dom π
β§ (π΅ βΎ
(0..^((β―βπ΅)
β 1))) β dom π)
β§ βπ β dom
πβπ β dom π((β―β(πβπ)) < (β―β(πβπ΄)) β ((πβπ) = (πβπ) β (πβ0) = (πβ0)))) β ((β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβ(π΅ βΎ (0..^((β―βπ΅) β 1)))) β ((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β0) = ((π΅
βΎ (0..^((β―βπ΅) β 1)))β0)))) |
177 | 56, 158, 16, 176 | syl21anc 837 |
. . . 4
β’ (π β ((β―β(πβ(π΄ βΎ (0..^((β―βπ΄) β 1))))) <
(β―β(πβπ΄)) β ((πβ(π΄ βΎ (0..^((β―βπ΄) β 1)))) = (πβ(π΅ βΎ (0..^((β―βπ΅) β 1)))) β ((π΄ βΎ
(0..^((β―βπ΄)
β 1)))β0) = ((π΅
βΎ (0..^((β―βπ΅) β 1)))β0)))) |
178 | 77, 161, 177 | mp2d 49 |
. . 3
β’ (π β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) =
((π΅ βΎ
(0..^((β―βπ΅)
β 1)))β0)) |
179 | | lbfzo0 13621 |
. . . . 5
β’ (0 β
(0..^((β―βπ΄)
β 1)) β ((β―βπ΄) β 1) β
β) |
180 | 21, 179 | sylibr 233 |
. . . 4
β’ (π β 0 β
(0..^((β―βπ΄)
β 1))) |
181 | 180 | fvresd 6866 |
. . 3
β’ (π β ((π΄ βΎ (0..^((β―βπ΄) β 1)))β0) = (π΄β0)) |
182 | | lbfzo0 13621 |
. . . . 5
β’ (0 β
(0..^((β―βπ΅)
β 1)) β ((β―βπ΅) β 1) β
β) |
183 | 85, 182 | sylibr 233 |
. . . 4
β’ (π β 0 β
(0..^((β―βπ΅)
β 1))) |
184 | 183 | fvresd 6866 |
. . 3
β’ (π β ((π΅ βΎ (0..^((β―βπ΅) β 1)))β0) = (π΅β0)) |
185 | 178, 181,
184 | 3eqtr3d 2781 |
. 2
β’ (π β (π΄β0) = (π΅β0)) |
186 | 185, 19 | pm2.65i 193 |
1
β’ Β¬
π |