Metamath Proof Explorer

Theorem nmeq0

Description: The identity is the only element of the group with zero norm. First part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 24-Nov-2006) (Revised by Mario Carneiro, 4-Oct-2015)

		Ref	Expression
	Hypotheses	nmf.x	$⊢ X = {Base}_{G}$
		nmf.n	$⊢ N = norm (G)$
		nmeq0.z	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	nmeq0	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) = 0 \leftrightarrow A = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nmeq0.z	$⊢ \underset{˙}{0} = 0_{G}$
4		eqid	$⊢ dist (G) = dist (G)$
5	2 1 3 4	nmval	$⊢ A \in X \to N (A) = A dist (G) \underset{˙}{0}$
6	5	adantl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) = A dist (G) \underset{˙}{0}$
7	6	eqeq1d	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) = 0 \leftrightarrow A dist (G) \underset{˙}{0} = 0)$
8		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
9	8	adantr	$⊢ (G \in NrmGrp \land A \in X) \to G \in Grp$
10	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
11	9 10	syl	$⊢ (G \in NrmGrp \land A \in X) \to \underset{˙}{0} \in X$
12		ngpxms	$⊢ G \in NrmGrp \to G \in ∞MetSp$
13	1 4	xmseq0	$⊢ (G \in ∞MetSp \land A \in X \land \underset{˙}{0} \in X) \to (A dist (G) \underset{˙}{0} = 0 \leftrightarrow A = \underset{˙}{0})$
14	12 13	syl3an1	$⊢ (G \in NrmGrp \land A \in X \land \underset{˙}{0} \in X) \to (A dist (G) \underset{˙}{0} = 0 \leftrightarrow A = \underset{˙}{0})$
15	11 14	mpd3an3	$⊢ (G \in NrmGrp \land A \in X) \to (A dist (G) \underset{˙}{0} = 0 \leftrightarrow A = \underset{˙}{0})$
16	7 15	bitrd	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) = 0 \leftrightarrow A = \underset{˙}{0})$