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