Step | Hyp | Ref
| Expression |
1 | | sseqval.2 |
. . . 4
β’ (π β π β Word π) |
2 | | wrdf 14408 |
. . . 4
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π:(0..^(β―βπ))βΆπ) |
4 | | vex 3450 |
. . . . . . . . 9
β’ π€ β V |
5 | 4 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π€ β (π β {β
})) β π€ β V) |
6 | | fvex 6856 |
. . . . . . . . 9
β’ (π₯β((β―βπ₯) β 1)) β
V |
7 | | df-lsw 14452 |
. . . . . . . . 9
β’ lastS =
(π₯ β V β¦ (π₯β((β―βπ₯) β 1))) |
8 | 6, 7 | dmmpti 6646 |
. . . . . . . 8
β’ dom lastS
= V |
9 | 5, 8 | eleqtrrdi 2849 |
. . . . . . 7
β’ ((π β§ π€ β (π β {β
})) β π€ β dom
lastS) |
10 | | eldifsn 4748 |
. . . . . . . . 9
β’ (π€ β (π β {β
}) β (π€ β π β§ π€ β β
)) |
11 | | sseqval.3 |
. . . . . . . . . . . 12
β’ π = (Word π β© (β‘β― β
(β€β₯β(β―βπ)))) |
12 | | inss1 4189 |
. . . . . . . . . . . 12
β’ (Word
π β© (β‘β― β
(β€β₯β(β―βπ)))) β Word π |
13 | 11, 12 | eqsstri 3979 |
. . . . . . . . . . 11
β’ π β Word π |
14 | 13 | sseli 3941 |
. . . . . . . . . 10
β’ (π€ β π β π€ β Word π) |
15 | | lswcl 14457 |
. . . . . . . . . 10
β’ ((π€ β Word π β§ π€ β β
) β (lastSβπ€) β π) |
16 | 14, 15 | sylan 581 |
. . . . . . . . 9
β’ ((π€ β π β§ π€ β β
) β (lastSβπ€) β π) |
17 | 10, 16 | sylbi 216 |
. . . . . . . 8
β’ (π€ β (π β {β
}) β
(lastSβπ€) β
π) |
18 | 17 | adantl 483 |
. . . . . . 7
β’ ((π β§ π€ β (π β {β
})) β
(lastSβπ€) β
π) |
19 | 9, 18 | jca 513 |
. . . . . 6
β’ ((π β§ π€ β (π β {β
})) β (π€ β dom lastS β§
(lastSβπ€) β
π)) |
20 | 19 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ€ β (π β {β
})(π€ β dom lastS β§ (lastSβπ€) β π)) |
21 | 6, 7 | fnmpti 6645 |
. . . . . 6
β’ lastS Fn
V |
22 | | fnfun 6603 |
. . . . . 6
β’ (lastS Fn
V β Fun lastS) |
23 | | ffvresb 7073 |
. . . . . 6
β’ (Fun
lastS β ((lastS βΎ (π β {β
})):(π β {β
})βΆπ β βπ€ β (π β {β
})(π€ β dom lastS β§ (lastSβπ€) β π))) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
β’ ((lastS
βΎ (π β
{β
})):(π β
{β
})βΆπ β
βπ€ β (π β {β
})(π€ β dom lastS β§
(lastSβπ€) β
π)) |
25 | 20, 24 | sylibr 233 |
. . . 4
β’ (π β (lastS βΎ (π β {β
})):(π β {β
})βΆπ) |
26 | | eqid 2737 |
. . . . 5
β’
(β€β₯β(β―βπ)) =
(β€β₯β(β―βπ)) |
27 | | lencl 14422 |
. . . . . . 7
β’ (π β Word π β (β―βπ) β
β0) |
28 | 27 | nn0zd 12526 |
. . . . . 6
β’ (π β Word π β (β―βπ) β β€) |
29 | 1, 28 | syl 17 |
. . . . 5
β’ (π β (β―βπ) β
β€) |
30 | | ovex 7391 |
. . . . . . 7
β’ (π ++ β¨β(πΉβπ)ββ©) β V |
31 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β
(β€β₯β(β―βπ))) β π β
(β€β₯β(β―βπ))) |
32 | 1, 27 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β―βπ) β
β0) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β
(β€β₯β(β―βπ))) β (β―βπ) β
β0) |
34 | | elnn0uz 12809 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (β―βπ) β
(β€β₯β0)) |
35 | 33, 34 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β
(β€β₯β(β―βπ))) β (β―βπ) β
(β€β₯β0)) |
36 | | uztrn 12782 |
. . . . . . . . 9
β’ ((π β
(β€β₯β(β―βπ)) β§ (β―βπ) β (β€β₯β0))
β π β
(β€β₯β0)) |
37 | 31, 35, 36 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β
(β€β₯β(β―βπ))) β π β
(β€β₯β0)) |
38 | | nn0uz 12806 |
. . . . . . . 8
β’
β0 = (β€β₯β0) |
39 | 37, 38 | eleqtrrdi 2849 |
. . . . . . 7
β’ ((π β§ π β
(β€β₯β(β―βπ))) β π β β0) |
40 | | fvconst2g 7152 |
. . . . . . 7
β’ (((π ++ β¨β(πΉβπ)ββ©) β V β§ π β β0)
β ((β0 Γ {(π ++ β¨β(πΉβπ)ββ©)})βπ) = (π ++ β¨β(πΉβπ)ββ©)) |
41 | 30, 39, 40 | sylancr 588 |
. . . . . 6
β’ ((π β§ π β
(β€β₯β(β―βπ))) β ((β0 Γ
{(π ++ β¨β(πΉβπ)ββ©)})βπ) = (π ++ β¨β(πΉβπ)ββ©)) |
42 | | sseqval.4 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆπ) |
43 | | sseqval.1 |
. . . . . . . . . . . . . 14
β’ (π β π β V) |
44 | 43, 1, 11, 42 | sseqmw 32994 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
45 | 42, 44 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ (π β (πΉβπ) β π) |
46 | 45 | s1cld 14492 |
. . . . . . . . . . 11
β’ (π β β¨β(πΉβπ)ββ© β Word π) |
47 | | ccatcl 14463 |
. . . . . . . . . . 11
β’ ((π β Word π β§ β¨β(πΉβπ)ββ© β Word π) β (π ++ β¨β(πΉβπ)ββ©) β Word π) |
48 | 1, 46, 47 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π ++ β¨β(πΉβπ)ββ©) β Word π) |
49 | 30 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π ++ β¨β(πΉβπ)ββ©) β V) |
50 | | ccatws1len 14509 |
. . . . . . . . . . . . 13
β’ (π β Word π β (β―β(π ++ β¨β(πΉβπ)ββ©)) = ((β―βπ) + 1)) |
51 | 1, 50 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β―β(π ++ β¨β(πΉβπ)ββ©)) = ((β―βπ) + 1)) |
52 | | uzid 12779 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β€ β (β―βπ) β
(β€β₯β(β―βπ))) |
53 | | peano2uz 12827 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β (β€β₯β(β―βπ)) β ((β―βπ) + 1) β
(β€β₯β(β―βπ))) |
54 | 29, 52, 53 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ) + 1) β
(β€β₯β(β―βπ))) |
55 | 51, 54 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (π β (β―β(π ++ β¨β(πΉβπ)ββ©)) β
(β€β₯β(β―βπ))) |
56 | | hashf 14239 |
. . . . . . . . . . . 12
β’
β―:VβΆ(β0 βͺ {+β}) |
57 | | ffn 6669 |
. . . . . . . . . . . 12
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
58 | | elpreima 7009 |
. . . . . . . . . . . 12
β’ (β―
Fn V β ((π ++
β¨β(πΉβπ)ββ©) β (β‘β― β
(β€β₯β(β―βπ))) β ((π ++ β¨β(πΉβπ)ββ©) β V β§
(β―β(π ++
β¨β(πΉβπ)ββ©)) β
(β€β₯β(β―βπ))))) |
59 | 56, 57, 58 | mp2b 10 |
. . . . . . . . . . 11
β’ ((π ++ β¨β(πΉβπ)ββ©) β (β‘β― β
(β€β₯β(β―βπ))) β ((π ++ β¨β(πΉβπ)ββ©) β V β§
(β―β(π ++
β¨β(πΉβπ)ββ©)) β
(β€β₯β(β―βπ)))) |
60 | 49, 55, 59 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β (π ++ β¨β(πΉβπ)ββ©) β (β‘β― β
(β€β₯β(β―βπ)))) |
61 | 48, 60 | elind 4155 |
. . . . . . . . 9
β’ (π β (π ++ β¨β(πΉβπ)ββ©) β (Word π β© (β‘β― β
(β€β₯β(β―βπ))))) |
62 | 61, 11 | eleqtrrdi 2849 |
. . . . . . . 8
β’ (π β (π ++ β¨β(πΉβπ)ββ©) β π) |
63 | 62 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β
(β€β₯β(β―βπ))) β (π ++ β¨β(πΉβπ)ββ©) β π) |
64 | | ccatws1n0 14521 |
. . . . . . . . 9
β’ (π β Word π β (π ++ β¨β(πΉβπ)ββ©) β
β
) |
65 | 1, 64 | syl 17 |
. . . . . . . 8
β’ (π β (π ++ β¨β(πΉβπ)ββ©) β
β
) |
66 | 65 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β
(β€β₯β(β―βπ))) β (π ++ β¨β(πΉβπ)ββ©) β
β
) |
67 | | eldifsn 4748 |
. . . . . . 7
β’ ((π ++ β¨β(πΉβπ)ββ©) β (π β {β
}) β ((π ++ β¨β(πΉβπ)ββ©) β π β§ (π ++ β¨β(πΉβπ)ββ©) β
β
)) |
68 | 63, 66, 67 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ π β
(β€β₯β(β―βπ))) β (π ++ β¨β(πΉβπ)ββ©) β (π β {β
})) |
69 | 41, 68 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π β
(β€β₯β(β―βπ))) β ((β0 Γ
{(π ++ β¨β(πΉβπ)ββ©)})βπ) β (π β {β
})) |
70 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)) = (π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©))) |
71 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β§ (π₯ = π β§ π¦ = π)) β π₯ = π) |
72 | 71 | fveq2d 6847 |
. . . . . . . . 9
β’ (((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β§ (π₯ = π β§ π¦ = π)) β (πΉβπ₯) = (πΉβπ)) |
73 | 72 | s1eqd 14490 |
. . . . . . . 8
β’ (((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β§ (π₯ = π β§ π¦ = π)) β β¨β(πΉβπ₯)ββ© = β¨β(πΉβπ)ββ©) |
74 | 71, 73 | oveq12d 7376 |
. . . . . . 7
β’ (((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β§ (π₯ = π β§ π¦ = π)) β (π₯ ++ β¨β(πΉβπ₯)ββ©) = (π ++ β¨β(πΉβπ)ββ©)) |
75 | | vex 3450 |
. . . . . . . 8
β’ π β V |
76 | 75 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β V) |
77 | | vex 3450 |
. . . . . . . 8
β’ π β V |
78 | 77 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β V) |
79 | | ovex 7391 |
. . . . . . . 8
β’ (π ++ β¨β(πΉβπ)ββ©) β V |
80 | 79 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β V) |
81 | 70, 74, 76, 78, 80 | ovmpod 7508 |
. . . . . 6
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π(π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©))π) = (π ++ β¨β(πΉβπ)ββ©)) |
82 | | eldifi 4087 |
. . . . . . . . . . . 12
β’ (π β (π β {β
}) β π β π) |
83 | 82 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β π) |
84 | 13, 83 | sselid 3943 |
. . . . . . . . . 10
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β Word π) |
85 | 42 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β πΉ:πβΆπ) |
86 | 85, 83 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (πΉβπ) β π) |
87 | 86 | s1cld 14492 |
. . . . . . . . . 10
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β
β¨β(πΉβπ)ββ© β Word π) |
88 | | ccatcl 14463 |
. . . . . . . . . 10
β’ ((π β Word π β§ β¨β(πΉβπ)ββ© β Word π) β (π ++ β¨β(πΉβπ)ββ©) β Word π) |
89 | 84, 87, 88 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β Word π) |
90 | 13, 82 | sselid 3943 |
. . . . . . . . . . . . 13
β’ (π β (π β {β
}) β π β Word π) |
91 | 90 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β Word π) |
92 | | ccatws1len 14509 |
. . . . . . . . . . . 12
β’ (π β Word π β (β―β(π ++ β¨β(πΉβπ)ββ©)) = ((β―βπ) + 1)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β
(β―β(π ++
β¨β(πΉβπ)ββ©)) =
((β―βπ) +
1)) |
94 | 83, 11 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β (Word π β© (β‘β― β
(β€β₯β(β―βπ))))) |
95 | 94 | elin2d 4160 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β π β (β‘β― β
(β€β₯β(β―βπ)))) |
96 | | elpreima 7009 |
. . . . . . . . . . . . . 14
β’ (β―
Fn V β (π β
(β‘β― β
(β€β₯β(β―βπ))) β (π β V β§ (β―βπ) β
(β€β₯β(β―βπ))))) |
97 | 56, 57, 96 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (π β (β‘β― β
(β€β₯β(β―βπ))) β (π β V β§ (β―βπ) β
(β€β₯β(β―βπ)))) |
98 | 95, 97 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π β V β§
(β―βπ) β
(β€β₯β(β―βπ)))) |
99 | | peano2uz 12827 |
. . . . . . . . . . . 12
β’
((β―βπ)
β (β€β₯β(β―βπ)) β ((β―βπ) + 1) β
(β€β₯β(β―βπ))) |
100 | 98, 99 | simpl2im 505 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β
((β―βπ) + 1)
β (β€β₯β(β―βπ))) |
101 | 93, 100 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β
(β―β(π ++
β¨β(πΉβπ)ββ©)) β
(β€β₯β(β―βπ))) |
102 | | elpreima 7009 |
. . . . . . . . . . 11
β’ (β―
Fn V β ((π ++
β¨β(πΉβπ)ββ©) β (β‘β― β
(β€β₯β(β―βπ))) β ((π ++ β¨β(πΉβπ)ββ©) β V β§
(β―β(π ++
β¨β(πΉβπ)ββ©)) β
(β€β₯β(β―βπ))))) |
103 | 56, 57, 102 | mp2b 10 |
. . . . . . . . . 10
β’ ((π ++ β¨β(πΉβπ)ββ©) β (β‘β― β
(β€β₯β(β―βπ))) β ((π ++ β¨β(πΉβπ)ββ©) β V β§
(β―β(π ++
β¨β(πΉβπ)ββ©)) β
(β€β₯β(β―βπ)))) |
104 | 80, 101, 103 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β (β‘β― β
(β€β₯β(β―βπ)))) |
105 | 89, 104 | elind 4155 |
. . . . . . . 8
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β (Word π β© (β‘β― β
(β€β₯β(β―βπ))))) |
106 | 105, 11 | eleqtrrdi 2849 |
. . . . . . 7
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β π) |
107 | | ccatws1n0 14521 |
. . . . . . . 8
β’ (π β Word π β (π ++ β¨β(πΉβπ)ββ©) β
β
) |
108 | 91, 107 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β
β
) |
109 | | eldifsn 4748 |
. . . . . . 7
β’ ((π ++ β¨β(πΉβπ)ββ©) β (π β {β
}) β ((π ++ β¨β(πΉβπ)ββ©) β π β§ (π ++ β¨β(πΉβπ)ββ©) β
β
)) |
110 | 106, 108,
109 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π ++ β¨β(πΉβπ)ββ©) β (π β {β
})) |
111 | 81, 110 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ (π β (π β {β
}) β§ π β (π β {β
}))) β (π(π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©))π) β (π β {β
})) |
112 | 26, 29, 69, 111 | seqf 13930 |
. . . 4
β’ (π β seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)})):(β€β₯β(β―βπ))βΆ(π β {β
})) |
113 | | fco2 6696 |
. . . 4
β’ (((lastS
βΎ (π β
{β
})):(π β
{β
})βΆπ β§
seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)})):(β€β₯β(β―βπ))βΆ(π β {β
})) β (lastS β seq(β―βπ)((π₯
β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0 Γ {(π ++ β¨β(πΉβπ)ββ©)}))):(β€β₯β(β―βπ))βΆπ) |
114 | 25, 112, 113 | syl2anc 585 |
. . 3
β’ (π β (lastS β
seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)}))):(β€β₯β(β―βπ))βΆπ) |
115 | | fzouzdisj 13609 |
. . . 4
β’
((0..^(β―βπ)) β©
(β€β₯β(β―βπ))) = β
|
116 | 115 | a1i 11 |
. . 3
β’ (π β ((0..^(β―βπ)) β©
(β€β₯β(β―βπ))) = β
) |
117 | | fun 6705 |
. . 3
β’ (((π:(0..^(β―βπ))βΆπ β§ (lastS β
seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)}))):(β€β₯β(β―βπ))βΆπ) β§ ((0..^(β―βπ)) β© (β€β₯β(β―βπ))) = β
) β (π βͺ (lastS β seq(β―βπ)((π₯ β V,
π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0 Γ {(π ++ β¨β(πΉβπ)ββ©)})))):((0..^(β―βπ)) βͺ (β€β₯β(β―βπ)))βΆ(π βͺ π)) |
118 | 3, 114, 116, 117 | syl21anc 837 |
. 2
β’ (π β (π βͺ (lastS β
seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)})))):((0..^(β―βπ)) βͺ
(β€β₯β(β―βπ)))βΆ(π βͺ π)) |
119 | 43, 1, 11, 42 | sseqval 32991 |
. . 3
β’ (π β (πseqstrπΉ) = (π βͺ (lastS β
seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)}))))) |
120 | | fzouzsplit 13608 |
. . . . . 6
β’
((β―βπ)
β (β€β₯β0) β (β€β₯β0)
= ((0..^(β―βπ))
βͺ (β€β₯β(β―βπ)))) |
121 | 34, 120 | sylbi 216 |
. . . . 5
β’
((β―βπ)
β β0 β (β€β₯β0) =
((0..^(β―βπ))
βͺ (β€β₯β(β―βπ)))) |
122 | 1, 27, 121 | 3syl 18 |
. . . 4
β’ (π β
(β€β₯β0) = ((0..^(β―βπ)) βͺ
(β€β₯β(β―βπ)))) |
123 | 38, 122 | eqtrid 2789 |
. . 3
β’ (π β β0 =
((0..^(β―βπ))
βͺ (β€β₯β(β―βπ)))) |
124 | | unidm 4113 |
. . . . 5
β’ (π βͺ π) = π |
125 | 124 | a1i 11 |
. . . 4
β’ (π β (π βͺ π) = π) |
126 | 125 | eqcomd 2743 |
. . 3
β’ (π β π = (π βͺ π)) |
127 | 119, 123,
126 | feq123d 6658 |
. 2
β’ (π β ((πseqstrπΉ):β0βΆπ β (π βͺ (lastS β
seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0
Γ {(π ++
β¨β(πΉβπ)ββ©)})))):((0..^(β―βπ)) βͺ
(β€β₯β(β―βπ)))βΆ(π βͺ π))) |
128 | 118, 127 | mpbird 257 |
1
β’ (π β (πseqstrπΉ):β0βΆπ) |