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