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