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

Metamath Proof Explorer

Theorem frmdbas

Description: The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frmdbas.m 
|- M = ( freeMnd ` I )
frmdbas.b 
|- B = ( Base ` M )
Assertion frmdbas 
|- ( I e. V -> B = Word I )

Proof

Step Hyp Ref Expression
1 frmdbas.m 
 |-  M = ( freeMnd ` I )
2 frmdbas.b 
 |-  B = ( Base ` M )
3 eqidd 
 |-  ( I e. V -> Word I = Word I )
4 eqid 
 |-  ( ++ |` ( Word I X. Word I ) ) = ( ++ |` ( Word I X. Word I ) )
5 1 3 4 frmdval 
 |-  ( I e. V -> M = { <. ( Base ` ndx ) , Word I >. , <. ( +g ` ndx ) , ( ++ |` ( Word I X. Word I ) ) >. } )
6 5 fveq2d 
 |-  ( I e. V -> ( Base ` M ) = ( Base ` { <. ( Base ` ndx ) , Word I >. , <. ( +g ` ndx ) , ( ++ |` ( Word I X. Word I ) ) >. } ) )
7 wrdexg 
 |-  ( I e. V -> Word I e. _V )
8 eqid 
 |-  { <. ( Base ` ndx ) , Word I >. , <. ( +g ` ndx ) , ( ++ |` ( Word I X. Word I ) ) >. } = { <. ( Base ` ndx ) , Word I >. , <. ( +g ` ndx ) , ( ++ |` ( Word I X. Word I ) ) >. }
9 8 grpbase 
 |-  ( Word I e. _V -> Word I = ( Base ` { <. ( Base ` ndx ) , Word I >. , <. ( +g ` ndx ) , ( ++ |` ( Word I X. Word I ) ) >. } ) )
10 7 9 syl 
 |-  ( I e. V -> Word I = ( Base ` { <. ( Base ` ndx ) , Word I >. , <. ( +g ` ndx ) , ( ++ |` ( Word I X. Word I ) ) >. } ) )
11 6 10 eqtr4d 
 |-  ( I e. V -> ( Base ` M ) = Word I )
12 2 11 eqtrid 
 |-  ( I e. V -> B = Word I )