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

Metamath Proof Explorer

Theorem vrgpfval

Description: The canonical injection from the generating set I to the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 vrgpfval.r 
 |-  .~ = ( ~FG ` I )
2 vrgpfval.u 
 |-  U = ( varFGrp ` I )
3 elex 
 |-  ( I e. V -> I e. _V )
4 id 
 |-  ( i = I -> i = I )
5 fveq2 
 |-  ( i = I -> ( ~FG ` i ) = ( ~FG ` I ) )
6 5 1 eqtr4di 
 |-  ( i = I -> ( ~FG ` i ) = .~ )
7 6 eceq2d 
 |-  ( i = I -> [ <" <. j , (/) >. "> ] ( ~FG ` i ) = [ <" <. j , (/) >. "> ] .~ )
8 4 7 mpteq12dv 
 |-  ( i = I -> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
9 df-vrgp 
 |-  varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) )
10 vex 
 |-  i e. _V
11 10 mptex 
 |-  ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) e. _V
12 8 9 11 fvmpt3i 
 |-  ( I e. _V -> ( varFGrp ` I ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
13 3 12 syl 
 |-  ( I e. V -> ( varFGrp ` I ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
14 2 13 eqtrid 
 |-  ( I e. V -> U = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )