Theorem grplinv

Description: The left 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	grplinv	⊢ ( ( 𝐺 ∈ 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 3 4	grpinvval	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )
6	5	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )
7	1 2 3	grpinveu	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 )
8		riotacl2	⊢ ( ∃! 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝑦 + 𝑋 ) = 0 } )
9	7 8	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝑦 + 𝑋 ) = 0 } )
10	6 9	eqeltrd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝑦 + 𝑋 ) = 0 } )
11		oveq1	⊢ ( 𝑦 = ( 𝑁 ‘ 𝑋 ) → ( 𝑦 + 𝑋 ) = ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) )
12	11	eqeq1d	⊢ ( 𝑦 = ( 𝑁 ‘ 𝑋 ) → ( ( 𝑦 + 𝑋 ) = 0 ↔ ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 ) )
13	12	elrab	⊢ ( ( 𝑁 ‘ 𝑋 ) ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝑦 + 𝑋 ) = 0 } ↔ ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 ) )
14	13	simprbi	⊢ ( ( 𝑁 ‘ 𝑋 ) ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝑦 + 𝑋 ) = 0 } → ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 )
15	10 14	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 )