Theorem ablsubadd23

Description: Commutative/associative law for addition and subtraction in abelian groups. ( subadd23d analog.) (Contributed by AV, 2-Mar-2025)

	Ref	Expression
Hypotheses	ablsubadd.b	|- B = ( Base ` G )
	ablsubadd.p	|- .+ = ( +g ` G )
	ablsubadd.m	|- .- = ( -g ` G )
Assertion	ablsubadd23	|- ( ( 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		3ancomb	|- ( ( X e. B /\ Y e. B /\ Z e. B ) <-> ( X e. B /\ Z e. B /\ Y e. B ) )
5	4	biimpi	|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X e. B /\ Z e. B /\ Y e. B ) )
6	1 2 3	abladdsub	|- ( ( G e. Abel /\ ( X e. B /\ Z e. B /\ Y e. B ) ) -> ( ( X .+ Z ) .- Y ) = ( ( X .- Y ) .+ Z ) )
7	5 6	sylan2	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) .- Y ) = ( ( X .- Y ) .+ Z ) )
8		ablgrp	|- ( G e. Abel -> G e. Grp )
9	1 2 3	grpaddsubass	|- ( ( G e. Grp /\ ( X e. B /\ Z e. B /\ Y e. B ) ) -> ( ( X .+ Z ) .- Y ) = ( X .+ ( Z .- Y ) ) )
10	8 5 9	syl2an	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Z ) .- Y ) = ( X .+ ( Z .- Y ) ) )
11	7 10	eqtr3d	|- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) .+ Z ) = ( X .+ ( Z .- Y ) ) )