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

Metamath Proof Explorer

Theorem efmndov

Description: The value of the group operation of the monoid of endofunctions on A . (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndtset.g 
|- G = ( EndoFMnd ` A )
efmndplusg.b 
|- B = ( Base ` G )
efmndplusg.p 
|- .+ = ( +g ` G )
Assertion efmndov 
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )

Proof

Step Hyp Ref Expression
1 efmndtset.g 
 |-  G = ( EndoFMnd ` A )
2 efmndplusg.b 
 |-  B = ( Base ` G )
3 efmndplusg.p 
 |-  .+ = ( +g ` G )
4 coexg 
 |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )
5 coeq1 
 |-  ( f = X -> ( f o. g ) = ( X o. g ) )
6 coeq2 
 |-  ( g = Y -> ( X o. g ) = ( X o. Y ) )
7 1 2 3 efmndplusg 
 |-  .+ = ( f e. B , g e. B |-> ( f o. g ) )
8 5 6 7 ovmpog 
 |-  ( ( X e. B /\ Y e. B /\ ( X o. Y ) e. _V ) -> ( X .+ Y ) = ( X o. Y ) )
9 4 8 mpd3an3 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )