Step |
Hyp |
Ref |
Expression |
1 |
|
hasheq0 |
|- ( W e. Word V -> ( ( # ` W ) = 0 <-> W = (/) ) ) |
2 |
1
|
biimpa |
|- ( ( W e. Word V /\ ( # ` W ) = 0 ) -> W = (/) ) |
3 |
|
s1cli |
|- <" (/) "> e. Word _V |
4 |
|
ccatlid |
|- ( <" (/) "> e. Word _V -> ( (/) ++ <" (/) "> ) = <" (/) "> ) |
5 |
3 4
|
ax-mp |
|- ( (/) ++ <" (/) "> ) = <" (/) "> |
6 |
5
|
fveq1i |
|- ( ( (/) ++ <" (/) "> ) ` 0 ) = ( <" (/) "> ` 0 ) |
7 |
|
0ex |
|- (/) e. _V |
8 |
|
s1fv |
|- ( (/) e. _V -> ( <" (/) "> ` 0 ) = (/) ) |
9 |
7 8
|
ax-mp |
|- ( <" (/) "> ` 0 ) = (/) |
10 |
6 9
|
eqtri |
|- ( ( (/) ++ <" (/) "> ) ` 0 ) = (/) |
11 |
|
id |
|- ( W = (/) -> W = (/) ) |
12 |
|
fveq1 |
|- ( W = (/) -> ( W ` 0 ) = ( (/) ` 0 ) ) |
13 |
|
0fv |
|- ( (/) ` 0 ) = (/) |
14 |
12 13
|
eqtrdi |
|- ( W = (/) -> ( W ` 0 ) = (/) ) |
15 |
14
|
s1eqd |
|- ( W = (/) -> <" ( W ` 0 ) "> = <" (/) "> ) |
16 |
11 15
|
oveq12d |
|- ( W = (/) -> ( W ++ <" ( W ` 0 ) "> ) = ( (/) ++ <" (/) "> ) ) |
17 |
16
|
fveq1d |
|- ( W = (/) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( ( (/) ++ <" (/) "> ) ` 0 ) ) |
18 |
10 17 14
|
3eqtr4a |
|- ( W = (/) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) ) |
19 |
2 18
|
syl |
|- ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) ) |
20 |
1
|
necon3bid |
|- ( W e. Word V -> ( ( # ` W ) =/= 0 <-> W =/= (/) ) ) |
21 |
20
|
biimpa |
|- ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> W =/= (/) ) |
22 |
|
lennncl |
|- ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN ) |
23 |
21 22
|
syldan |
|- ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> ( # ` W ) e. NN ) |
24 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN ) |
25 |
23 24
|
sylibr |
|- ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) |
26 |
|
ccats1val1 |
|- ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) ) |
27 |
25 26
|
syldan |
|- ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) ) |
28 |
19 27
|
pm2.61dane |
|- ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) ) |