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

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	$⊢ \underset{˙}{+} = +_{M}$
Assertion	frmdadd	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X ++ Y$

Step	Hyp	Ref	Expression
1		frmdbas.m	$⊢ M = freeMnd (I)$
2		frmdbas.b	$⊢ B = {Base}_{M}$
3		frmdplusg.p	$⊢ \underset{˙}{+} = +_{M}$
4	1 2 3	frmdplusg	$⊢ \underset{˙}{+} = {++ ↾}_{(B \times B)}$
5	4	oveqi	$⊢ X \underset{˙}{+} Y = X ({++ ↾}_{(B \times B)}) Y$
6		ovres	$⊢ (X \in B \land Y \in B) \to X ({++ ↾}_{(B \times B)}) Y = X ++ Y$
7	5 6	eqtrid	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X ++ Y$