Theorem efmndplusg

Description: The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024)

	Ref	Expression
Hypotheses	efmndtset.g	$$⊢G=\mathrm{EndoFMnd}\left(A\right)$$
	efmndplusg.b	$$⊢B={\mathrm{Base}}_G$$
	efmndplusg.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	efmndplusg	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	$$⊢G=\mathrm{EndoFMnd}\left(A\right)$$
2		efmndplusg.b	$$⊢B={\mathrm{Base}}_G$$
3		efmndplusg.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4	1 2	efmndbas	$$⊢B=A^A$$
5		eqid	$$⊢\left(f\in B,g\in B⟼f\circ g\right)=\left(f\in B,g\in B⟼f\circ g\right)$$
6		eqid	$$⊢{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
7	1 4 5 6	efmnd	$$⊢A\in \mathrm{V}\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(f\in B,g\in B⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}$$
8	7	fveq2d	$$⊢A\in \mathrm{V}\to {+}_G={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(f\in B,g\in B⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}}$$
9	2	fvexi	$$⊢B\in \mathrm{V}$$
10	9 9	mpoex	$$⊢\left(f\in B,g\in B⟼f\circ g\right)\in \mathrm{V}$$
11		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(f\in B,g\in B⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(f\in B,g\in B⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}$$
12	11	topgrpplusg	$$⊢\left(f\in B,g\in B⟼f\circ g\right)\in \mathrm{V}\to \left(f\in B,g\in B⟼f\circ g\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(f\in B,g\in B⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}}$$
13	10 12	ax-mp	$$⊢\left(f\in B,g\in B⟼f\circ g\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(f\in B,g\in B⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)⟩\right\}}$$
14	8 3 13	3eqtr4g	$$⊢A\in \mathrm{V}\to \underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$
15		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{EndoFMnd}\left(A\right)=\varnothing$$
16	1 15	eqtrid	$$⊢\neg A\in \mathrm{V}\to G=\varnothing$$
17	16	fveq2d	$$⊢\neg A\in \mathrm{V}\to {+}_G={+}_{\varnothing }$$
18		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
19	18	str0	$$⊢\varnothing ={+}_{\varnothing }$$
20	17 3 19	3eqtr4g	$$⊢\neg A\in \mathrm{V}\to \underset{\dot{}}{+}=\varnothing$$
21	16	fveq2d	$$⊢\neg A\in \mathrm{V}\to {\mathrm{Base}}_G={\mathrm{Base}}_{\varnothing }$$
22		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
23	21 2 22	3eqtr4g	$$⊢\neg A\in \mathrm{V}\to B=\varnothing$$
24	23	olcd	$$⊢\neg A\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
25		0mpo0	$$⊢\left(B=\varnothing \vee B=\varnothing \right)\to \left(f\in B,g\in B⟼f\circ g\right)=\varnothing$$
26	24 25	syl	$$⊢\neg A\in \mathrm{V}\to \left(f\in B,g\in B⟼f\circ g\right)=\varnothing$$
27	20 26	eqtr4d	$$⊢\neg A\in \mathrm{V}\to \underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$
28	14 27	pm2.61i	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$