Metamath Proof Explorer

Theorem frgpval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgpval.m 
|- G = ( freeGrp ` I )
frgpval.b 
|- M = ( freeMnd ` ( I X. 2o ) )
frgpval.r 
|- .~ = ( ~FG ` I )
Assertion frgpval 
|- ( I e. V -> G = ( M /s .~ ) )

Proof

Step Hyp Ref Expression
1 frgpval.m 
 |-  G = ( freeGrp ` I )
2 frgpval.b 
 |-  M = ( freeMnd ` ( I X. 2o ) )
3 frgpval.r 
 |-  .~ = ( ~FG ` I )
4 elex 
 |-  ( I e. V -> I e. _V )
5 xpeq1 
 |-  ( i = I -> ( i X. 2o ) = ( I X. 2o ) )
6 5 fveq2d 
 |-  ( i = I -> ( freeMnd ` ( i X. 2o ) ) = ( freeMnd ` ( I X. 2o ) ) )
7 6 2 eqtr4di 
 |-  ( i = I -> ( freeMnd ` ( i X. 2o ) ) = M )
8 fveq2 
 |-  ( i = I -> ( ~FG ` i ) = ( ~FG ` I ) )
9 8 3 eqtr4di 
 |-  ( i = I -> ( ~FG ` i ) = .~ )
10 7 9 oveq12d 
 |-  ( i = I -> ( ( freeMnd ` ( i X. 2o ) ) /s ( ~FG ` i ) ) = ( M /s .~ ) )
11 df-frgp 
 |-  freeGrp = ( i e. _V |-> ( ( freeMnd ` ( i X. 2o ) ) /s ( ~FG ` i ) ) )
12 ovex 
 |-  ( M /s .~ ) e. _V
13 10 11 12 fvmpt 
 |-  ( I e. _V -> ( freeGrp ` I ) = ( M /s .~ ) )
14 4 13 syl 
 |-  ( I e. V -> ( freeGrp ` I ) = ( M /s .~ ) )
15 1 14 syl5eq 
 |-  ( I e. V -> G = ( M /s .~ ) )