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 
|- B = ( Base ` G )
grpinvnzcl.z 
|- .0. = ( 0g ` G )
grpinvnzcl.n 
|- N = ( invg ` G )
Assertion grpinvnz 
|- ( ( G e. Grp /\ X e. B /\ X =/= .0. ) -> ( N ` X ) =/= .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 fveq2 
 |-  ( ( N ` X ) = .0. -> ( N ` ( N ` X ) ) = ( N ` .0. ) )
5 4 adantl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( N ` X ) = .0. ) -> ( N ` ( N ` X ) ) = ( N ` .0. ) )
6 1 3 grpinvinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
7 6 adantr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( N ` X ) = .0. ) -> ( N ` ( N ` X ) ) = X )
8 2 3 grpinvid 
 |-  ( G e. Grp -> ( N ` .0. ) = .0. )
9 8 ad2antrr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( N ` X ) = .0. ) -> ( N ` .0. ) = .0. )
10 5 7 9 3eqtr3d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( N ` X ) = .0. ) -> X = .0. )
11 10 ex 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) = .0. -> X = .0. ) )
12 11 necon3d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X =/= .0. -> ( N ` X ) =/= .0. ) )
13 12 3impia 
 |-  ( ( G e. Grp /\ X e. B /\ X =/= .0. ) -> ( N ` X ) =/= .0. )