# 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 𝑋 = ran 𝐺
grpoinveu.2 𝑈 = ( GId ‘ 𝐺 )
Assertion grpoinveu ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ∃! 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )

### Proof

Step Hyp Ref Expression
1 grpoinveu.1 𝑋 = ran 𝐺
2 grpoinveu.2 𝑈 = ( GId ‘ 𝐺 )
3 1 2 grpoidinv2 ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
4 simpl ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = 𝑈 )
5 4 reximi ( ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ∃ 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
6 5 adantl ( ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) → ∃ 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
7 3 6 syl ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ∃ 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
8 eqtr3 ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = ( 𝑧 𝐺 𝐴 ) )
9 1 grporcan ( ( 𝐺 ∈ GrpOp ∧ ( 𝑦𝑋𝑧𝑋𝐴𝑋 ) ) → ( ( 𝑦 𝐺 𝐴 ) = ( 𝑧 𝐺 𝐴 ) ↔ 𝑦 = 𝑧 ) )
10 8 9 syl5ib ( ( 𝐺 ∈ GrpOp ∧ ( 𝑦𝑋𝑧𝑋𝐴𝑋 ) ) → ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) → 𝑦 = 𝑧 ) )
11 10 3exp2 ( 𝐺 ∈ GrpOp → ( 𝑦𝑋 → ( 𝑧𝑋 → ( 𝐴𝑋 → ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) → 𝑦 = 𝑧 ) ) ) ) )
12 11 com24 ( 𝐺 ∈ GrpOp → ( 𝐴𝑋 → ( 𝑧𝑋 → ( 𝑦𝑋 → ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) → 𝑦 = 𝑧 ) ) ) ) )
13 12 imp41 ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ 𝑧𝑋 ) ∧ 𝑦𝑋 ) → ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) → 𝑦 = 𝑧 ) )
14 13 an32s ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧𝑋 ) → ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) → 𝑦 = 𝑧 ) )
15 14 expd ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 → ( ( 𝑧 𝐺 𝐴 ) = 𝑈𝑦 = 𝑧 ) ) )
16 15 ralrimdva ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 → ∀ 𝑧𝑋 ( ( 𝑧 𝐺 𝐴 ) = 𝑈𝑦 = 𝑧 ) ) )
17 16 ancld ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ∀ 𝑧𝑋 ( ( 𝑧 𝐺 𝐴 ) = 𝑈𝑦 = 𝑧 ) ) ) )
18 17 reximdva ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ( ∃ 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 → ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ∀ 𝑧𝑋 ( ( 𝑧 𝐺 𝐴 ) = 𝑈𝑦 = 𝑧 ) ) ) )
19 7 18 mpd ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ∀ 𝑧𝑋 ( ( 𝑧 𝐺 𝐴 ) = 𝑈𝑦 = 𝑧 ) ) )
20 oveq1 ( 𝑦 = 𝑧 → ( 𝑦 𝐺 𝐴 ) = ( 𝑧 𝐺 𝐴 ) )
21 20 eqeq1d ( 𝑦 = 𝑧 → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ↔ ( 𝑧 𝐺 𝐴 ) = 𝑈 ) )
22 21 reu8 ( ∃! 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ↔ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ∀ 𝑧𝑋 ( ( 𝑧 𝐺 𝐴 ) = 𝑈𝑦 = 𝑧 ) ) )
23 19 22 sylibr ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ∃! 𝑦𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )