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

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 1oex 
 |-  1o e. _V
4 3 prid2 
 |-  1o e. { (/) , 1o }
5 df2o3 
 |-  2o = { (/) , 1o }
6 4 5 eleqtrri 
 |-  1o e. 2o
7 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 ) >. "> >. ) )
8 6 7 mpanr2 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) )
9 8 3impa 
 |-  ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) )
10 tru 
 |-  T.
11 eqidd 
 |-  ( T. -> <. J , 1o >. = <. J , 1o >. )
12 difid 
 |-  ( 1o \ 1o ) = (/)
13 12 opeq2i 
 |-  <. J , ( 1o \ 1o ) >. = <. J , (/) >.
14 13 a1i 
 |-  ( T. -> <. J , ( 1o \ 1o ) >. = <. J , (/) >. )
15 11 14 s2eqd 
 |-  ( T. -> <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> = <" <. J , 1o >. <. J , (/) >. "> )
16 oteq3 
 |-  ( <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> = <" <. J , 1o >. <. J , (/) >. "> -> <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. = <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. )
17 10 15 16 mp2b 
 |-  <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. = <. N , N , <" <. J , 1o >. <. J , (/) >. "> >.
18 17 oveq2i 
 |-  ( A splice <. N , N , <" <. J , 1o >. <. J , ( 1o \ 1o ) >. "> >. ) = ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. )
19 9 18 breqtrdi 
 |-  ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. ) )