Metamath Proof Explorer


Theorem plusfval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses plusffval.1
|- B = ( Base ` G )
plusffval.2
|- .+ = ( +g ` G )
plusffval.3
|- .+^ = ( +f ` G )
Assertion plusfval
|- ( ( X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )

Proof

Step Hyp Ref Expression
1 plusffval.1
 |-  B = ( Base ` G )
2 plusffval.2
 |-  .+ = ( +g ` G )
3 plusffval.3
 |-  .+^ = ( +f ` G )
4 oveq12
 |-  ( ( x = X /\ y = Y ) -> ( x .+ y ) = ( X .+ Y ) )
5 1 2 3 plusffval
 |-  .+^ = ( x e. B , y e. B |-> ( x .+ y ) )
6 ovex
 |-  ( X .+ Y ) e. _V
7 4 5 6 ovmpoa
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )