Metamath Proof Explorer


Theorem abladdsub4

Description: Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses ablsubadd.b
|- B = ( Base ` G )
ablsubadd.p
|- .+ = ( +g ` G )
ablsubadd.m
|- .- = ( -g ` G )
Assertion abladdsub4
|- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) = ( Z .+ W ) <-> ( X .- Z ) = ( W .- Y ) ) )

Proof

Step Hyp Ref Expression
1 ablsubadd.b
 |-  B = ( Base ` G )
2 ablsubadd.p
 |-  .+ = ( +g ` G )
3 ablsubadd.m
 |-  .- = ( -g ` G )
4 ablgrp
 |-  ( G e. Abel -> G e. Grp )
5 4 3ad2ant1
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. Grp )
6 simp2l
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> X e. B )
7 simp2r
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Y e. B )
8 1 2 grpcl
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
9 5 6 7 8 syl3anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .+ Y ) e. B )
10 simp3l
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Z e. B )
11 simp3r
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> W e. B )
12 1 2 grpcl
 |-  ( ( G e. Grp /\ Z e. B /\ W e. B ) -> ( Z .+ W ) e. B )
13 5 10 11 12 syl3anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z .+ W ) e. B )
14 1 2 grpcl
 |-  ( ( G e. Grp /\ Z e. B /\ Y e. B ) -> ( Z .+ Y ) e. B )
15 5 10 7 14 syl3anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z .+ Y ) e. B )
16 1 3 grpsubrcan
 |-  ( ( G e. Grp /\ ( ( X .+ Y ) e. B /\ ( Z .+ W ) e. B /\ ( Z .+ Y ) e. B ) ) -> ( ( ( X .+ Y ) .- ( Z .+ Y ) ) = ( ( Z .+ W ) .- ( Z .+ Y ) ) <-> ( X .+ Y ) = ( Z .+ W ) ) )
17 5 9 13 15 16 syl13anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( ( X .+ Y ) .- ( Z .+ Y ) ) = ( ( Z .+ W ) .- ( Z .+ Y ) ) <-> ( X .+ Y ) = ( Z .+ W ) ) )
18 simp1
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. Abel )
19 1 2 3 ablsub4
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ Y e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ Y ) ) = ( ( X .- Z ) .+ ( Y .- Y ) ) )
20 18 6 7 10 7 19 syl122anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ Y ) ) = ( ( X .- Z ) .+ ( Y .- Y ) ) )
21 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
22 1 21 3 grpsubid
 |-  ( ( G e. Grp /\ Y e. B ) -> ( Y .- Y ) = ( 0g ` G ) )
23 5 7 22 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y .- Y ) = ( 0g ` G ) )
24 23 oveq2d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .- Z ) .+ ( Y .- Y ) ) = ( ( X .- Z ) .+ ( 0g ` G ) ) )
25 1 3 grpsubcl
 |-  ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( X .- Z ) e. B )
26 5 6 10 25 syl3anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .- Z ) e. B )
27 1 2 21 grprid
 |-  ( ( G e. Grp /\ ( X .- Z ) e. B ) -> ( ( X .- Z ) .+ ( 0g ` G ) ) = ( X .- Z ) )
28 5 26 27 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .- Z ) .+ ( 0g ` G ) ) = ( X .- Z ) )
29 20 24 28 3eqtrd
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ Y ) ) = ( X .- Z ) )
30 1 2 3 ablsub4
 |-  ( ( G e. Abel /\ ( Z e. B /\ W e. B ) /\ ( Z e. B /\ Y e. B ) ) -> ( ( Z .+ W ) .- ( Z .+ Y ) ) = ( ( Z .- Z ) .+ ( W .- Y ) ) )
31 18 10 11 10 7 30 syl122anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( Z .+ W ) .- ( Z .+ Y ) ) = ( ( Z .- Z ) .+ ( W .- Y ) ) )
32 1 21 3 grpsubid
 |-  ( ( G e. Grp /\ Z e. B ) -> ( Z .- Z ) = ( 0g ` G ) )
33 5 10 32 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z .- Z ) = ( 0g ` G ) )
34 33 oveq1d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( Z .- Z ) .+ ( W .- Y ) ) = ( ( 0g ` G ) .+ ( W .- Y ) ) )
35 1 3 grpsubcl
 |-  ( ( G e. Grp /\ W e. B /\ Y e. B ) -> ( W .- Y ) e. B )
36 5 11 7 35 syl3anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( W .- Y ) e. B )
37 1 2 21 grplid
 |-  ( ( G e. Grp /\ ( W .- Y ) e. B ) -> ( ( 0g ` G ) .+ ( W .- Y ) ) = ( W .- Y ) )
38 5 36 37 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( 0g ` G ) .+ ( W .- Y ) ) = ( W .- Y ) )
39 31 34 38 3eqtrd
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( Z .+ W ) .- ( Z .+ Y ) ) = ( W .- Y ) )
40 29 39 eqeq12d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( ( X .+ Y ) .- ( Z .+ Y ) ) = ( ( Z .+ W ) .- ( Z .+ Y ) ) <-> ( X .- Z ) = ( W .- Y ) ) )
41 17 40 bitr3d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) = ( Z .+ W ) <-> ( X .- Z ) = ( W .- Y ) ) )