This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpsubadd

Description: Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpsubadd.b 
|- B = ( Base ` G )
grpsubadd.p 
|- .+ = ( +g ` G )
grpsubadd.m 
|- .- = ( -g ` G )
Assertion grpsubadd 
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Z .+ 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 2 4 3 grpsubval 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
6 5 3adant3 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
7 6 adantl 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
8 7 eqeq1d 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( X .+ ( ( invg ` G ) ` Y ) ) = Z ) )
9 simpl 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Grp )
10 simpr1 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
11 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
12 11 3ad2antr2 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( invg ` G ) ` Y ) e. B )
13 1 2 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) e. B )
14 9 10 12 13 syl3anc 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( ( invg ` G ) ` Y ) ) e. B )
15 simpr3 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
16 simpr2 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
17 1 2 grprcan 
 |-  ( ( G e. Grp /\ ( ( X .+ ( ( invg ` G ) ` Y ) ) e. B /\ Z e. B /\ Y e. B ) ) -> ( ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ Y ) = ( Z .+ Y ) <-> ( X .+ ( ( invg ` G ) ` Y ) ) = Z ) )
18 9 14 15 16 17 syl13anc 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ Y ) = ( Z .+ Y ) <-> ( X .+ ( ( invg ` G ) ` Y ) ) = Z ) )
19 1 2 grpass 
 |-  ( ( G e. Grp /\ ( X e. B /\ ( ( invg ` G ) ` Y ) e. B /\ Y e. B ) ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ Y ) = ( X .+ ( ( ( invg ` G ) ` Y ) .+ Y ) ) )
20 9 10 12 16 19 syl13anc 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ Y ) = ( X .+ ( ( ( invg ` G ) ` Y ) .+ Y ) ) )
21 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
22 1 2 21 4 grplinv 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( ( invg ` G ) ` Y ) .+ Y ) = ( 0g ` G ) )
23 22 3ad2antr2 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Y ) .+ Y ) = ( 0g ` G ) )
24 23 oveq2d 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( ( ( invg ` G ) ` Y ) .+ Y ) ) = ( X .+ ( 0g ` G ) ) )
25 1 2 21 grprid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( 0g ` G ) ) = X )
26 25 3ad2antr1 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( 0g ` G ) ) = X )
27 20 24 26 3eqtrd 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ Y ) = X )
28 27 eqeq1d 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ Y ) = ( Z .+ Y ) <-> X = ( Z .+ Y ) ) )
29 8 18 28 3bitr2d 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> X = ( Z .+ Y ) ) )
30 eqcom 
 |-  ( X = ( Z .+ Y ) <-> ( Z .+ Y ) = X )
31 29 30 bitrdi 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Z .+ Y ) = X ) )