# Metamath Proof Explorer

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

Ref Expression
Hypotheses grpsubadd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$

### Proof

Step Hyp Ref Expression
1 grpsubadd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
4 simpl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {G}\in \mathrm{Grp}$
5 simpr1 ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
6 simpr2 ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
7 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
8 1 7 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {Z}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
9 8 3ad2antr3 ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
10 1 2 grpass
11 4 5 6 9 10 syl13anc
12 1 2 grpcl
14 simpr3 ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$