Metamath Proof Explorer


Theorem efmndcl

Description: The group operation of the monoid of endofunctions on A is closed. (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 efmndcl X B Y B X + ˙ Y B

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 3 efmndov X B Y B X + ˙ Y = X Y
5 1 2 efmndbasf X B X : A A
6 1 2 efmndbasf Y B Y : A A
7 fco X : A A Y : A A X Y : A A
8 5 6 7 syl2an X B Y B X Y : A A
9 coexg X B Y B X Y V
10 1 2 elefmndbas2 X Y V X Y B X Y : A A
11 9 10 syl X B Y B X Y B X Y : A A
12 8 11 mpbird X B Y B X Y B
13 4 12 eqeltrd X B Y B X + ˙ Y B