efmndcl

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

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

Step	Hyp	Ref	Expression
1		efmndtset.g	$⊢ G = EndoFMnd (A)$
2		efmndplusg.b	$⊢ B = {Base}_{G}$
3		efmndplusg.p	$⊢ \underset{˙}{+} = +_{G}$
4	1 2 3	efmndov	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X \circ Y$
5	1 2	efmndbasf	$⊢ X \in B \to X : A ⟶ A$
6	1 2	efmndbasf	$⊢ Y \in B \to Y : A ⟶ A$
7		fco	$⊢ (X : A ⟶ A \land Y : A ⟶ A) \to (X \circ Y) : A ⟶ A$
8	5 6 7	syl2an	$⊢ (X \in B \land Y \in B) \to (X \circ Y) : A ⟶ A$
9		coexg	$⊢ (X \in B \land Y \in B) \to X \circ Y \in V$
10	1 2	elefmndbas2	$⊢ X \circ Y \in V \to (X \circ Y \in B \leftrightarrow (X \circ Y) : A ⟶ A)$
11	9 10	syl	$⊢ (X \in B \land Y \in B) \to (X \circ Y \in B \leftrightarrow (X \circ Y) : A ⟶ A)$
12	8 11	mpbird	$⊢ (X \in B \land Y \in B) \to X \circ Y \in B$
13	4 12	eqeltrd	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$

Metamath Proof Explorer