# Metamath Proof Explorer

## Theorem grprcan

Description: Right cancellation law for groups. (Contributed by NM, 24-Aug-2011) (Proof shortened by Mario Carneiro, 6-Jan-2015)

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

### Proof

Step Hyp Ref Expression
1 grprcan.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 grprcan.p
3 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
4 1 2 3 grpinvex
6 simprr
7 6 oveq1d
8 simpll
9 1 2 grpass
10 8 9 sylan
11 simplr1
12 simplr3
13 simprll
14 10 11 12 13 caovassd
15 simplr2
16 10 15 12 13 caovassd
17 7 14 16 3eqtr3d
18 1 2 grpcl
19 8 18 syl3an1
20 1 3 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {B}$
21 8 20 syl
22 1 2 3 grplid
23 8 22 sylan
24 1 2 3 grpinvex
25 8 24 sylan
26 simpr
28 simprlr
30 19 21 23 10 25 26 27 29 grprinvd
31 12 30 mpdan
32 31 oveq2d
33 31 oveq2d
34 17 32 33 3eqtr3d
35 1 2 3 grprid
36 8 11 35 syl2anc
37 1 2 3 grprid
38 8 15 37 syl2anc
39 34 36 38 3eqtr3d
40 39 expr
41 5 40 rexlimddv
42 oveq1
43 41 42 impbid1