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