Metamath Proof Explorer

Theorem efgtlen

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
Assertion efgtlen 
|- ( ( X e. W /\ A e. ran ( T ` X ) ) -> ( # ` A ) = ( ( # ` X ) + 2 ) )

Proof

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 ffvelcdmi 
 |-  ( 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 ) )