Metamath Proof Explorer

Theorem efgi1

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
Assertion efgi1 
|- ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. ) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 1oelpr 
 |-  1o e. { (/) , 1o }
4 df2o3 
 |-  2o = { (/) , 1o }
5 3 4 eleqtrri 
 |-  1o e. 2o
6 1 2 efgi 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ 1o e. 2o ) ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) )
7 5 6 mpanr2 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) )
8 7 3impa 
 |-  ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) )
9 tru 
 |-  T.
10 eqidd 
 |-  ( T. -> <. J , 1o >. = <. J , 1o >. )
11 difid 
 |-  ( 1o \ 1o ) = (/)
12 11 opeq2i 
 |-  <. J , ( 1o \ 1o ) >. = <. J , (/) >.
13 12 a1i 
 |-  ( T. -> <. J , ( 1o \ 1o ) >. = <. J , (/) >. )
14 10 13 s2eqd 
 |-  ( T. -> <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> = <" <. J , 1o >. <. J , (/) >. "> )
15 oteq3 
 |-  ( <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> = <" <. J , 1o >. <. J , (/) >. "> -> <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. = <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. )
16 9 14 15 mp2b 
 |-  <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. = <. N , N , <" <. J , 1o >. <. J , (/) >. "> >.
17 16 oveq2i 
 |-  ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) = ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. )
18 8 17 breqtrdi 
 |-  ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. ) )