efmndov

Description: The value of the group operation of the monoid of endofunctions on A . (Contributed by AV, 27-Jan-2024)

	Ref	Expression
Hypotheses	efmndtset.g	$⊢ G = EndoFMnd (A)$
	efmndplusg.b	$⊢ B = {Base}_{G}$
	efmndplusg.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	efmndov	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X \circ Y$

Step	Hyp	Ref	Expression
1		efmndtset.g	$⊢ G = EndoFMnd (A)$
2		efmndplusg.b	$⊢ B = {Base}_{G}$
3		efmndplusg.p	$⊢ \underset{˙}{+} = +_{G}$
4		coexg	$⊢ (X \in B \land Y \in B) \to X \circ Y \in V$
5		coeq1	$⊢ f = X \to f \circ g = X \circ g$
6		coeq2	$⊢ g = Y \to X \circ g = X \circ Y$
7	1 2 3	efmndplusg	$⊢ \underset{˙}{+} = (f \in B, g \in B ⟼ f \circ g)$
8	5 6 7	ovmpog	$⊢ (X \in B \land Y \in B \land X \circ Y \in V) \to X \underset{˙}{+} Y = X \circ Y$
9	4 8	mpd3an3	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X \circ Y$

Metamath Proof Explorer