Metamath Proof Explorer


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