This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpinveu

Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of Herstein p. 55. (Contributed by NM, 24-Aug-2011)

Ref Expression
Hypotheses grpinveu.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpinveu.p ⊢ + = ( +g ‘ 𝐺 )
grpinveu.o ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion grpinveu ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 grpinveu.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpinveu.p ⊢ + = ( +g ‘ 𝐺 )
3 grpinveu.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 1 2 3 grpinvex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 )
5 eqtr3 ⊢ ( ( ( 𝑦 + 𝑋 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) → ( 𝑦 + 𝑋 ) = ( 𝑧 + 𝑋 ) )
6 1 2 grprcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑦 + 𝑋 ) = ( 𝑧 + 𝑋 ) ↔ 𝑦 = 𝑧 ) )
7 5 6 imbitrid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑦 + 𝑋 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) → 𝑦 = 𝑧 ) )
8 7 3exp2 ⊢ ( 𝐺 ∈ Grp → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝐵 → ( 𝑋 ∈ 𝐵 → ( ( ( 𝑦 + 𝑋 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) → 𝑦 = 𝑧 ) ) ) ) )
9 8 com24 ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐵 → ( 𝑧 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 → ( ( ( 𝑦 + 𝑋 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) → 𝑦 = 𝑧 ) ) ) ) )
10 9 imp41 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑦 + 𝑋 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) → 𝑦 = 𝑧 ) )
11 10 an32s ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑦 + 𝑋 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) → 𝑦 = 𝑧 ) )
12 11 expd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑦 + 𝑋 ) = 0 → ( ( 𝑧 + 𝑋 ) = 0 → 𝑦 = 𝑧 ) ) )
13 12 ralrimdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 + 𝑋 ) = 0 → ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 + 𝑋 ) = 0 → 𝑦 = 𝑧 ) ) )
14 13 ancld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 + 𝑋 ) = 0 → ( ( 𝑦 + 𝑋 ) = 0 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 + 𝑋 ) = 0 → 𝑦 = 𝑧 ) ) ) )
15 14 reximdva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 → ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑋 ) = 0 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 + 𝑋 ) = 0 → 𝑦 = 𝑧 ) ) ) )
16 4 15 mpd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑋 ) = 0 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 + 𝑋 ) = 0 → 𝑦 = 𝑧 ) ) )
17 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 + 𝑋 ) = ( 𝑧 + 𝑋 ) )
18 17 eqeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 + 𝑋 ) = 0 ↔ ( 𝑧 + 𝑋 ) = 0 ) )
19 18 reu8 ⊢ ( ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑋 ) = 0 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 + 𝑋 ) = 0 → 𝑦 = 𝑧 ) ) )
20 16 19 sylibr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 )