Theorem plusfeq

Description: If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	plusffval.1	|- B = ( Base ` G )
	plusffval.2	|- .+ = ( +g ` G )
	plusffval.3	|- .+^ = ( +f ` G )
Assertion	plusfeq	|- ( .+ Fn ( B X. B ) -> .+^ = .+ )

Proof

Step	Hyp	Ref	Expression
1		plusffval.1	|- B = ( Base ` G )
2		plusffval.2	|- .+ = ( +g ` G )
3		plusffval.3	|- .+^ = ( +f ` G )
4	1 2 3	plusffval	|- .+^ = ( x e. B , y e. B |-> ( x .+ y ) )
5		fnov	|- ( .+ Fn ( B X. B ) <-> .+ = ( x e. B , y e. B |-> ( x .+ y ) ) )
6	5	biimpi	|- ( .+ Fn ( B X. B ) -> .+ = ( x e. B , y e. B |-> ( x .+ y ) ) )
7	4 6	eqtr4id	|- ( .+ Fn ( B X. B ) -> .+^ = .+ )