Theorem grpsubinv

Description: Subtraction of an inverse. (Contributed by NM, 7-Apr-2015)

	Ref	Expression
Hypotheses	grpsubinv.b	|- B = ( Base ` G )
	grpsubinv.p	|- .+ = ( +g ` G )
	grpsubinv.m	|- .- = ( -g ` G )
	grpsubinv.n	|- N = ( invg ` G )
	grpsubinv.g	|- ( ph -> G e. Grp )
	grpsubinv.x	|- ( ph -> X e. B )
	grpsubinv.y	|- ( ph -> Y e. B )
Assertion	grpsubinv	|- ( ph -> ( X .- ( N ` Y ) ) = ( X .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		grpsubinv.b	|- B = ( Base ` G )
2		grpsubinv.p	|- .+ = ( +g ` G )
3		grpsubinv.m	|- .- = ( -g ` G )
4		grpsubinv.n	|- N = ( invg ` G )
5		grpsubinv.g	|- ( ph -> G e. Grp )
6		grpsubinv.x	|- ( ph -> X e. B )
7		grpsubinv.y	|- ( ph -> Y e. B )
8	1 4	grpinvcl	|- ( ( G e. Grp /\ Y e. B ) -> ( N ` Y ) e. B )
9	5 7 8	syl2anc	|- ( ph -> ( N ` Y ) e. B )
10	1 2 4 3	grpsubval	|- ( ( X e. B /\ ( N ` Y ) e. B ) -> ( X .- ( N ` Y ) ) = ( X .+ ( N ` ( N ` Y ) ) ) )
11	6 9 10	syl2anc	|- ( ph -> ( X .- ( N ` Y ) ) = ( X .+ ( N ` ( N ` Y ) ) ) )
12	1 4	grpinvinv	|- ( ( G e. Grp /\ Y e. B ) -> ( N ` ( N ` Y ) ) = Y )
13	5 7 12	syl2anc	|- ( ph -> ( N ` ( N ` Y ) ) = Y )
14	13	oveq2d	|- ( ph -> ( X .+ ( N ` ( N ` Y ) ) ) = ( X .+ Y ) )
15	11 14	eqtrd	|- ( ph -> ( X .- ( N ` Y ) ) = ( X .+ Y ) )