Theorem 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	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmndplusg.b	$$⊢B={\mathrm{Base}}_G$$
	efmndplusg.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	efmndov	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		efmndplusg.b	$$⊢B={\mathrm{Base}}_G$$
3		efmndplusg.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		coexg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in \mathrm{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{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$
8	5 6 7	ovmpog	$$⊢\left(X\in B\wedge Y\in B\wedge X\circ Y\in \mathrm{V}\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$
9	4 8	mpd3an3	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$