Step |
Hyp |
Ref |
Expression |
1 |
|
s1cl |
|- ( X e. V -> <" X "> e. Word V ) |
2 |
1
|
adantr |
|- ( ( X e. V /\ Y e. V ) -> <" X "> e. Word V ) |
3 |
|
s1cl |
|- ( Y e. V -> <" Y "> e. Word V ) |
4 |
3
|
adantl |
|- ( ( X e. V /\ Y e. V ) -> <" Y "> e. Word V ) |
5 |
|
1z |
|- 1 e. ZZ |
6 |
|
2z |
|- 2 e. ZZ |
7 |
|
1lt2 |
|- 1 < 2 |
8 |
|
fzolb |
|- ( 1 e. ( 1 ..^ 2 ) <-> ( 1 e. ZZ /\ 2 e. ZZ /\ 1 < 2 ) ) |
9 |
5 6 7 8
|
mpbir3an |
|- 1 e. ( 1 ..^ 2 ) |
10 |
|
s1len |
|- ( # ` <" X "> ) = 1 |
11 |
|
s1len |
|- ( # ` <" Y "> ) = 1 |
12 |
10 11
|
oveq12i |
|- ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = ( 1 + 1 ) |
13 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
14 |
12 13
|
eqtri |
|- ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) = 2 |
15 |
10 14
|
oveq12i |
|- ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) = ( 1 ..^ 2 ) |
16 |
9 15
|
eleqtrri |
|- 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) |
17 |
16
|
a1i |
|- ( ( X e. V /\ Y e. V ) -> 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) ) |
18 |
|
ccatval2 |
|- ( ( <" X "> e. Word V /\ <" Y "> e. Word V /\ 1 e. ( ( # ` <" X "> ) ..^ ( ( # ` <" X "> ) + ( # ` <" Y "> ) ) ) ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) ) |
19 |
2 4 17 18
|
syl3anc |
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) ) |
20 |
10
|
oveq2i |
|- ( 1 - ( # ` <" X "> ) ) = ( 1 - 1 ) |
21 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
22 |
20 21
|
eqtri |
|- ( 1 - ( # ` <" X "> ) ) = 0 |
23 |
22
|
a1i |
|- ( Y e. V -> ( 1 - ( # ` <" X "> ) ) = 0 ) |
24 |
23
|
fveq2d |
|- ( Y e. V -> ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = ( <" Y "> ` 0 ) ) |
25 |
|
s1fv |
|- ( Y e. V -> ( <" Y "> ` 0 ) = Y ) |
26 |
24 25
|
eqtrd |
|- ( Y e. V -> ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = Y ) |
27 |
26
|
adantl |
|- ( ( X e. V /\ Y e. V ) -> ( <" Y "> ` ( 1 - ( # ` <" X "> ) ) ) = Y ) |
28 |
19 27
|
eqtrd |
|- ( ( X e. V /\ Y e. V ) -> ( ( <" X "> ++ <" Y "> ) ` 1 ) = Y ) |