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	$⊢ \underset{˙}{0} = 0_{G}$
	grpinvnzcl.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvnzcl	$⊢ (G \in Grp \land X \in (B ∖ \{\underset{˙}{0}\})) \to N (X) \in (B ∖ \{\underset{˙}{0}\})$

Step	Hyp	Ref	Expression
1		grpinvnzcl.b	$⊢ B = {Base}_{G}$
2		grpinvnzcl.z	$⊢ \underset{˙}{0} = 0_{G}$
3		grpinvnzcl.n	$⊢ N = {inv}_{g} (G)$
4		eldifi	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \to X \in B$
5	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
6	4 5	sylan2	$⊢ (G \in Grp \land X \in (B ∖ \{\underset{˙}{0}\})) \to N (X) \in B$
7		eldifsn	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in B \land X \neq \underset{˙}{0})$
8	1 2 3	grpinvnz	$⊢ (G \in Grp \land X \in B \land X \neq \underset{˙}{0}) \to N (X) \neq \underset{˙}{0}$
9	8	3expb	$⊢ (G \in Grp \land (X \in B \land X \neq \underset{˙}{0})) \to N (X) \neq \underset{˙}{0}$
10	7 9	sylan2b	$⊢ (G \in Grp \land X \in (B ∖ \{\underset{˙}{0}\})) \to N (X) \neq \underset{˙}{0}$
11		eldifsn	$⊢ N (X) \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (N (X) \in B \land N (X) \neq \underset{˙}{0})$
12	6 10 11	sylanbrc	$⊢ (G \in Grp \land X \in (B ∖ \{\underset{˙}{0}\})) \to N (X) \in (B ∖ \{\underset{˙}{0}\})$

Metamath Proof Explorer