efmndmnd

Description: The monoid of endofunctions on a set A is actually a monoid. (Contributed by AV, 31-Jan-2024)

		Ref	Expression
	Hypothesis	ielefmnd.g	No typesetting found for \|- G = ( EndoFMnd ` A ) with typecode \|-
	Assertion	efmndmnd	$⊢ A \in V \to G \in Mnd$

Proof

Step	Hyp	Ref	Expression
1		ielefmnd.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for \|- G = ( EndoFMnd ` A ) with typecode \|-
2	1	efmndsgrp	Could not format G e. Smgrp : No typesetting found for \|- G e. Smgrp with typecode \|-
3	2	a1i	Could not format ( A e. V -> G e. Smgrp ) : No typesetting found for \|- ( A e. V -> G e. Smgrp ) with typecode \|-
4	1	ielefmnd	$⊢ A \in V \to {I ↾}_{A} \in {Base}_{G}$
5		oveq1	$⊢ i = {I ↾}_{A} \to i +_{G} f = ({I ↾}_{A}) +_{G} f$
6	5	eqeq1d	$⊢ i = {I ↾}_{A} \to (i +_{G} f = f \leftrightarrow ({I ↾}_{A}) +_{G} f = f)$
7		oveq2	$⊢ i = {I ↾}_{A} \to f +_{G} i = f +_{G} ({I ↾}_{A})$
8	7	eqeq1d	$⊢ i = {I ↾}_{A} \to (f +_{G} i = f \leftrightarrow f +_{G} ({I ↾}_{A}) = f)$
9	6 8	anbi12d	$⊢ i = {I ↾}_{A} \to ((i +_{G} f = f \land f +_{G} i = f) \leftrightarrow (({I ↾}_{A}) +_{G} f = f \land f +_{G} ({I ↾}_{A}) = f))$
10	9	ralbidv	$⊢ i = {I ↾}_{A} \to (\forall f \in {Base}_{G} (i +_{G} f = f \land f +_{G} i = f) \leftrightarrow \forall f \in {Base}_{G} (({I ↾}_{A}) +_{G} f = f \land f +_{G} ({I ↾}_{A}) = f))$
11	10	adantl	$⊢ (A \in V \land i = {I ↾}_{A}) \to (\forall f \in {Base}_{G} (i +_{G} f = f \land f +_{G} i = f) \leftrightarrow \forall f \in {Base}_{G} (({I ↾}_{A}) +_{G} f = f \land f +_{G} ({I ↾}_{A}) = f))$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13	1 12	efmndbasf	$⊢ f \in {Base}_{G} \to f : A ⟶ A$
14	13	adantl	$⊢ (A \in V \land f \in {Base}_{G}) \to f : A ⟶ A$
15		fcoi2	$⊢ f : A ⟶ A \to ({I ↾}_{A}) \circ f = f$
16		fcoi1	$⊢ f : A ⟶ A \to f \circ ({I ↾}_{A}) = f$
17	15 16	jca	$⊢ f : A ⟶ A \to (({I ↾}_{A}) \circ f = f \land f \circ ({I ↾}_{A}) = f)$
18	14 17	syl	$⊢ (A \in V \land f \in {Base}_{G}) \to (({I ↾}_{A}) \circ f = f \land f \circ ({I ↾}_{A}) = f)$
19		eqid	$⊢ +_{G} = +_{G}$
20	1 12 19	efmndov	$⊢ ({I ↾}_{A} \in {Base}_{G} \land f \in {Base}_{G}) \to ({I ↾}_{A}) +_{G} f = ({I ↾}_{A}) \circ f$
21	4 20	sylan	$⊢ (A \in V \land f \in {Base}_{G}) \to ({I ↾}_{A}) +_{G} f = ({I ↾}_{A}) \circ f$
22	21	eqeq1d	$⊢ (A \in V \land f \in {Base}_{G}) \to (({I ↾}_{A}) +_{G} f = f \leftrightarrow ({I ↾}_{A}) \circ f = f)$
23	4	anim1ci	$⊢ (A \in V \land f \in {Base}_{G}) \to (f \in {Base}_{G} \land {I ↾}_{A} \in {Base}_{G})$
24	1 12 19	efmndov	$⊢ (f \in {Base}_{G} \land {I ↾}_{A} \in {Base}_{G}) \to f +_{G} ({I ↾}_{A}) = f \circ ({I ↾}_{A})$
25	23 24	syl	$⊢ (A \in V \land f \in {Base}_{G}) \to f +_{G} ({I ↾}_{A}) = f \circ ({I ↾}_{A})$
26	25	eqeq1d	$⊢ (A \in V \land f \in {Base}_{G}) \to (f +_{G} ({I ↾}_{A}) = f \leftrightarrow f \circ ({I ↾}_{A}) = f)$
27	22 26	anbi12d	$⊢ (A \in V \land f \in {Base}_{G}) \to ((({I ↾}_{A}) +_{G} f = f \land f +_{G} ({I ↾}_{A}) = f) \leftrightarrow (({I ↾}_{A}) \circ f = f \land f \circ ({I ↾}_{A}) = f))$
28	18 27	mpbird	$⊢ (A \in V \land f \in {Base}_{G}) \to (({I ↾}_{A}) +_{G} f = f \land f +_{G} ({I ↾}_{A}) = f)$
29	28	ralrimiva	$⊢ A \in V \to \forall f \in {Base}_{G} (({I ↾}_{A}) +_{G} f = f \land f +_{G} ({I ↾}_{A}) = f)$
30	4 11 29	rspcedvd	$⊢ A \in V \to \exists i \in {Base}_{G} \forall f \in {Base}_{G} (i +_{G} f = f \land f +_{G} i = f)$
31	12 19	ismnddef	Could not format ( G e. Mnd <-> ( G e. Smgrp /\ E. i e. ( Base ` G ) A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) ) ) : No typesetting found for \|- ( G e. Mnd <-> ( G e. Smgrp /\ E. i e. ( Base ` G ) A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) ) ) with typecode \|-
32	3 30 31	sylanbrc	$⊢ A \in V \to G \in Mnd$

Metamath Proof Explorer

Theorem efmndmnd

Proof