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