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 ) )