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	$⊢ \underset{˙}{0} = 0_{G}$
	grpinvnzcl.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvnz	$⊢ (G \in Grp \land X \in B \land X \neq \underset{˙}{0}) \to N (X) \neq \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		fveq2	$⊢ N (X) = \underset{˙}{0} \to N (N (X)) = N (\underset{˙}{0})$
5	4	adantl	$⊢ ((G \in Grp \land X \in B) \land N (X) = \underset{˙}{0}) \to N (N (X)) = N (\underset{˙}{0})$
6	1 3	grpinvinv	$⊢ (G \in Grp \land X \in B) \to N (N (X)) = X$
7	6	adantr	$⊢ ((G \in Grp \land X \in B) \land N (X) = \underset{˙}{0}) \to N (N (X)) = X$
8	2 3	grpinvid	$⊢ G \in Grp \to N (\underset{˙}{0}) = \underset{˙}{0}$
9	8	ad2antrr	$⊢ ((G \in Grp \land X \in B) \land N (X) = \underset{˙}{0}) \to N (\underset{˙}{0}) = \underset{˙}{0}$
10	5 7 9	3eqtr3d	$⊢ ((G \in Grp \land X \in B) \land N (X) = \underset{˙}{0}) \to X = \underset{˙}{0}$
11	10	ex	$⊢ (G \in Grp \land X \in B) \to (N (X) = \underset{˙}{0} \to X = \underset{˙}{0})$
12	11	necon3d	$⊢ (G \in Grp \land X \in B) \to (X \neq \underset{˙}{0} \to N (X) \neq \underset{˙}{0})$
13	12	3impia	$⊢ (G \in Grp \land X \in B \land X \neq \underset{˙}{0}) \to N (X) \neq \underset{˙}{0}$

Metamath Proof Explorer