Theorem grpsubval

Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	grpsubval.b	|- B = ( Base ` G )
	grpsubval.p	|- .+ = ( +g ` G )
	grpsubval.i	|- I = ( invg ` G )
	grpsubval.m	|- .- = ( -g ` G )
Assertion	grpsubval	|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( I ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpsubval.b	|- B = ( Base ` G )
2		grpsubval.p	|- .+ = ( +g ` G )
3		grpsubval.i	|- I = ( invg ` G )
4		grpsubval.m	|- .- = ( -g ` G )
5		oveq1	|- ( x = X -> ( x .+ ( I ` y ) ) = ( X .+ ( I ` y ) ) )
6		fveq2	|- ( y = Y -> ( I ` y ) = ( I ` Y ) )
7	6	oveq2d	|- ( y = Y -> ( X .+ ( I ` y ) ) = ( X .+ ( I ` Y ) ) )
8	1 2 3 4	grpsubfval	|- .- = ( x e. B , y e. B |-> ( x .+ ( I ` y ) ) )
9		ovex	|- ( X .+ ( I ` Y ) ) e. _V
10	5 7 8 9	ovmpo	|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( I ` Y ) ) )