# Metamath Proof Explorer

## Theorem grpsubf

Description: Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses grpsubcl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
grpsubcl.m
Assertion grpsubf

### Proof

Step Hyp Ref Expression
1 grpsubcl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 grpsubcl.m
3 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
4 1 3 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {y}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
5 4 3adant2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
6 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
7 1 6 grpcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {x}\in {B}\wedge {inv}_{g}\left({G}\right)\left({y}\right)\in {B}\right)\to {x}{+}_{{G}}{inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
8 5 7 syld3an3 ${⊢}\left({G}\in \mathrm{Grp}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to {x}{+}_{{G}}{inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
9 8 3expb ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{G}}{inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
10 9 ralrimivva ${⊢}{G}\in \mathrm{Grp}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
11 1 6 3 2 grpsubfval
12 11 fmpo
13 10 12 sylib