Metamath Proof Explorer

Theorem frgpeccl

Description: Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgp0.m 
|- G = ( freeGrp ` I )
frgp0.r 
|- .~ = ( ~FG ` I )
frgpeccl.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpeccl.b 
|- B = ( Base ` G )
Assertion frgpeccl 
|- ( X e. W -> [ X ] .~ e. B )

Proof

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 )