isngp

Description: The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	isngp.n	$⊢ N = norm (G)$
	isngp.z	$⊢ \underset{˙}{-} = -_{G}$
	isngp.d	$⊢ D = dist (G)$
Assertion	isngp	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} \subseteq D)$

Step	Hyp	Ref	Expression
1		isngp.n	$⊢ N = norm (G)$
2		isngp.z	$⊢ \underset{˙}{-} = -_{G}$
3		isngp.d	$⊢ D = dist (G)$
4		elin	$⊢ G \in (Grp \cap MetSp) \leftrightarrow (G \in Grp \land G \in MetSp)$
5	4	anbi1i	$⊢ (G \in (Grp \cap MetSp) \land N \circ \underset{˙}{-} \subseteq D) \leftrightarrow ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D)$
6		fveq2	$⊢ g = G \to norm (g) = norm (G)$
7	6 1	eqtr4di	$⊢ g = G \to norm (g) = N$
8		fveq2	$⊢ g = G \to -_{g} = -_{G}$
9	8 2	eqtr4di	$⊢ g = G \to -_{g} = \underset{˙}{-}$
10	7 9	coeq12d	$⊢ g = G \to norm (g) \circ -_{g} = N \circ \underset{˙}{-}$
11		fveq2	$⊢ g = G \to dist (g) = dist (G)$
12	11 3	eqtr4di	$⊢ g = G \to dist (g) = D$
13	10 12	sseq12d	$⊢ g = G \to (norm (g) \circ -_{g} \subseteq dist (g) \leftrightarrow N \circ \underset{˙}{-} \subseteq D)$
14		df-ngp	$⊢ NrmGrp = \{g \in (Grp \cap MetSp) \| norm (g) \circ -_{g} \subseteq dist (g)\}$
15	13 14	elrab2	$⊢ G \in NrmGrp \leftrightarrow (G \in (Grp \cap MetSp) \land N \circ \underset{˙}{-} \subseteq D)$
16		df-3an	$⊢ (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} \subseteq D) \leftrightarrow ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D)$
17	5 15 16	3bitr4i	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} \subseteq D)$

Metamath Proof Explorer