# Metamath Proof Explorer

## Theorem grpinvid2

Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011)

Ref Expression
Hypotheses grpinv.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
grpinv.p
grpinv.u
grpinv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
Assertion grpinvid2

### Proof

Step Hyp Ref Expression
1 grpinv.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 grpinv.p
3 grpinv.u
4 grpinv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
5 oveq1
7 1 2 3 4 grplinv
10 6 9 eqtr3d
11 1 4 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {N}\left({X}\right)\in {B}$
12 1 2 3 grplid
13 11 12 syldan
15 14 eqcomd
17 oveq1
19 simprr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
20 simprl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
21 11 adantrr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {N}\left({X}\right)\in {B}$
22 19 20 21 3jca ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({Y}\in {B}\wedge {X}\in {B}\wedge {N}\left({X}\right)\in {B}\right)$
23 1 2 grpass
24 22 23 syldan
25 24 3impb
26 1 2 3 4 grprinv
27 26 oveq2d
29 1 2 3 grprid
31 25 28 30 3eqtrd