# Metamath Proof Explorer

## Theorem grplcan

Description: Left cancellation law for groups. (Contributed by NM, 25-Aug-2011)

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

### Proof

Step Hyp Ref Expression
1 grplcan.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 grplcan.p
3 oveq2
5 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
6 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
7 1 2 5 6 grplinv
9 8 oveq1d
10 1 6 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {Z}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
11 10 adantrl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Z}\in {B}\right)\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
12 simprr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
13 simprl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
14 11 12 13 3jca ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({inv}_{g}\left({G}\right)\left({Z}\right)\in {B}\wedge {Z}\in {B}\wedge {X}\in {B}\right)$
15 1 2 grpass
16 14 15 syldan
17 16 anassrs
18 1 2 5 grplid
20 9 17 19 3eqtr3d
24 23 oveq1d
25 10 adantrl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {inv}_{g}\left({G}\right)\left({Z}\right)\in {B}$
26 simprr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
27 simprl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
28 25 26 27 3jca ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({inv}_{g}\left({G}\right)\left({Z}\right)\in {B}\wedge {Z}\in {B}\wedge {Y}\in {B}\right)$
29 1 2 grpass
30 28 29 syldan
31 1 2 5 grplid