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 ) ) |
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 ) ) |