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 , (/) >. "> >. ) )