Metamath Proof Explorer

Theorem vrgpinv

Description: The inverse of a generating element is represented by <. A , 1 >. instead of <. A , 0 >. . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses vrgpfval.r 
|- .~ = ( ~FG ` I )
vrgpfval.u 
|- U = ( varFGrp ` I )
vrgpf.m 
|- G = ( freeGrp ` I )
vrgpinv.n 
|- N = ( invg ` G )
Assertion vrgpinv 
|- ( ( I e. V /\ A e. I ) -> ( N ` ( U ` A ) ) = [ <" <. A , 1o >. "> ] .~ )

Proof

Step Hyp Ref Expression
1 vrgpfval.r 
 |-  .~ = ( ~FG ` I )
2 vrgpfval.u 
 |-  U = ( varFGrp ` I )
3 vrgpf.m 
 |-  G = ( freeGrp ` I )
4 vrgpinv.n 
 |-  N = ( invg ` G )
5 1 2 vrgpval 
 |-  ( ( I e. V /\ A e. I ) -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )
6 5 fveq2d 
 |-  ( ( I e. V /\ A e. I ) -> ( N ` ( U ` A ) ) = ( N ` [ <" <. A , (/) >. "> ] .~ ) )
7 simpr 
 |-  ( ( I e. V /\ A e. I ) -> A e. I )
8 0ex 
 |-  (/) e. _V
9 8 prid1 
 |-  (/) e. { (/) , 1o }
10 df2o3 
 |-  2o = { (/) , 1o }
11 9 10 eleqtrri 
 |-  (/) e. 2o
12 opelxpi 
 |-  ( ( A e. I /\ (/) e. 2o ) -> <. A , (/) >. e. ( I X. 2o ) )
13 7 11 12 sylancl 
 |-  ( ( I e. V /\ A e. I ) -> <. A , (/) >. e. ( I X. 2o ) )
14 13 s1cld 
 |-  ( ( I e. V /\ A e. I ) -> <" <. A , (/) >. "> e. Word ( I X. 2o ) )
15 simpl 
 |-  ( ( I e. V /\ A e. I ) -> I e. V )
16 2on 
 |-  2o e. On
17 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
18 15 16 17 sylancl 
 |-  ( ( I e. V /\ A e. I ) -> ( I X. 2o ) e. _V )
19 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
20 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
21 18 19 20 3syl 
 |-  ( ( I e. V /\ A e. I ) -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
22 14 21 eleqtrrd 
 |-  ( ( I e. V /\ A e. I ) -> <" <. A , (/) >. "> e. ( _I ` Word ( I X. 2o ) ) )
23 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
24 eqid 
 |-  ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) = ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. )
25 23 3 1 4 24 frgpinv 
 |-  ( <" <. A , (/) >. "> e. ( _I ` Word ( I X. 2o ) ) -> ( N ` [ <" <. A , (/) >. "> ] .~ ) = [ ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. ( reverse ` <" <. A , (/) >. "> ) ) ] .~ )
26 22 25 syl 
 |-  ( ( I e. V /\ A e. I ) -> ( N ` [ <" <. A , (/) >. "> ] .~ ) = [ ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. ( reverse ` <" <. A , (/) >. "> ) ) ] .~ )
27 revs1 
 |-  ( reverse ` <" <. A , (/) >. "> ) = <" <. A , (/) >. ">
28 27 a1i 
 |-  ( ( I e. V /\ A e. I ) -> ( reverse ` <" <. A , (/) >. "> ) = <" <. A , (/) >. "> )
29 28 coeq2d 
 |-  ( ( I e. V /\ A e. I ) -> ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. ( reverse ` <" <. A , (/) >. "> ) ) = ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. <" <. A , (/) >. "> ) )
30 24 efgmf 
 |-  ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) : ( I X. 2o ) --> ( I X. 2o )
31 s1co 
 |-  ( ( <. A , (/) >. e. ( I X. 2o ) /\ ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) : ( I X. 2o ) --> ( I X. 2o ) ) -> ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. <" <. A , (/) >. "> ) = <" ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) ` <. A , (/) >. ) "> )
32 13 30 31 sylancl 
 |-  ( ( I e. V /\ A e. I ) -> ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. <" <. A , (/) >. "> ) = <" ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) ` <. A , (/) >. ) "> )
33 24 efgmval 
 |-  ( ( A e. I /\ (/) e. 2o ) -> ( A ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) (/) ) = <. A , ( 1o \ (/) ) >. )
34 7 11 33 sylancl 
 |-  ( ( I e. V /\ A e. I ) -> ( A ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) (/) ) = <. A , ( 1o \ (/) ) >. )
35 df-ov 
 |-  ( A ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) (/) ) = ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) ` <. A , (/) >. )
36 dif0 
 |-  ( 1o \ (/) ) = 1o
37 36 opeq2i 
 |-  <. A , ( 1o \ (/) ) >. = <. A , 1o >.
38 34 35 37 3eqtr3g 
 |-  ( ( I e. V /\ A e. I ) -> ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) ` <. A , (/) >. ) = <. A , 1o >. )
39 38 s1eqd 
 |-  ( ( I e. V /\ A e. I ) -> <" ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) ` <. A , (/) >. ) "> = <" <. A , 1o >. "> )
40 29 32 39 3eqtrd 
 |-  ( ( I e. V /\ A e. I ) -> ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. ( reverse ` <" <. A , (/) >. "> ) ) = <" <. A , 1o >. "> )
41 40 eceq1d 
 |-  ( ( I e. V /\ A e. I ) -> [ ( ( x e. I , y e. 2o |-> <. x , ( 1o \ y ) >. ) o. ( reverse ` <" <. A , (/) >. "> ) ) ] .~ = [ <" <. A , 1o >. "> ] .~ )
42 6 26 41 3eqtrd 
 |-  ( ( I e. V /\ A e. I ) -> ( N ` ( U ` A ) ) = [ <" <. A , 1o >. "> ] .~ )