Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
3 |
|
efgval2.m |
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) |
4 |
|
efgval2.t |
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) |
5 |
1 2 3 4
|
efgtf |
|- ( X e. W -> ( ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` X ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W ) ) |
6 |
5
|
simpld |
|- ( X e. W -> ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) ) |
7 |
6
|
rneqd |
|- ( X e. W -> ran ( T ` X ) = ran ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) ) |
8 |
7
|
eleq2d |
|- ( X e. W -> ( A e. ran ( T ` X ) <-> A e. ran ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) ) ) |
9 |
|
eqid |
|- ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) |
10 |
|
ovex |
|- ( X splice <. a , a , <" b ( M ` b ) "> >. ) e. _V |
11 |
9 10
|
elrnmpo |
|- ( A e. ran ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) <-> E. a e. ( 0 ... ( # ` X ) ) E. b e. ( I X. 2o ) A = ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) |
12 |
8 11
|
bitrdi |
|- ( X e. W -> ( A e. ran ( T ` X ) <-> E. a e. ( 0 ... ( # ` X ) ) E. b e. ( I X. 2o ) A = ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) ) |
13 |
|
fviss |
|- ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o ) |
14 |
1 13
|
eqsstri |
|- W C_ Word ( I X. 2o ) |
15 |
|
simpl |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> X e. W ) |
16 |
14 15
|
sselid |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> X e. Word ( I X. 2o ) ) |
17 |
|
elfzuz |
|- ( a e. ( 0 ... ( # ` X ) ) -> a e. ( ZZ>= ` 0 ) ) |
18 |
17
|
ad2antrl |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> a e. ( ZZ>= ` 0 ) ) |
19 |
|
eluzfz2b |
|- ( a e. ( ZZ>= ` 0 ) <-> a e. ( 0 ... a ) ) |
20 |
18 19
|
sylib |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> a e. ( 0 ... a ) ) |
21 |
|
simprl |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> a e. ( 0 ... ( # ` X ) ) ) |
22 |
|
simprr |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> b e. ( I X. 2o ) ) |
23 |
3
|
efgmf |
|- M : ( I X. 2o ) --> ( I X. 2o ) |
24 |
23
|
ffvelrni |
|- ( b e. ( I X. 2o ) -> ( M ` b ) e. ( I X. 2o ) ) |
25 |
22 24
|
syl |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( M ` b ) e. ( I X. 2o ) ) |
26 |
22 25
|
s2cld |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> <" b ( M ` b ) "> e. Word ( I X. 2o ) ) |
27 |
16 20 21 26
|
spllen |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( # ` ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( ( # ` X ) + ( ( # ` <" b ( M ` b ) "> ) - ( a - a ) ) ) ) |
28 |
|
s2len |
|- ( # ` <" b ( M ` b ) "> ) = 2 |
29 |
28
|
a1i |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( # ` <" b ( M ` b ) "> ) = 2 ) |
30 |
|
eluzelcn |
|- ( a e. ( ZZ>= ` 0 ) -> a e. CC ) |
31 |
18 30
|
syl |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> a e. CC ) |
32 |
31
|
subidd |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( a - a ) = 0 ) |
33 |
29 32
|
oveq12d |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` <" b ( M ` b ) "> ) - ( a - a ) ) = ( 2 - 0 ) ) |
34 |
|
2cn |
|- 2 e. CC |
35 |
34
|
subid1i |
|- ( 2 - 0 ) = 2 |
36 |
33 35
|
eqtrdi |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` <" b ( M ` b ) "> ) - ( a - a ) ) = 2 ) |
37 |
36
|
oveq2d |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` X ) + ( ( # ` <" b ( M ` b ) "> ) - ( a - a ) ) ) = ( ( # ` X ) + 2 ) ) |
38 |
27 37
|
eqtrd |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( # ` ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( ( # ` X ) + 2 ) ) |
39 |
|
fveqeq2 |
|- ( A = ( X splice <. a , a , <" b ( M ` b ) "> >. ) -> ( ( # ` A ) = ( ( # ` X ) + 2 ) <-> ( # ` ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( ( # ` X ) + 2 ) ) ) |
40 |
38 39
|
syl5ibrcom |
|- ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( A = ( X splice <. a , a , <" b ( M ` b ) "> >. ) -> ( # ` A ) = ( ( # ` X ) + 2 ) ) ) |
41 |
40
|
rexlimdvva |
|- ( X e. W -> ( E. a e. ( 0 ... ( # ` X ) ) E. b e. ( I X. 2o ) A = ( X splice <. a , a , <" b ( M ` b ) "> >. ) -> ( # ` A ) = ( ( # ` X ) + 2 ) ) ) |
42 |
12 41
|
sylbid |
|- ( X e. W -> ( A e. ran ( T ` X ) -> ( # ` A ) = ( ( # ` X ) + 2 ) ) ) |
43 |
42
|
imp |
|- ( ( X e. W /\ A e. ran ( T ` X ) ) -> ( # ` A ) = ( ( # ` X ) + 2 ) ) |