Step |
Hyp |
Ref |
Expression |
1 |
|
ccatfval |
|- ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) ) |
2 |
1
|
3adant3 |
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) ) |
3 |
|
eleq1 |
|- ( x = I -> ( x e. ( 0 ..^ ( # ` S ) ) <-> I e. ( 0 ..^ ( # ` S ) ) ) ) |
4 |
|
fveq2 |
|- ( x = I -> ( S ` x ) = ( S ` I ) ) |
5 |
|
fvoveq1 |
|- ( x = I -> ( T ` ( x - ( # ` S ) ) ) = ( T ` ( I - ( # ` S ) ) ) ) |
6 |
3 4 5
|
ifbieq12d |
|- ( x = I -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) = if ( I e. ( 0 ..^ ( # ` S ) ) , ( S ` I ) , ( T ` ( I - ( # ` S ) ) ) ) ) |
7 |
|
fzodisj |
|- ( ( 0 ..^ ( # ` S ) ) i^i ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) = (/) |
8 |
|
minel |
|- ( ( I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) /\ ( ( 0 ..^ ( # ` S ) ) i^i ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) = (/) ) -> -. I e. ( 0 ..^ ( # ` S ) ) ) |
9 |
7 8
|
mpan2 |
|- ( I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) -> -. I e. ( 0 ..^ ( # ` S ) ) ) |
10 |
9
|
3ad2ant3 |
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> -. I e. ( 0 ..^ ( # ` S ) ) ) |
11 |
10
|
iffalsed |
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( I e. ( 0 ..^ ( # ` S ) ) , ( S ` I ) , ( T ` ( I - ( # ` S ) ) ) ) = ( T ` ( I - ( # ` S ) ) ) ) |
12 |
6 11
|
sylan9eqr |
|- ( ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x = I ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) = ( T ` ( I - ( # ` S ) ) ) ) |
13 |
|
wrdfin |
|- ( S e. Word B -> S e. Fin ) |
14 |
13
|
adantr |
|- ( ( S e. Word B /\ T e. Word B ) -> S e. Fin ) |
15 |
|
hashcl |
|- ( S e. Fin -> ( # ` S ) e. NN0 ) |
16 |
|
fzoss1 |
|- ( ( # ` S ) e. ( ZZ>= ` 0 ) -> ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) |
17 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
18 |
16 17
|
eleq2s |
|- ( ( # ` S ) e. NN0 -> ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) |
19 |
14 15 18
|
3syl |
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) |
20 |
19
|
sseld |
|- ( ( S e. Word B /\ T e. Word B ) -> ( I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) ) |
21 |
20
|
3impia |
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) |
22 |
|
fvexd |
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( T ` ( I - ( # ` S ) ) ) e. _V ) |
23 |
2 12 21 22
|
fvmptd |
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( ( S ++ T ) ` I ) = ( T ` ( I - ( # ` S ) ) ) ) |