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 imbitrid ⊢ ( ( 𝐺 ∈ 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 ∧ 𝐴 ∈ 𝑋 ) → ∃! 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )