Theorem abladdsub

Description: Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	|- B = ( Base ` G )
2		ablsubadd.p	|- .+ = ( +g ` G )
3		ablsubadd.m	|- .- = ( -g ` G )
4	1 2	ablcom	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
5	4	3adant3r3	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ Y ) = ( Y .+ X ) )
6	5	oveq1d	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( Y .+ X ) .- Z ) )
7		ablgrp	|- ( G e. Abel -> G e. Grp )
8	7	adantr	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Grp )
9		simpr2	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
10		simpr1	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
11		simpr3	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
12	1 2 3	grpaddsubass	|- ( ( G e. Grp /\ ( Y e. B /\ X e. B /\ Z e. B ) ) -> ( ( Y .+ X ) .- Z ) = ( Y .+ ( X .- Z ) ) )
13	8 9 10 11 12	syl13anc	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .+ X ) .- Z ) = ( Y .+ ( X .- Z ) ) )
14		simpl	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Abel )
15	1 3	grpsubcl	|- ( ( G e. Grp /\ X e. B /\ Z e. B ) -> ( X .- Z ) e. B )
16	8 10 11 15	syl3anc	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .- Z ) e. B )
17	1 2	ablcom	|- ( ( G e. Abel /\ Y e. B /\ ( X .- Z ) e. B ) -> ( Y .+ ( X .- Z ) ) = ( ( X .- Z ) .+ Y ) )
18	14 9 16 17	syl3anc	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .+ ( X .- Z ) ) = ( ( X .- Z ) .+ Y ) )
19	6 13 18	3eqtrd	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( X .- Z ) .+ Y ) )