Theorem plusffn

Description: The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015)

	Ref	Expression
Hypotheses	plusffn.1	|- B = ( Base ` G )
	plusffn.2	|- .+^ = ( +f ` G )
Assertion	plusffn	|- .+^ Fn ( B X. B )

Proof

Step	Hyp	Ref	Expression
1		plusffn.1	|- B = ( Base ` G )
2		plusffn.2	|- .+^ = ( +f ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4	1 3 2	plusffval	|- .+^ = ( x e. B , y e. B |-> ( x ( +g ` G ) y ) )
5		ovex	|- ( x ( +g ` G ) y ) e. _V
6	4 5	fnmpoi	|- .+^ Fn ( B X. B )