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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
efmndplusg.b B = Base G
efmndplusg.p + ˙ = + G
Assertion efmndplusg + ˙ = f B , g B f g

Proof

Step Hyp Ref Expression
1 efmndtset.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 efmndplusg.b B = Base G
3 efmndplusg.p + ˙ = + G
4 1 2 efmndbas B = A A
5 eqid f B , g B f g = f B , g B f g
6 eqid 𝑡 A × 𝒫 A = 𝑡 A × 𝒫 A
7 1 4 5 6 efmnd A V G = Base ndx B + ndx f B , g B f g TopSet ndx 𝑡 A × 𝒫 A
8 7 fveq2d A V + G = + Base ndx B + ndx f B , g B f g TopSet ndx 𝑡 A × 𝒫 A
9 2 fvexi B V
10 9 9 mpoex f B , g B f g V
11 eqid Base ndx B + ndx f B , g B f g TopSet ndx 𝑡 A × 𝒫 A = Base ndx B + ndx f B , g B f g TopSet ndx 𝑡 A × 𝒫 A
12 11 topgrpplusg f B , g B f g V f B , g B f g = + Base ndx B + ndx f B , g B f g TopSet ndx 𝑡 A × 𝒫 A
13 10 12 ax-mp f B , g B f g = + Base ndx B + ndx f B , g B f g TopSet ndx 𝑡 A × 𝒫 A
14 8 3 13 3eqtr4g A V + ˙ = f B , g B f g
15 fvprc Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) with typecode |-
16 1 15 syl5eq ¬ A V G =
17 16 fveq2d ¬ A V + G = +
18 plusgid + 𝑔 = Slot + ndx
19 18 str0 = +
20 17 3 19 3eqtr4g ¬ A V + ˙ =
21 16 fveq2d ¬ A V Base G = Base
22 base0 = Base
23 21 2 22 3eqtr4g ¬ A V B =
24 23 olcd ¬ A V B = B =
25 0mpo0 B = B = f B , g B f g =
26 24 25 syl ¬ A V f B , g B f g =
27 20 26 eqtr4d ¬ A V + ˙ = f B , g B f g
28 14 27 pm2.61i + ˙ = f B , g B f g