Theorem vrgpval

Description: The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	vrgpfval.r	|- .~ = ( ~FG ` I )
	vrgpfval.u	|- U = ( varFGrp ` I )
Assertion	vrgpval	|- ( ( I e. V /\ A e. I ) -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	|- .~ = ( ~FG ` I )
2		vrgpfval.u	|- U = ( varFGrp ` I )
3	1 2	vrgpfval	|- ( I e. V -> U = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
4	3	fveq1d	|- ( I e. V -> ( U ` A ) = ( ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) ` A ) )
5		opeq1	|- ( j = A -> <. j , (/) >. = <. A , (/) >. )
6	5	s1eqd	|- ( j = A -> <" <. j , (/) >. "> = <" <. A , (/) >. "> )
7	6	eceq1d	|- ( j = A -> [ <" <. j , (/) >. "> ] .~ = [ <" <. A , (/) >. "> ] .~ )
8		eqid	|- ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ )
9	1	fvexi	|- .~ e. _V
10		ecexg	|- ( .~ e. _V -> [ <" <. A , (/) >. "> ] .~ e. _V )
11	9 10	ax-mp	|- [ <" <. A , (/) >. "> ] .~ e. _V
12	7 8 11	fvmpt	|- ( A e. I -> ( ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) ` A ) = [ <" <. A , (/) >. "> ] .~ )
13	4 12	sylan9eq	|- ( ( I e. V /\ A e. I ) -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )