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

Metamath Proof Explorer

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 } ) )