| 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
|
eqtrid |
|- ( I e. V -> G = ( M /s .~ ) ) |