Step | Hyp | Ref
| Expression |
1 | | efgredlem.5 |
. . . . 5
β’ (π β Β¬ (π΄β0) = (π΅β0)) |
2 | | efgredlem.3 |
. . . . . . . . 9
β’ (π β π΅ β dom π) |
3 | | efgval.w |
. . . . . . . . . 10
β’ π = ( I βWord (πΌ Γ
2o)) |
4 | | efgval.r |
. . . . . . . . . 10
β’ βΌ = (
~FG βπΌ) |
5 | | efgval2.m |
. . . . . . . . . 10
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
6 | | efgval2.t |
. . . . . . . . . 10
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
7 | | efgred.d |
. . . . . . . . . 10
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
8 | | efgred.s |
. . . . . . . . . 10
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
9 | 3, 4, 5, 6, 7, 8 | efgsval 19518 |
. . . . . . . . 9
β’ (π΅ β dom π β (πβπ΅) = (π΅β((β―βπ΅) β 1))) |
10 | 2, 9 | syl 17 |
. . . . . . . 8
β’ (π β (πβπ΅) = (π΅β((β―βπ΅) β 1))) |
11 | | efgredlem.4 |
. . . . . . . . 9
β’ (π β (πβπ΄) = (πβπ΅)) |
12 | | efgredlem.2 |
. . . . . . . . . 10
β’ (π β π΄ β dom π) |
13 | 3, 4, 5, 6, 7, 8 | efgsval 19518 |
. . . . . . . . . 10
β’ (π΄ β dom π β (πβπ΄) = (π΄β((β―βπ΄) β 1))) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
β’ (π β (πβπ΄) = (π΄β((β―βπ΄) β 1))) |
15 | 11, 14 | eqtr3d 2775 |
. . . . . . . 8
β’ (π β (πβπ΅) = (π΄β((β―βπ΄) β 1))) |
16 | 10, 15 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (π΅β((β―βπ΅) β 1)) = (π΄β((β―βπ΄) β 1))) |
17 | | oveq1 7365 |
. . . . . . . . 9
β’
((β―βπ΄) =
1 β ((β―βπ΄)
β 1) = (1 β 1)) |
18 | | 1m1e0 12230 |
. . . . . . . . 9
β’ (1
β 1) = 0 |
19 | 17, 18 | eqtrdi 2789 |
. . . . . . . 8
β’
((β―βπ΄) =
1 β ((β―βπ΄)
β 1) = 0) |
20 | 19 | fveq2d 6847 |
. . . . . . 7
β’
((β―βπ΄) =
1 β (π΄β((β―βπ΄) β 1)) = (π΄β0)) |
21 | 16, 20 | sylan9eq 2793 |
. . . . . 6
β’ ((π β§ (β―βπ΄) = 1) β (π΅β((β―βπ΅) β 1)) = (π΄β0)) |
22 | 11 | eleq1d 2819 |
. . . . . . . . 9
β’ (π β ((πβπ΄) β π· β (πβπ΅) β π·)) |
23 | 3, 4, 5, 6, 7, 8 | efgs1b 19523 |
. . . . . . . . . 10
β’ (π΄ β dom π β ((πβπ΄) β π· β (β―βπ΄) = 1)) |
24 | 12, 23 | syl 17 |
. . . . . . . . 9
β’ (π β ((πβπ΄) β π· β (β―βπ΄) = 1)) |
25 | 3, 4, 5, 6, 7, 8 | efgs1b 19523 |
. . . . . . . . . 10
β’ (π΅ β dom π β ((πβπ΅) β π· β (β―βπ΅) = 1)) |
26 | 2, 25 | syl 17 |
. . . . . . . . 9
β’ (π β ((πβπ΅) β π· β (β―βπ΅) = 1)) |
27 | 22, 24, 26 | 3bitr3d 309 |
. . . . . . . 8
β’ (π β ((β―βπ΄) = 1 β
(β―βπ΅) =
1)) |
28 | 27 | biimpa 478 |
. . . . . . 7
β’ ((π β§ (β―βπ΄) = 1) β
(β―βπ΅) =
1) |
29 | | oveq1 7365 |
. . . . . . . . 9
β’
((β―βπ΅) =
1 β ((β―βπ΅)
β 1) = (1 β 1)) |
30 | 29, 18 | eqtrdi 2789 |
. . . . . . . 8
β’
((β―βπ΅) =
1 β ((β―βπ΅)
β 1) = 0) |
31 | 30 | fveq2d 6847 |
. . . . . . 7
β’
((β―βπ΅) =
1 β (π΅β((β―βπ΅) β 1)) = (π΅β0)) |
32 | 28, 31 | syl 17 |
. . . . . 6
β’ ((π β§ (β―βπ΄) = 1) β (π΅β((β―βπ΅) β 1)) = (π΅β0)) |
33 | 21, 32 | eqtr3d 2775 |
. . . . 5
β’ ((π β§ (β―βπ΄) = 1) β (π΄β0) = (π΅β0)) |
34 | 1, 33 | mtand 815 |
. . . 4
β’ (π β Β¬ (β―βπ΄) = 1) |
35 | 3, 4, 5, 6, 7, 8 | efgsdm 19517 |
. . . . . . . 8
β’ (π΄ β dom π β (π΄ β (Word π β {β
}) β§ (π΄β0) β π· β§ βπ’ β (1..^(β―βπ΄))(π΄βπ’) β ran (πβ(π΄β(π’ β 1))))) |
36 | 35 | simp1bi 1146 |
. . . . . . 7
β’ (π΄ β dom π β π΄ β (Word π β {β
})) |
37 | | eldifsn 4748 |
. . . . . . . 8
β’ (π΄ β (Word π β {β
}) β (π΄ β Word π β§ π΄ β β
)) |
38 | | lennncl 14428 |
. . . . . . . 8
β’ ((π΄ β Word π β§ π΄ β β
) β (β―βπ΄) β
β) |
39 | 37, 38 | sylbi 216 |
. . . . . . 7
β’ (π΄ β (Word π β {β
}) β
(β―βπ΄) β
β) |
40 | 12, 36, 39 | 3syl 18 |
. . . . . 6
β’ (π β (β―βπ΄) β
β) |
41 | | elnn1uz2 12855 |
. . . . . 6
β’
((β―βπ΄)
β β β ((β―βπ΄) = 1 β¨ (β―βπ΄) β
(β€β₯β2))) |
42 | 40, 41 | sylib 217 |
. . . . 5
β’ (π β ((β―βπ΄) = 1 β¨ (β―βπ΄) β
(β€β₯β2))) |
43 | 42 | ord 863 |
. . . 4
β’ (π β (Β¬
(β―βπ΄) = 1
β (β―βπ΄)
β (β€β₯β2))) |
44 | 34, 43 | mpd 15 |
. . 3
β’ (π β (β―βπ΄) β
(β€β₯β2)) |
45 | | uz2m1nn 12853 |
. . 3
β’
((β―βπ΄)
β (β€β₯β2) β ((β―βπ΄) β 1) β
β) |
46 | 44, 45 | syl 17 |
. 2
β’ (π β ((β―βπ΄) β 1) β
β) |
47 | 34, 27 | mtbid 324 |
. . . 4
β’ (π β Β¬ (β―βπ΅) = 1) |
48 | 3, 4, 5, 6, 7, 8 | efgsdm 19517 |
. . . . . . . 8
β’ (π΅ β dom π β (π΅ β (Word π β {β
}) β§ (π΅β0) β π· β§ βπ’ β (1..^(β―βπ΅))(π΅βπ’) β ran (πβ(π΅β(π’ β 1))))) |
49 | 48 | simp1bi 1146 |
. . . . . . 7
β’ (π΅ β dom π β π΅ β (Word π β {β
})) |
50 | | eldifsn 4748 |
. . . . . . . 8
β’ (π΅ β (Word π β {β
}) β (π΅ β Word π β§ π΅ β β
)) |
51 | | lennncl 14428 |
. . . . . . . 8
β’ ((π΅ β Word π β§ π΅ β β
) β (β―βπ΅) β
β) |
52 | 50, 51 | sylbi 216 |
. . . . . . 7
β’ (π΅ β (Word π β {β
}) β
(β―βπ΅) β
β) |
53 | 2, 49, 52 | 3syl 18 |
. . . . . 6
β’ (π β (β―βπ΅) β
β) |
54 | | elnn1uz2 12855 |
. . . . . 6
β’
((β―βπ΅)
β β β ((β―βπ΅) = 1 β¨ (β―βπ΅) β
(β€β₯β2))) |
55 | 53, 54 | sylib 217 |
. . . . 5
β’ (π β ((β―βπ΅) = 1 β¨ (β―βπ΅) β
(β€β₯β2))) |
56 | 55 | ord 863 |
. . . 4
β’ (π β (Β¬
(β―βπ΅) = 1
β (β―βπ΅)
β (β€β₯β2))) |
57 | 47, 56 | mpd 15 |
. . 3
β’ (π β (β―βπ΅) β
(β€β₯β2)) |
58 | | uz2m1nn 12853 |
. . 3
β’
((β―βπ΅)
β (β€β₯β2) β ((β―βπ΅) β 1) β
β) |
59 | 57, 58 | syl 17 |
. 2
β’ (π β ((β―βπ΅) β 1) β
β) |
60 | 46, 59 | jca 513 |
1
β’ (π β (((β―βπ΄) β 1) β β
β§ ((β―βπ΅)
β 1) β β)) |