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 
|- B = ( Base ` G )
grpinvnzcl.z 
|- .0. = ( 0g ` G )
grpinvnzcl.n 
|- N = ( invg ` G )
Assertion grpinvnzcl 
|- ( ( G e. Grp /\ X e. ( B \ { .0. } ) ) -> ( N ` X ) e. ( B \ { .0. } ) )

Proof

Step Hyp Ref Expression
1 grpinvnzcl.b 
 |-  B = ( Base ` G )
2 grpinvnzcl.z 
 |-  .0. = ( 0g ` G )
3 grpinvnzcl.n 
 |-  N = ( invg ` G )
4 eldifi 
 |-  ( X e. ( B \ { .0. } ) -> X e. B )
5 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
6 4 5 sylan2 
 |-  ( ( G e. Grp /\ X e. ( B \ { .0. } ) ) -> ( N ` X ) e. B )
7 eldifsn 
 |-  ( X e. ( B \ { .0. } ) <-> ( X e. B /\ X =/= .0. ) )
8 1 2 3 grpinvnz 
 |-  ( ( G e. Grp /\ X e. B /\ X =/= .0. ) -> ( N ` X ) =/= .0. )
9 8 3expb 
 |-  ( ( G e. Grp /\ ( X e. B /\ X =/= .0. ) ) -> ( N ` X ) =/= .0. )
10 7 9 sylan2b 
 |-  ( ( G e. Grp /\ X e. ( B \ { .0. } ) ) -> ( N ` X ) =/= .0. )
11 eldifsn 
 |-  ( ( N ` X ) e. ( B \ { .0. } ) <-> ( ( N ` X ) e. B /\ ( N ` X ) =/= .0. ) )
12 6 10 11 sylanbrc 
 |-  ( ( G e. Grp /\ X e. ( B \ { .0. } ) ) -> ( N ` X ) e. ( B \ { .0. } ) )