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	grprinvd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = 0 )