Theorem grpinvnzcl

Description: The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015)

	Ref	Expression
Hypotheses	grpinvnzcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpinvnzcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
	grpinvnzcl.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	grpinvnzcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑁 ‘ 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvnzcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvnzcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		grpinvnzcl.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		eldifi	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → 𝑋 ∈ 𝐵 )
5	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
6	4 5	sylan2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
7		eldifsn	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) )
8	1 2 3	grpinvnz	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ 𝑋 ) ≠ 0 )
9	8	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ) → ( 𝑁 ‘ 𝑋 ) ≠ 0 )
10	7 9	sylan2b	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑁 ‘ 𝑋 ) ≠ 0 )
11		eldifsn	⊢ ( ( 𝑁 ‘ 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑋 ) ≠ 0 ) )
12	6 10 11	sylanbrc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑁 ‘ 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) )