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={\mathrm{Base}}_G$$
	grpinvnzcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
	grpinvnzcl.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	grpinvnzcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to N\left(X\right)\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpinvnzcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinvnzcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		grpinvnzcl.n	$$⊢N={inv}_g\left(G\right)$$
4		eldifi	$$⊢X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\in B$$
5	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$
6	4 5	sylan2	$$⊢\left(G\in \mathrm{Grp}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to N\left(X\right)\in B$$
7		eldifsn	$$⊢X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)$$
8	1 2 3	grpinvnz	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to N\left(X\right)\ne \underset{\dot{}}{0}$$
9	8	3expb	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\right)\to N\left(X\right)\ne \underset{\dot{}}{0}$$
10	7 9	sylan2b	$$⊢\left(G\in \mathrm{Grp}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to N\left(X\right)\ne \underset{\dot{}}{0}$$
11		eldifsn	$$⊢N\left(X\right)\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(N\left(X\right)\in B\wedge N\left(X\right)\ne \underset{\dot{}}{0}\right)$$
12	6 10 11	sylanbrc	$$⊢\left(G\in \mathrm{Grp}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to N\left(X\right)\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$