Theorem grpinvnz

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

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

Proof

Step	Hyp	Ref	Expression
1		grpinvnzcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpinvnzcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		grpinvnzcl.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
4		fveq2	⊢ ( ( 𝑁 ‘ 𝑋 ) = 0 → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 0 ) )
5	4	adantl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) = 0 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ 0 ) )
6	1 3	grpinvinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
7	6	adantr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) = 0 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
8	2 3	grpinvid	⊢ ( 𝐺 ∈ Grp → ( 𝑁 ‘ 0 ) = 0 )
9	8	ad2antrr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) = 0 ) → ( 𝑁 ‘ 0 ) = 0 )
10	5 7 9	3eqtr3d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) = 0 ) → 𝑋 = 0 )
11	10	ex	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) = 0 → 𝑋 = 0 ) )
12	11	necon3d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≠ 0 → ( 𝑁 ‘ 𝑋 ) ≠ 0 ) )
13	12	3impia	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ 𝑋 ) ≠ 0 )