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

Metamath Proof Explorer

Theorem grprinv

Description: The right inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grpinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpinv.p ⊢ + = ( +g ‘ 𝐺 )
grpinv.u ⊢ 0 = ( 0g ‘ 𝐺 )
grpinv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion grprinv ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 grpinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpinv.p ⊢ + = ( +g ‘ 𝐺 )
3 grpinv.u ⊢ 0 = ( 0g ‘ 𝐺 )
4 grpinv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
5 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
6 1 3 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
7 1 2 3 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
8 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9 1 2 3 grpinvex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
10 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11 1 4 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
12 1 2 3 4 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 )
13 5 6 7 8 9 10 11 12 grpinva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = 0 )