This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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