| Step |
Hyp |
Ref |
Expression |
| 1 |
|
frgp0.m |
|- G = ( freeGrp ` I ) |
| 2 |
|
frgp0.r |
|- .~ = ( ~FG ` I ) |
| 3 |
|
frgpeccl.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
| 4 |
|
frgpeccl.b |
|- B = ( Base ` G ) |
| 5 |
2
|
fvexi |
|- .~ e. _V |
| 6 |
5
|
ecelqsi |
|- ( X e. W -> [ X ] .~ e. ( W /. .~ ) ) |
| 7 |
3
|
efgrcl |
|- ( X e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) ) |
| 8 |
7
|
simpld |
|- ( X e. W -> I e. _V ) |
| 9 |
|
eqid |
|- ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) ) |
| 10 |
1 9 2
|
frgpval |
|- ( I e. _V -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) ) |
| 11 |
8 10
|
syl |
|- ( X e. W -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) ) |
| 12 |
7
|
simprd |
|- ( X e. W -> W = Word ( I X. 2o ) ) |
| 13 |
|
2on |
|- 2o e. On |
| 14 |
|
xpexg |
|- ( ( I e. _V /\ 2o e. On ) -> ( I X. 2o ) e. _V ) |
| 15 |
8 13 14
|
sylancl |
|- ( X e. W -> ( I X. 2o ) e. _V ) |
| 16 |
|
eqid |
|- ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) |
| 17 |
9 16
|
frmdbas |
|- ( ( I X. 2o ) e. _V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) ) |
| 18 |
15 17
|
syl |
|- ( X e. W -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) ) |
| 19 |
12 18
|
eqtr4d |
|- ( X e. W -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) |
| 20 |
5
|
a1i |
|- ( X e. W -> .~ e. _V ) |
| 21 |
|
fvexd |
|- ( X e. W -> ( freeMnd ` ( I X. 2o ) ) e. _V ) |
| 22 |
11 19 20 21
|
qusbas |
|- ( X e. W -> ( W /. .~ ) = ( Base ` G ) ) |
| 23 |
22 4
|
eqtr4di |
|- ( X e. W -> ( W /. .~ ) = B ) |
| 24 |
6 23
|
eleqtrd |
|- ( X e. W -> [ X ] .~ e. B ) |