Metamath Proof Explorer


Theorem frmdadd

Description: Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdbas.m
|- M = ( freeMnd ` I )
frmdbas.b
|- B = ( Base ` M )
frmdplusg.p
|- .+ = ( +g ` M )
Assertion frmdadd
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X ++ Y ) )

Proof

Step Hyp Ref Expression
1 frmdbas.m
 |-  M = ( freeMnd ` I )
2 frmdbas.b
 |-  B = ( Base ` M )
3 frmdplusg.p
 |-  .+ = ( +g ` M )
4 1 2 3 frmdplusg
 |-  .+ = ( ++ |` ( B X. B ) )
5 4 oveqi
 |-  ( X .+ Y ) = ( X ( ++ |` ( B X. B ) ) Y )
6 ovres
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( ++ |` ( B X. B ) ) Y ) = ( X ++ Y ) )
7 5 6 syl5eq
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X ++ Y ) )