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=\mathrm{freeMnd}\left(I\right)$$
	frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
	frmdplusg.p	$$⊢\underset{\dot{}}{+}={+}_M$$
Assertion	frmdadd	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\mathrm{++}Y$$

Proof

Step	Hyp	Ref	Expression
1		frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
2		frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
3		frmdplusg.p	$$⊢\underset{\dot{}}{+}={+}_M$$
4	1 2 3	frmdplusg	$$⊢\underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
5	4	oveqi	$$⊢X\underset{\dot{}}{+}Y=X\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)Y$$
6		ovres	$$⊢\left(X\in B\wedge Y\in B\right)\to X\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)Y=X\mathrm{++}Y$$
7	5 6	syl5eq	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\mathrm{++}Y$$