Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . . 4
β’ βΌ = (
~FG βπΌ) |
3 | | efgval2.m |
. . . 4
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
4 | | efgval2.t |
. . . 4
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
5 | | efgred.d |
. . . 4
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
6 | | efgred.s |
. . . 4
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsval 19601 |
. . 3
β’ ((π΄ ++ β¨βπ΅ββ©) β dom π β (πβ(π΄ ++ β¨βπ΅ββ©)) = ((π΄ ++ β¨βπ΅ββ©)β((β―β(π΄ ++ β¨βπ΅ββ©)) β
1))) |
8 | | s1cl 14554 |
. . . . . . . . 9
β’ (π΅ β π β β¨βπ΅ββ© β Word π) |
9 | | ccatlen 14527 |
. . . . . . . . 9
β’ ((π΄ β Word π β§ β¨βπ΅ββ© β Word π) β (β―β(π΄ ++ β¨βπ΅ββ©)) = ((β―βπ΄) +
(β―ββ¨βπ΅ββ©))) |
10 | 8, 9 | sylan2 593 |
. . . . . . . 8
β’ ((π΄ β Word π β§ π΅ β π) β (β―β(π΄ ++ β¨βπ΅ββ©)) = ((β―βπ΄) +
(β―ββ¨βπ΅ββ©))) |
11 | | s1len 14558 |
. . . . . . . . 9
β’
(β―ββ¨βπ΅ββ©) = 1 |
12 | 11 | oveq2i 7422 |
. . . . . . . 8
β’
((β―βπ΄) +
(β―ββ¨βπ΅ββ©)) = ((β―βπ΄) + 1) |
13 | 10, 12 | eqtrdi 2788 |
. . . . . . 7
β’ ((π΄ β Word π β§ π΅ β π) β (β―β(π΄ ++ β¨βπ΅ββ©)) = ((β―βπ΄) + 1)) |
14 | 13 | oveq1d 7426 |
. . . . . 6
β’ ((π΄ β Word π β§ π΅ β π) β ((β―β(π΄ ++ β¨βπ΅ββ©)) β 1) =
(((β―βπ΄) + 1)
β 1)) |
15 | | lencl 14485 |
. . . . . . . . . 10
β’ (π΄ β Word π β (β―βπ΄) β
β0) |
16 | 15 | nn0cnd 12536 |
. . . . . . . . 9
β’ (π΄ β Word π β (β―βπ΄) β β) |
17 | | ax-1cn 11170 |
. . . . . . . . 9
β’ 1 β
β |
18 | | pncan 11468 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ 1 β β) β (((β―βπ΄) + 1) β 1) =
(β―βπ΄)) |
19 | 16, 17, 18 | sylancl 586 |
. . . . . . . 8
β’ (π΄ β Word π β (((β―βπ΄) + 1) β 1) = (β―βπ΄)) |
20 | 16 | addlidd 11417 |
. . . . . . . 8
β’ (π΄ β Word π β (0 + (β―βπ΄)) = (β―βπ΄)) |
21 | 19, 20 | eqtr4d 2775 |
. . . . . . 7
β’ (π΄ β Word π β (((β―βπ΄) + 1) β 1) = (0 +
(β―βπ΄))) |
22 | 21 | adantr 481 |
. . . . . 6
β’ ((π΄ β Word π β§ π΅ β π) β (((β―βπ΄) + 1) β 1) = (0 +
(β―βπ΄))) |
23 | 14, 22 | eqtrd 2772 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β π) β ((β―β(π΄ ++ β¨βπ΅ββ©)) β 1) = (0 +
(β―βπ΄))) |
24 | 23 | fveq2d 6895 |
. . . 4
β’ ((π΄ β Word π β§ π΅ β π) β ((π΄ ++ β¨βπ΅ββ©)β((β―β(π΄ ++ β¨βπ΅ββ©)) β 1)) =
((π΄ ++ β¨βπ΅ββ©)β(0 +
(β―βπ΄)))) |
25 | | simpl 483 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β π) β π΄ β Word π) |
26 | 8 | adantl 482 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β π) β β¨βπ΅ββ© β Word π) |
27 | | 1nn 12225 |
. . . . . . . 8
β’ 1 β
β |
28 | 11, 27 | eqeltri 2829 |
. . . . . . 7
β’
(β―ββ¨βπ΅ββ©) β
β |
29 | | lbfzo0 13674 |
. . . . . . 7
β’ (0 β
(0..^(β―ββ¨βπ΅ββ©)) β
(β―ββ¨βπ΅ββ©) β
β) |
30 | 28, 29 | mpbir 230 |
. . . . . 6
β’ 0 β
(0..^(β―ββ¨βπ΅ββ©)) |
31 | 30 | a1i 11 |
. . . . 5
β’ ((π΄ β Word π β§ π΅ β π) β 0 β
(0..^(β―ββ¨βπ΅ββ©))) |
32 | | ccatval3 14531 |
. . . . 5
β’ ((π΄ β Word π β§ β¨βπ΅ββ© β Word π β§ 0 β
(0..^(β―ββ¨βπ΅ββ©))) β ((π΄ ++ β¨βπ΅ββ©)β(0 +
(β―βπ΄))) =
(β¨βπ΅ββ©β0)) |
33 | 25, 26, 31, 32 | syl3anc 1371 |
. . . 4
β’ ((π΄ β Word π β§ π΅ β π) β ((π΄ ++ β¨βπ΅ββ©)β(0 +
(β―βπ΄))) =
(β¨βπ΅ββ©β0)) |
34 | | s1fv 14562 |
. . . . 5
β’ (π΅ β π β (β¨βπ΅ββ©β0) = π΅) |
35 | 34 | adantl 482 |
. . . 4
β’ ((π΄ β Word π β§ π΅ β π) β (β¨βπ΅ββ©β0) = π΅) |
36 | 24, 33, 35 | 3eqtrd 2776 |
. . 3
β’ ((π΄ β Word π β§ π΅ β π) β ((π΄ ++ β¨βπ΅ββ©)β((β―β(π΄ ++ β¨βπ΅ββ©)) β 1)) =
π΅) |
37 | 7, 36 | sylan9eqr 2794 |
. 2
β’ (((π΄ β Word π β§ π΅ β π) β§ (π΄ ++ β¨βπ΅ββ©) β dom π) β (πβ(π΄ ++ β¨βπ΅ββ©)) = π΅) |
38 | 37 | 3impa 1110 |
1
β’ ((π΄ β Word π β§ π΅ β π β§ (π΄ ++ β¨βπ΅ββ©) β dom π) β (πβ(π΄ ++ β¨βπ΅ββ©)) = π΅) |