Metamath Proof Explorer


Theorem efgtval

Description: Value of the extension function, which maps a word (a representation of the group element as a sequence of elements and their inverses) to its direct extensions, defined as the original representation with an element and its inverse inserted somewhere in the string. (Contributed by Mario Carneiro, 29-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 efgtval
|- ( ( X e. W /\ N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) -> ( N ( T ` X ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) )

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 oveqd
 |-  ( X e. W -> ( N ( T ` X ) A ) = ( N ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) A ) )
8 oteq1
 |-  ( a = N -> <. a , a , <" b ( M ` b ) "> >. = <. N , a , <" b ( M ` b ) "> >. )
9 oteq2
 |-  ( a = N -> <. N , a , <" b ( M ` b ) "> >. = <. N , N , <" b ( M ` b ) "> >. )
10 8 9 eqtrd
 |-  ( a = N -> <. a , a , <" b ( M ` b ) "> >. = <. N , N , <" b ( M ` b ) "> >. )
11 10 oveq2d
 |-  ( a = N -> ( X splice <. a , a , <" b ( M ` b ) "> >. ) = ( X splice <. N , N , <" b ( M ` b ) "> >. ) )
12 id
 |-  ( b = A -> b = A )
13 fveq2
 |-  ( b = A -> ( M ` b ) = ( M ` A ) )
14 12 13 s2eqd
 |-  ( b = A -> <" b ( M ` b ) "> = <" A ( M ` A ) "> )
15 14 oteq3d
 |-  ( b = A -> <. N , N , <" b ( M ` b ) "> >. = <. N , N , <" A ( M ` A ) "> >. )
16 15 oveq2d
 |-  ( b = A -> ( X splice <. N , N , <" b ( M ` b ) "> >. ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) )
17 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 ) "> >. ) )
18 ovex
 |-  ( X splice <. N , N , <" A ( M ` A ) "> >. ) e. _V
19 11 16 17 18 ovmpo
 |-  ( ( N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) -> ( N ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) )
20 7 19 sylan9eq
 |-  ( ( X e. W /\ ( N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) ) -> ( N ( T ` X ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) )
21 20 3impb
 |-  ( ( X e. W /\ N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) -> ( N ( T ` X ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) )