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	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
	efmndplusg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	efmndplusg.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	efmndplusg	⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2		efmndplusg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		efmndplusg.p	⊢ + = ( +g ‘ 𝐺 )
4	1 2	efmndbas	⊢ 𝐵 = ( 𝐴 ↑m 𝐴 )
5		eqid	⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )
6		eqid	⊢ ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
7	1 4 5 6	efmnd	⊢ ( 𝐴 ∈ V → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
8	7	fveq2d	⊢ ( 𝐴 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
9	2	fvexi	⊢ 𝐵 ∈ V
10	9 9	mpoex	⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V
11		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ }
12	11	topgrpplusg	⊢ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
13	10 12	ax-mp	⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
14	8 3 13	3eqtr4g	⊢ ( 𝐴 ∈ V → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) )
15		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ )
16	1 15	syl5eq	⊢ ( ¬ 𝐴 ∈ V → 𝐺 = ∅ )
17	16	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ ∅ ) )
18		plusgid	⊢ +g = Slot ( +g ‘ ndx )
19	18	str0	⊢ ∅ = ( +g ‘ ∅ )
20	17 3 19	3eqtr4g	⊢ ( ¬ 𝐴 ∈ V → + = ∅ )
21	16	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
22		base0	⊢ ∅ = ( Base ‘ ∅ )
23	21 2 22	3eqtr4g	⊢ ( ¬ 𝐴 ∈ V → 𝐵 = ∅ )
24	23	olcd	⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
25		0mpo0	⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ∅ )
26	24 25	syl	⊢ ( ¬ 𝐴 ∈ V → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ∅ )
27	20 26	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) )
28	14 27	pm2.61i	⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )