# Metamath Proof Explorer

## Theorem grpinvid1

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 grpinvid1

### 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 oveq2
7 1 2 3 4 grprinv
10 6 9 eqtr3d
11 oveq2
13 1 2 3 4 grplinv
14 13 oveq1d
16 1 4 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {N}\left({X}\right)\in {B}$
17 16 adantrr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {N}\left({X}\right)\in {B}$
18 simprl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
19 simprr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
20 17 18 19 3jca ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({N}\left({X}\right)\in {B}\wedge {X}\in {B}\wedge {Y}\in {B}\right)$
21 1 2 grpass
22 20 21 syldan
23 22 3impb
24 15 23 eqtr3d
25 1 2 3 grplid