isngp2

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)$
	isngp2.x	$⊢ X = {Base}_{G}$
	isngp2.e	$⊢ E = {D ↾}_{(X \times X)}$
Assertion	isngp2	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = E)$

Proof

Step	Hyp	Ref	Expression
1		isngp.n	$⊢ N = norm (G)$
2		isngp.z	$⊢ \underset{˙}{-} = -_{G}$
3		isngp.d	$⊢ D = dist (G)$
4		isngp2.x	$⊢ X = {Base}_{G}$
5		isngp2.e	$⊢ E = {D ↾}_{(X \times X)}$
6	1 2 3	isngp	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} \subseteq D)$
7		resss	$⊢ {D ↾}_{(X \times X)} \subseteq D$
8	5 7	eqsstri	$⊢ E \subseteq D$
9		sseq1	$⊢ N \circ \underset{˙}{-} = E \to (N \circ \underset{˙}{-} \subseteq D \leftrightarrow E \subseteq D)$
10	8 9	mpbiri	$⊢ N \circ \underset{˙}{-} = E \to N \circ \underset{˙}{-} \subseteq D$
11	3	reseq1i	$⊢ {D ↾}_{(X \times X)} = {dist (G) ↾}_{(X \times X)}$
12	5 11	eqtri	$⊢ E = {dist (G) ↾}_{(X \times X)}$
13	4 12	msmet	$⊢ G \in MetSp \to E \in Met (X)$
14	1 4 3 5	nmf2	$⊢ (G \in Grp \land E \in Met (X)) \to N : X ⟶ ℝ$
15	13 14	sylan2	$⊢ (G \in Grp \land G \in MetSp) \to N : X ⟶ ℝ$
16	4 2	grpsubf	$⊢ G \in Grp \to \underset{˙}{-} : X \times X ⟶ X$
17	16	ad2antrr	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to \underset{˙}{-} : X \times X ⟶ X$
18		fco	$⊢ (N : X ⟶ ℝ \land \underset{˙}{-} : X \times X ⟶ X) \to (N \circ \underset{˙}{-}) : X \times X ⟶ ℝ$
19	15 17 18	syl2an2r	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to (N \circ \underset{˙}{-}) : X \times X ⟶ ℝ$
20	19	fdmd	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to dom (N \circ \underset{˙}{-}) = X \times X$
21	20	reseq2d	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to {E ↾}_{dom (N \circ \underset{˙}{-})} = {E ↾}_{(X \times X)}$
22	4 12	msf	$⊢ G \in MetSp \to E : X \times X ⟶ ℝ$
23	22	ad2antlr	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to E : X \times X ⟶ ℝ$
24	23	ffund	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to Fun E$
25		simpr	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to N \circ \underset{˙}{-} \subseteq D$
26		ssv	$⊢ ℝ \subseteq V$
27		fss	$⊢ ((N \circ \underset{˙}{-}) : X \times X ⟶ ℝ \land ℝ \subseteq V) \to (N \circ \underset{˙}{-}) : X \times X ⟶ V$
28	19 26 27	sylancl	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to (N \circ \underset{˙}{-}) : X \times X ⟶ V$
29		fssxp	$⊢ (N \circ \underset{˙}{-}) : X \times X ⟶ V \to N \circ \underset{˙}{-} \subseteq (X \times X) \times V$
30	28 29	syl	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to N \circ \underset{˙}{-} \subseteq (X \times X) \times V$
31	25 30	ssind	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to N \circ \underset{˙}{-} \subseteq D \cap ((X \times X) \times V)$
32		df-res	$⊢ {D ↾}_{(X \times X)} = D \cap ((X \times X) \times V)$
33	5 32	eqtri	$⊢ E = D \cap ((X \times X) \times V)$
34	31 33	sseqtrrdi	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to N \circ \underset{˙}{-} \subseteq E$
35		funssres	$⊢ (Fun E \land N \circ \underset{˙}{-} \subseteq E) \to {E ↾}_{dom (N \circ \underset{˙}{-})} = N \circ \underset{˙}{-}$
36	24 34 35	syl2anc	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to {E ↾}_{dom (N \circ \underset{˙}{-})} = N \circ \underset{˙}{-}$
37		ffn	$⊢ E : X \times X ⟶ ℝ \to E Fn (X \times X)$
38		fnresdm	$⊢ E Fn (X \times X) \to {E ↾}_{(X \times X)} = E$
39	23 37 38	3syl	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to {E ↾}_{(X \times X)} = E$
40	21 36 39	3eqtr3d	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D) \to N \circ \underset{˙}{-} = E$
41	40	ex	$⊢ (G \in Grp \land G \in MetSp) \to (N \circ \underset{˙}{-} \subseteq D \to N \circ \underset{˙}{-} = E)$
42	10 41	impbid2	$⊢ (G \in Grp \land G \in MetSp) \to (N \circ \underset{˙}{-} = E \leftrightarrow N \circ \underset{˙}{-} \subseteq D)$
43	42	pm5.32i	$⊢ ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} = E) \leftrightarrow ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} \subseteq D)$
44		df-3an	$⊢ (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = E) \leftrightarrow ((G \in Grp \land G \in MetSp) \land N \circ \underset{˙}{-} = E)$
45		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)$
46	43 44 45	3bitr4i	$⊢ (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = E) \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} \subseteq D)$
47	6 46	bitr4i	$⊢ G \in NrmGrp \leftrightarrow (G \in Grp \land G \in MetSp \land N \circ \underset{˙}{-} = E)$

Metamath Proof Explorer

Theorem isngp2

Proof