# Metamath Proof Explorer

## Theorem grpoinveu

Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of Herstein p. 55. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpoinveu.1 ${⊢}{X}=\mathrm{ran}{G}$
grpoinveu.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
Assertion grpoinveu ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \exists !{y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$

### Proof

Step Hyp Ref Expression
1 grpoinveu.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpoinveu.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
3 1 2 grpoidinv2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left(\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$
4 simpl ${⊢}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\to {y}{G}{A}={U}$
5 4 reximi ${⊢}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
6 5 adantl ${⊢}\left(\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
7 3 6 syl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
8 eqtr3 ${⊢}\left({y}{G}{A}={U}\wedge {z}{G}{A}={U}\right)\to {y}{G}{A}={z}{G}{A}$
9 1 grporcan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {z}\in {X}\wedge {A}\in {X}\right)\right)\to \left({y}{G}{A}={z}{G}{A}↔{y}={z}\right)$
10 8 9 syl5ib ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {z}\in {X}\wedge {A}\in {X}\right)\right)\to \left(\left({y}{G}{A}={U}\wedge {z}{G}{A}={U}\right)\to {y}={z}\right)$
11 10 3exp2 ${⊢}{G}\in \mathrm{GrpOp}\to \left({y}\in {X}\to \left({z}\in {X}\to \left({A}\in {X}\to \left(\left({y}{G}{A}={U}\wedge {z}{G}{A}={U}\right)\to {y}={z}\right)\right)\right)\right)$
12 11 com24 ${⊢}{G}\in \mathrm{GrpOp}\to \left({A}\in {X}\to \left({z}\in {X}\to \left({y}\in {X}\to \left(\left({y}{G}{A}={U}\wedge {z}{G}{A}={U}\right)\to {y}={z}\right)\right)\right)\right)$
13 12 imp41 ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {z}\in {X}\right)\wedge {y}\in {X}\right)\to \left(\left({y}{G}{A}={U}\wedge {z}{G}{A}={U}\right)\to {y}={z}\right)$
14 13 an32s ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to \left(\left({y}{G}{A}={U}\wedge {z}{G}{A}={U}\right)\to {y}={z}\right)$
15 14 expd ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to \left({y}{G}{A}={U}\to \left({z}{G}{A}={U}\to {y}={z}\right)\right)$
16 15 ralrimdva ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({y}{G}{A}={U}\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}{G}{A}={U}\to {y}={z}\right)\right)$
17 16 ancld ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({y}{G}{A}={U}\to \left({y}{G}{A}={U}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}{G}{A}={U}\to {y}={z}\right)\right)\right)$
18 17 reximdva ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}{G}{A}={U}\to {y}={z}\right)\right)\right)$
19 7 18 mpd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}{G}{A}={U}\to {y}={z}\right)\right)$
20 oveq1 ${⊢}{y}={z}\to {y}{G}{A}={z}{G}{A}$
21 20 eqeq1d ${⊢}{y}={z}\to \left({y}{G}{A}={U}↔{z}{G}{A}={U}\right)$
22 21 reu8 ${⊢}\exists !{y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({z}{G}{A}={U}\to {y}={z}\right)\right)$
23 19 22 sylibr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \exists !{y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$