Metamath Proof Explorer

Theorem efgtf

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

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 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
6 1 5 eqsstri 
 |-  W C_ Word ( I X. 2o )
7 simpl 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> X e. W )
8 6 7 sseldi 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> X e. Word ( I X. 2o ) )
9 simprr 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> b e. ( I X. 2o ) )
10 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
11 10 ffvelrni 
 |-  ( b e. ( I X. 2o ) -> ( M ` b ) e. ( I X. 2o ) )
12 11 ad2antll 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( M ` b ) e. ( I X. 2o ) )
13 9 12 s2cld 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> <" b ( M ` b ) "> e. Word ( I X. 2o ) )
14 splcl 
 |-  ( ( X e. Word ( I X. 2o ) /\ <" b ( M ` b ) "> e. Word ( I X. 2o ) ) -> ( X splice <. a , a , <" b ( M ` b ) "> >. ) e. Word ( I X. 2o ) )
15 8 13 14 syl2anc 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( X splice <. a , a , <" b ( M ` b ) "> >. ) e. Word ( I X. 2o ) )
16 1 efgrcl 
 |-  ( X e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
17 16 simprd 
 |-  ( X e. W -> W = Word ( I X. 2o ) )
18 17 adantr 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> W = Word ( I X. 2o ) )
19 15 18 eleqtrrd 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) /\ b e. ( I X. 2o ) ) ) -> ( X splice <. a , a , <" b ( M ` b ) "> >. ) e. W )
20 19 ralrimivva 
 |-  ( X e. W -> A. a e. ( 0 ... ( # ` X ) ) A. b e. ( I X. 2o ) ( X splice <. a , a , <" b ( M ` b ) "> >. ) e. W )
21 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 ) "> >. ) )
22 21 fmpo 
 |-  ( A. a e. ( 0 ... ( # ` X ) ) A. b e. ( I X. 2o ) ( X splice <. a , a , <" b ( M ` b ) "> >. ) e. W <-> ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W )
23 20 22 sylib 
 |-  ( X e. W -> ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W )
24 ovex 
 |-  ( 0 ... ( # ` X ) ) e. _V
25 16 simpld 
 |-  ( X e. W -> I e. _V )
26 2on 
 |-  2o e. On
27 xpexg 
 |-  ( ( I e. _V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
28 25 26 27 sylancl 
 |-  ( X e. W -> ( I X. 2o ) e. _V )
29 xpexg 
 |-  ( ( ( 0 ... ( # ` X ) ) e. _V /\ ( I X. 2o ) e. _V ) -> ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) e. _V )
30 24 28 29 sylancr 
 |-  ( X e. W -> ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) e. _V )
31 1 fvexi 
 |-  W e. _V
32 31 a1i 
 |-  ( X e. W -> W e. _V )
33 fex2 
 |-  ( ( ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W /\ ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) e. _V /\ W e. _V ) -> ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) e. _V )
34 23 30 32 33 syl3anc 
 |-  ( X e. W -> ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) e. _V )
35 fveq2 
 |-  ( u = X -> ( # ` u ) = ( # ` X ) )
36 35 oveq2d 
 |-  ( u = X -> ( 0 ... ( # ` u ) ) = ( 0 ... ( # ` X ) ) )
37 eqidd 
 |-  ( u = X -> ( I X. 2o ) = ( I X. 2o ) )
38 oveq1 
 |-  ( u = X -> ( u splice <. a , a , <" b ( M ` b ) "> >. ) = ( X splice <. a , a , <" b ( M ` b ) "> >. ) )
39 36 37 38 mpoeq123dv 
 |-  ( u = X -> ( a e. ( 0 ... ( # ` u ) ) , b e. ( I X. 2o ) |-> ( u splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) )
40 oteq1 
 |-  ( n = a -> <. n , n , <" w ( M ` w ) "> >. = <. a , n , <" w ( M ` w ) "> >. )
41 oteq2 
 |-  ( n = a -> <. a , n , <" w ( M ` w ) "> >. = <. a , a , <" w ( M ` w ) "> >. )
42 40 41 eqtrd 
 |-  ( n = a -> <. n , n , <" w ( M ` w ) "> >. = <. a , a , <" w ( M ` w ) "> >. )
43 42 oveq2d 
 |-  ( n = a -> ( v splice <. n , n , <" w ( M ` w ) "> >. ) = ( v splice <. a , a , <" w ( M ` w ) "> >. ) )
44 id 
 |-  ( w = b -> w = b )
45 fveq2 
 |-  ( w = b -> ( M ` w ) = ( M ` b ) )
46 44 45 s2eqd 
 |-  ( w = b -> <" w ( M ` w ) "> = <" b ( M ` b ) "> )
47 46 oteq3d 
 |-  ( w = b -> <. a , a , <" w ( M ` w ) "> >. = <. a , a , <" b ( M ` b ) "> >. )
48 47 oveq2d 
 |-  ( w = b -> ( v splice <. a , a , <" w ( M ` w ) "> >. ) = ( v splice <. a , a , <" b ( M ` b ) "> >. ) )
49 43 48 cbvmpov 
 |-  ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) = ( a e. ( 0 ... ( # ` v ) ) , b e. ( I X. 2o ) |-> ( v splice <. a , a , <" b ( M ` b ) "> >. ) )
50 fveq2 
 |-  ( v = u -> ( # ` v ) = ( # ` u ) )
51 50 oveq2d 
 |-  ( v = u -> ( 0 ... ( # ` v ) ) = ( 0 ... ( # ` u ) ) )
52 eqidd 
 |-  ( v = u -> ( I X. 2o ) = ( I X. 2o ) )
53 oveq1 
 |-  ( v = u -> ( v splice <. a , a , <" b ( M ` b ) "> >. ) = ( u splice <. a , a , <" b ( M ` b ) "> >. ) )
54 51 52 53 mpoeq123dv 
 |-  ( v = u -> ( a e. ( 0 ... ( # ` v ) ) , b e. ( I X. 2o ) |-> ( v splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( a e. ( 0 ... ( # ` u ) ) , b e. ( I X. 2o ) |-> ( u splice <. a , a , <" b ( M ` b ) "> >. ) ) )
55 49 54 syl5eq 
 |-  ( v = u -> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) = ( a e. ( 0 ... ( # ` u ) ) , b e. ( I X. 2o ) |-> ( u splice <. a , a , <" b ( M ` b ) "> >. ) ) )
56 55 cbvmptv 
 |-  ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) = ( u e. W |-> ( a e. ( 0 ... ( # ` u ) ) , b e. ( I X. 2o ) |-> ( u splice <. a , a , <" b ( M ` b ) "> >. ) ) )
57 4 56 eqtri 
 |-  T = ( u e. W |-> ( a e. ( 0 ... ( # ` u ) ) , b e. ( I X. 2o ) |-> ( u splice <. a , a , <" b ( M ` b ) "> >. ) ) )
58 39 57 fvmptg 
 |-  ( ( X e. W /\ ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) e. _V ) -> ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) )
59 34 58 mpdan 
 |-  ( X e. W -> ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) )
60 59 feq1d 
 |-  ( X e. W -> ( ( T ` X ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W <-> ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W ) )
61 23 60 mpbird 
 |-  ( X e. W -> ( T ` X ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W )
62 59 61 jca 
 |-  ( 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 ) )