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