Metamath Proof Explorer


Theorem efgi0

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 efgi0
|- ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. ) )

Proof

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