Metamath Proof Explorer

Theorem grpnpcan

Description: Cancellation law for subtraction ( npcan analog). (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses grpsubadd.b 
|- B = ( Base ` G )
grpsubadd.p 
|- .+ = ( +g ` G )
grpsubadd.m 
|- .- = ( -g ` G )
Assertion grpnpcan 
|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .- Y ) .+ Y ) = X )

Proof

Step Hyp Ref Expression
1 grpsubadd.b 
 |-  B = ( Base ` G )
2 grpsubadd.p 
 |-  .+ = ( +g ` G )
3 grpsubadd.m 
 |-  .- = ( -g ` G )
4 eqid 
 |-  ( invg ` G ) = ( invg ` G )
5 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
6 5 3adant2 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
7 1 2 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) e. B )
8 6 7 syld3an3 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) e. B )
9 1 2 4 3 grpsubval 
 |-  ( ( ( X .+ ( ( invg ` G ) ` Y ) ) e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) ) )
10 8 6 9 syl2anc 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) ) )
11 1 2 3 grppncan 
 |-  ( ( G e. Grp /\ X e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = X )
12 6 11 syld3an3 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = X )
13 1 2 4 3 grpsubval 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
14 13 3adant1 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
15 14 eqcomd 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) = ( X .- Y ) )
16 1 4 grpinvinv 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) = Y )
17 16 3adant2 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) = Y )
18 15 17 oveq12d 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) ) = ( ( X .- Y ) .+ Y ) )
19 10 12 18 3eqtr3rd 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .- Y ) .+ Y ) = X )