Metamath Proof Explorer

Theorem ablsubaddsub

Description: Double subtraction and addition in abelian groups. ( cnambpcma analog.) (Contributed by AV, 3-Mar-2025)

Ref Expression
Hypotheses ablsubadd.b 
|- B = ( Base ` G )
ablsubadd.p 
|- .+ = ( +g ` G )
ablsubadd.m 
|- .- = ( -g ` G )
Assertion ablsubaddsub 
|- ( ( 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 3 ablsubadd23 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) .+ Z ) = ( X .+ ( Z .- Y ) ) )
5 4 oveq1d 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( X .- Y ) .+ Z ) .- X ) = ( ( X .+ ( Z .- Y ) ) .- X ) )
6 simpl 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Abel )
7 simpr1 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
8 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
9 8 adantr 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> G e. Grp )
10 simpr3 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
11 simpr2 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
12 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ Z e. B /\ Y e. B ) -> ( Z .- Y ) e. B )
13 9 10 11 12 syl3anc 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Z .- Y ) e. B )
14 1 2 ablcom 
 |-  ( ( G e. Abel /\ X e. B /\ ( Z .- Y ) e. B ) -> ( X .+ ( Z .- Y ) ) = ( ( Z .- Y ) .+ X ) )
15 6 7 13 14 syl3anc 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( Z .- Y ) ) = ( ( Z .- Y ) .+ X ) )
16 15 oveq1d 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ ( Z .- Y ) ) .- X ) = ( ( ( Z .- Y ) .+ X ) .- X ) )
17 1 2 3 grpaddsubass 
 |-  ( ( G e. Grp /\ ( ( Z .- Y ) e. B /\ X e. B /\ X e. B ) ) -> ( ( ( Z .- Y ) .+ X ) .- X ) = ( ( Z .- Y ) .+ ( X .- X ) ) )
18 9 13 7 7 17 syl13anc 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( Z .- Y ) .+ X ) .- X ) = ( ( Z .- Y ) .+ ( X .- X ) ) )
19 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
20 1 19 3 grpsubid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .- X ) = ( 0g ` G ) )
21 9 7 20 syl2anc 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .- X ) = ( 0g ` G ) )
22 21 oveq2d 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .- Y ) .+ ( X .- X ) ) = ( ( Z .- Y ) .+ ( 0g ` G ) ) )
23 1 2 19 9 13 grpridd 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .- Y ) .+ ( 0g ` G ) ) = ( Z .- Y ) )
24 18 22 23 3eqtrd 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( Z .- Y ) .+ X ) .- X ) = ( Z .- Y ) )
25 5 16 24 3eqtrd 
 |-  ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( X .- Y ) .+ Z ) .- X ) = ( Z .- Y ) )