This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝐴 ∈ 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 ⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )