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

Metamath Proof Explorer

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 )