Metamath Proof Explorer


Theorem ablsub4

Description: Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014)

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

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 eqid
 |-  ( invg ` G ) = ( invg ` G )
15 1 2 14 3 grpsubval
 |-  ( ( ( X .+ Y ) e. B /\ ( Z .+ W ) e. B ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) )
16 9 13 15 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) )
17 ablcmn
 |-  ( G e. Abel -> G e. CMnd )
18 17 3ad2ant1
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. CMnd )
19 simp2
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X e. B /\ Y e. B ) )
20 1 14 grpinvcl
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B )
21 5 10 20 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( invg ` G ) ` Z ) e. B )
22 1 14 grpinvcl
 |-  ( ( G e. Grp /\ W e. B ) -> ( ( invg ` G ) ` W ) e. B )
23 5 11 22 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( invg ` G ) ` W ) e. B )
24 1 2 cmn4
 |-  ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( ( ( invg ` G ) ` Z ) e. B /\ ( ( invg ` G ) ` W ) e. B ) ) -> ( ( X .+ Y ) .+ ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) = ( ( X .+ ( ( invg ` G ) ` Z ) ) .+ ( Y .+ ( ( invg ` G ) ` W ) ) ) )
25 18 19 21 23 24 syl112anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) = ( ( X .+ ( ( invg ` G ) ` Z ) ) .+ ( Y .+ ( ( invg ` G ) ` W ) ) ) )
26 simp1
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. Abel )
27 1 2 14 ablinvadd
 |-  ( ( G e. Abel /\ Z e. B /\ W e. B ) -> ( ( invg ` G ) ` ( Z .+ W ) ) = ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) )
28 26 10 11 27 syl3anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( invg ` G ) ` ( Z .+ W ) ) = ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) )
29 28 oveq2d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) = ( ( X .+ Y ) .+ ( ( ( invg ` G ) ` Z ) .+ ( ( invg ` G ) ` W ) ) ) )
30 1 2 14 3 grpsubval
 |-  ( ( X e. B /\ Z e. B ) -> ( X .- Z ) = ( X .+ ( ( invg ` G ) ` Z ) ) )
31 6 10 30 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .- Z ) = ( X .+ ( ( invg ` G ) ` Z ) ) )
32 1 2 14 3 grpsubval
 |-  ( ( Y e. B /\ W e. B ) -> ( Y .- W ) = ( Y .+ ( ( invg ` G ) ` W ) ) )
33 7 11 32 syl2anc
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y .- W ) = ( Y .+ ( ( invg ` G ) ` W ) ) )
34 31 33 oveq12d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .- Z ) .+ ( Y .- W ) ) = ( ( X .+ ( ( invg ` G ) ` Z ) ) .+ ( Y .+ ( ( invg ` G ) ` W ) ) ) )
35 25 29 34 3eqtr4d
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( ( invg ` G ) ` ( Z .+ W ) ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) )
36 16 35 eqtrd
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) )