nrmmetd

Description: Show that a group norm generates a metric. Part of Definition 2.2-1 of Kreyszig p. 58. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	nrmmetd.x	$⊢ X = {Base}_{G}$
	nrmmetd.m	$⊢ \underset{˙}{-} = -_{G}$
	nrmmetd.z	$⊢ \underset{˙}{0} = 0_{G}$
	nrmmetd.g	$⊢ φ \to G \in Grp$
	nrmmetd.f	$⊢ φ \to F : X ⟶ ℝ$
	nrmmetd.1	$⊢ (φ \land x \in X) \to (F (x) = 0 \leftrightarrow x = \underset{˙}{0})$
	nrmmetd.2	$⊢ (φ \land (x \in X \land y \in X)) \to F (x \underset{˙}{-} y) \leq F (x) + F (y)$
Assertion	nrmmetd	$⊢ φ \to F \circ \underset{˙}{-} \in Met (X)$

Proof

Step	Hyp	Ref	Expression
1		nrmmetd.x	$⊢ X = {Base}_{G}$
2		nrmmetd.m	$⊢ \underset{˙}{-} = -_{G}$
3		nrmmetd.z	$⊢ \underset{˙}{0} = 0_{G}$
4		nrmmetd.g	$⊢ φ \to G \in Grp$
5		nrmmetd.f	$⊢ φ \to F : X ⟶ ℝ$
6		nrmmetd.1	$⊢ (φ \land x \in X) \to (F (x) = 0 \leftrightarrow x = \underset{˙}{0})$
7		nrmmetd.2	$⊢ (φ \land (x \in X \land y \in X)) \to F (x \underset{˙}{-} y) \leq F (x) + F (y)$
8	1 2	grpsubf	$⊢ G \in Grp \to \underset{˙}{-} : X \times X ⟶ X$
9	4 8	syl	$⊢ φ \to \underset{˙}{-} : X \times X ⟶ X$
10		fco	$⊢ (F : X ⟶ ℝ \land \underset{˙}{-} : X \times X ⟶ X) \to (F \circ \underset{˙}{-}) : X \times X ⟶ ℝ$
11	5 9 10	syl2anc	$⊢ φ \to (F \circ \underset{˙}{-}) : X \times X ⟶ ℝ$
12		opelxpi	$⊢ (a \in X \land b \in X) \to ⟨a, b⟩ \in (X \times X)$
13		fvco3	$⊢ (\underset{˙}{-} : X \times X ⟶ X \land ⟨a, b⟩ \in (X \times X)) \to (F \circ \underset{˙}{-}) (⟨a, b⟩) = F (\underset{˙}{-} (⟨a, b⟩))$
14	9 12 13	syl2an	$⊢ (φ \land (a \in X \land b \in X)) \to (F \circ \underset{˙}{-}) (⟨a, b⟩) = F (\underset{˙}{-} (⟨a, b⟩))$
15		df-ov	$⊢ a (F \circ \underset{˙}{-}) b = (F \circ \underset{˙}{-}) (⟨a, b⟩)$
16		df-ov	$⊢ a \underset{˙}{-} b = \underset{˙}{-} (⟨a, b⟩)$
17	16	fveq2i	$⊢ F (a \underset{˙}{-} b) = F (\underset{˙}{-} (⟨a, b⟩))$
18	14 15 17	3eqtr4g	$⊢ (φ \land (a \in X \land b \in X)) \to a (F \circ \underset{˙}{-}) b = F (a \underset{˙}{-} b)$
19	18	eqeq1d	$⊢ (φ \land (a \in X \land b \in X)) \to (a (F \circ \underset{˙}{-}) b = 0 \leftrightarrow F (a \underset{˙}{-} b) = 0)$
20	6	ralrimiva	$⊢ φ \to \forall x \in X (F (x) = 0 \leftrightarrow x = \underset{˙}{0})$
21	1 2	grpsubcl	$⊢ (G \in Grp \land a \in X \land b \in X) \to a \underset{˙}{-} b \in X$
22	21	3expb	$⊢ (G \in Grp \land (a \in X \land b \in X)) \to a \underset{˙}{-} b \in X$
23	4 22	sylan	$⊢ (φ \land (a \in X \land b \in X)) \to a \underset{˙}{-} b \in X$
24		fveq2	$⊢ x = a \underset{˙}{-} b \to F (x) = F (a \underset{˙}{-} b)$
25	24	eqeq1d	$⊢ x = a \underset{˙}{-} b \to (F (x) = 0 \leftrightarrow F (a \underset{˙}{-} b) = 0)$
26		eqeq1	$⊢ x = a \underset{˙}{-} b \to (x = \underset{˙}{0} \leftrightarrow a \underset{˙}{-} b = \underset{˙}{0})$
27	25 26	bibi12d	$⊢ x = a \underset{˙}{-} b \to ((F (x) = 0 \leftrightarrow x = \underset{˙}{0}) \leftrightarrow (F (a \underset{˙}{-} b) = 0 \leftrightarrow a \underset{˙}{-} b = \underset{˙}{0}))$
28	27	rspccva	$⊢ (\forall x \in X (F (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land a \underset{˙}{-} b \in X) \to (F (a \underset{˙}{-} b) = 0 \leftrightarrow a \underset{˙}{-} b = \underset{˙}{0})$
29	20 23 28	syl2an2r	$⊢ (φ \land (a \in X \land b \in X)) \to (F (a \underset{˙}{-} b) = 0 \leftrightarrow a \underset{˙}{-} b = \underset{˙}{0})$
30	1 3 2	grpsubeq0	$⊢ (G \in Grp \land a \in X \land b \in X) \to (a \underset{˙}{-} b = \underset{˙}{0} \leftrightarrow a = b)$
31	30	3expb	$⊢ (G \in Grp \land (a \in X \land b \in X)) \to (a \underset{˙}{-} b = \underset{˙}{0} \leftrightarrow a = b)$
32	4 31	sylan	$⊢ (φ \land (a \in X \land b \in X)) \to (a \underset{˙}{-} b = \underset{˙}{0} \leftrightarrow a = b)$
33	19 29 32	3bitrd	$⊢ (φ \land (a \in X \land b \in X)) \to (a (F \circ \underset{˙}{-}) b = 0 \leftrightarrow a = b)$
34	5	adantr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F : X ⟶ ℝ$
35	23	adantrr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to a \underset{˙}{-} b \in X$
36	34 35	ffvelrnd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} b) \in ℝ$
37	4	adantr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to G \in Grp$
38		simprll	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to a \in X$
39		simprr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to c \in X$
40	1 2	grpsubcl	$⊢ (G \in Grp \land a \in X \land c \in X) \to a \underset{˙}{-} c \in X$
41	37 38 39 40	syl3anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to a \underset{˙}{-} c \in X$
42	34 41	ffvelrnd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} c) \in ℝ$
43		simprlr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to b \in X$
44	1 2	grpsubcl	$⊢ (G \in Grp \land b \in X \land c \in X) \to b \underset{˙}{-} c \in X$
45	37 43 39 44	syl3anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to b \underset{˙}{-} c \in X$
46	34 45	ffvelrnd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (b \underset{˙}{-} c) \in ℝ$
47	42 46	readdcld	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c) \in ℝ$
48	1 2	grpsubcl	$⊢ (G \in Grp \land c \in X \land a \in X) \to c \underset{˙}{-} a \in X$
49	37 39 38 48	syl3anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to c \underset{˙}{-} a \in X$
50	34 49	ffvelrnd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (c \underset{˙}{-} a) \in ℝ$
51	1 2	grpsubcl	$⊢ (G \in Grp \land c \in X \land b \in X) \to c \underset{˙}{-} b \in X$
52	37 39 43 51	syl3anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to c \underset{˙}{-} b \in X$
53	34 52	ffvelrnd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (c \underset{˙}{-} b) \in ℝ$
54	50 53	readdcld	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (c \underset{˙}{-} a) + F (c \underset{˙}{-} b) \in ℝ$
55	1 2	grpnnncan2	$⊢ (G \in Grp \land (a \in X \land b \in X \land c \in X)) \to (a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c) = a \underset{˙}{-} b$
56	37 38 43 39 55	syl13anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to (a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c) = a \underset{˙}{-} b$
57	56	fveq2d	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F ((a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c)) = F (a \underset{˙}{-} b)$
58	7	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X F (x \underset{˙}{-} y) \leq F (x) + F (y)$
59	58	adantr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to \forall x \in X \forall y \in X F (x \underset{˙}{-} y) \leq F (x) + F (y)$
60		fvoveq1	$⊢ x = a \underset{˙}{-} c \to F (x \underset{˙}{-} y) = F ((a \underset{˙}{-} c) \underset{˙}{-} y)$
61		fveq2	$⊢ x = a \underset{˙}{-} c \to F (x) = F (a \underset{˙}{-} c)$
62	61	oveq1d	$⊢ x = a \underset{˙}{-} c \to F (x) + F (y) = F (a \underset{˙}{-} c) + F (y)$
63	60 62	breq12d	$⊢ x = a \underset{˙}{-} c \to (F (x \underset{˙}{-} y) \leq F (x) + F (y) \leftrightarrow F ((a \underset{˙}{-} c) \underset{˙}{-} y) \leq F (a \underset{˙}{-} c) + F (y))$
64		oveq2	$⊢ y = b \underset{˙}{-} c \to (a \underset{˙}{-} c) \underset{˙}{-} y = (a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c)$
65	64	fveq2d	$⊢ y = b \underset{˙}{-} c \to F ((a \underset{˙}{-} c) \underset{˙}{-} y) = F ((a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c))$
66		fveq2	$⊢ y = b \underset{˙}{-} c \to F (y) = F (b \underset{˙}{-} c)$
67	66	oveq2d	$⊢ y = b \underset{˙}{-} c \to F (a \underset{˙}{-} c) + F (y) = F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c)$
68	65 67	breq12d	$⊢ y = b \underset{˙}{-} c \to (F ((a \underset{˙}{-} c) \underset{˙}{-} y) \leq F (a \underset{˙}{-} c) + F (y) \leftrightarrow F ((a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c)) \leq F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c))$
69	63 68	rspc2va	$⊢ ((a \underset{˙}{-} c \in X \land b \underset{˙}{-} c \in X) \land \forall x \in X \forall y \in X F (x \underset{˙}{-} y) \leq F (x) + F (y)) \to F ((a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c)) \leq F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c)$
70	41 45 59 69	syl21anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F ((a \underset{˙}{-} c) \underset{˙}{-} (b \underset{˙}{-} c)) \leq F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c)$
71	57 70	eqbrtrrd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} b) \leq F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c)$
72		eleq1w	$⊢ b = c \to (b \in X \leftrightarrow c \in X)$
73	72	anbi2d	$⊢ b = c \to ((a \in X \land b \in X) \leftrightarrow (a \in X \land c \in X))$
74	73	anbi2d	$⊢ b = c \to ((φ \land (a \in X \land b \in X)) \leftrightarrow (φ \land (a \in X \land c \in X)))$
75		oveq2	$⊢ b = c \to a \underset{˙}{-} b = a \underset{˙}{-} c$
76	75	fveq2d	$⊢ b = c \to F (a \underset{˙}{-} b) = F (a \underset{˙}{-} c)$
77		fvoveq1	$⊢ b = c \to F (b \underset{˙}{-} a) = F (c \underset{˙}{-} a)$
78	76 77	breq12d	$⊢ b = c \to (F (a \underset{˙}{-} b) \leq F (b \underset{˙}{-} a) \leftrightarrow F (a \underset{˙}{-} c) \leq F (c \underset{˙}{-} a))$
79	74 78	imbi12d	$⊢ b = c \to (((φ \land (a \in X \land b \in X)) \to F (a \underset{˙}{-} b) \leq F (b \underset{˙}{-} a)) \leftrightarrow ((φ \land (a \in X \land c \in X)) \to F (a \underset{˙}{-} c) \leq F (c \underset{˙}{-} a)))$
80	4	adantr	$⊢ (φ \land (a \in X \land b \in X)) \to G \in Grp$
81	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
82	80 81	syl	$⊢ (φ \land (a \in X \land b \in X)) \to \underset{˙}{0} \in X$
83		simprr	$⊢ (φ \land (a \in X \land b \in X)) \to b \in X$
84		simprl	$⊢ (φ \land (a \in X \land b \in X)) \to a \in X$
85	1 2	grpsubcl	$⊢ (G \in Grp \land b \in X \land a \in X) \to b \underset{˙}{-} a \in X$
86	80 83 84 85	syl3anc	$⊢ (φ \land (a \in X \land b \in X)) \to b \underset{˙}{-} a \in X$
87	58	adantr	$⊢ (φ \land (a \in X \land b \in X)) \to \forall x \in X \forall y \in X F (x \underset{˙}{-} y) \leq F (x) + F (y)$
88		fvoveq1	$⊢ x = \underset{˙}{0} \to F (x \underset{˙}{-} y) = F (\underset{˙}{0} \underset{˙}{-} y)$
89		fveq2	$⊢ x = \underset{˙}{0} \to F (x) = F (\underset{˙}{0})$
90	89	oveq1d	$⊢ x = \underset{˙}{0} \to F (x) + F (y) = F (\underset{˙}{0}) + F (y)$
91	88 90	breq12d	$⊢ x = \underset{˙}{0} \to (F (x \underset{˙}{-} y) \leq F (x) + F (y) \leftrightarrow F (\underset{˙}{0} \underset{˙}{-} y) \leq F (\underset{˙}{0}) + F (y))$
92		oveq2	$⊢ y = b \underset{˙}{-} a \to \underset{˙}{0} \underset{˙}{-} y = \underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)$
93	92	fveq2d	$⊢ y = b \underset{˙}{-} a \to F (\underset{˙}{0} \underset{˙}{-} y) = F (\underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a))$
94		fveq2	$⊢ y = b \underset{˙}{-} a \to F (y) = F (b \underset{˙}{-} a)$
95	94	oveq2d	$⊢ y = b \underset{˙}{-} a \to F (\underset{˙}{0}) + F (y) = F (\underset{˙}{0}) + F (b \underset{˙}{-} a)$
96	93 95	breq12d	$⊢ y = b \underset{˙}{-} a \to (F (\underset{˙}{0} \underset{˙}{-} y) \leq F (\underset{˙}{0}) + F (y) \leftrightarrow F (\underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)) \leq F (\underset{˙}{0}) + F (b \underset{˙}{-} a))$
97	91 96	rspc2va	$⊢ ((\underset{˙}{0} \in X \land b \underset{˙}{-} a \in X) \land \forall x \in X \forall y \in X F (x \underset{˙}{-} y) \leq F (x) + F (y)) \to F (\underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)) \leq F (\underset{˙}{0}) + F (b \underset{˙}{-} a)$
98	82 86 87 97	syl21anc	$⊢ (φ \land (a \in X \land b \in X)) \to F (\underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)) \leq F (\underset{˙}{0}) + F (b \underset{˙}{-} a)$
99		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
100	1 2 99 3	grpinvval2	$⊢ (G \in Grp \land b \underset{˙}{-} a \in X) \to {inv}_{g} (G) (b \underset{˙}{-} a) = \underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)$
101	4 86 100	syl2an2r	$⊢ (φ \land (a \in X \land b \in X)) \to {inv}_{g} (G) (b \underset{˙}{-} a) = \underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)$
102	1 2 99	grpinvsub	$⊢ (G \in Grp \land b \in X \land a \in X) \to {inv}_{g} (G) (b \underset{˙}{-} a) = a \underset{˙}{-} b$
103	80 83 84 102	syl3anc	$⊢ (φ \land (a \in X \land b \in X)) \to {inv}_{g} (G) (b \underset{˙}{-} a) = a \underset{˙}{-} b$
104	101 103	eqtr3d	$⊢ (φ \land (a \in X \land b \in X)) \to \underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a) = a \underset{˙}{-} b$
105	104	fveq2d	$⊢ (φ \land (a \in X \land b \in X)) \to F (\underset{˙}{0} \underset{˙}{-} (b \underset{˙}{-} a)) = F (a \underset{˙}{-} b)$
106	4 81	syl	$⊢ φ \to \underset{˙}{0} \in X$
107		pm5.501	$⊢ x = \underset{˙}{0} \to (F (x) = 0 \leftrightarrow (x = \underset{˙}{0} \leftrightarrow F (x) = 0))$
108		bicom	$⊢ (x = \underset{˙}{0} \leftrightarrow F (x) = 0) \leftrightarrow (F (x) = 0 \leftrightarrow x = \underset{˙}{0})$
109	107 108	bitrdi	$⊢ x = \underset{˙}{0} \to (F (x) = 0 \leftrightarrow (F (x) = 0 \leftrightarrow x = \underset{˙}{0}))$
110	89	eqeq1d	$⊢ x = \underset{˙}{0} \to (F (x) = 0 \leftrightarrow F (\underset{˙}{0}) = 0)$
111	109 110	bitr3d	$⊢ x = \underset{˙}{0} \to ((F (x) = 0 \leftrightarrow x = \underset{˙}{0}) \leftrightarrow F (\underset{˙}{0}) = 0)$
112	111	rspccva	$⊢ (\forall x \in X (F (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land \underset{˙}{0} \in X) \to F (\underset{˙}{0}) = 0$
113	20 106 112	syl2anc	$⊢ φ \to F (\underset{˙}{0}) = 0$
114	113	adantr	$⊢ (φ \land (a \in X \land b \in X)) \to F (\underset{˙}{0}) = 0$
115	114	oveq1d	$⊢ (φ \land (a \in X \land b \in X)) \to F (\underset{˙}{0}) + F (b \underset{˙}{-} a) = 0 + F (b \underset{˙}{-} a)$
116	5	adantr	$⊢ (φ \land (a \in X \land b \in X)) \to F : X ⟶ ℝ$
117	116 86	ffvelrnd	$⊢ (φ \land (a \in X \land b \in X)) \to F (b \underset{˙}{-} a) \in ℝ$
118	117	recnd	$⊢ (φ \land (a \in X \land b \in X)) \to F (b \underset{˙}{-} a) \in ℂ$
119	118	addid2d	$⊢ (φ \land (a \in X \land b \in X)) \to 0 + F (b \underset{˙}{-} a) = F (b \underset{˙}{-} a)$
120	115 119	eqtrd	$⊢ (φ \land (a \in X \land b \in X)) \to F (\underset{˙}{0}) + F (b \underset{˙}{-} a) = F (b \underset{˙}{-} a)$
121	98 105 120	3brtr3d	$⊢ (φ \land (a \in X \land b \in X)) \to F (a \underset{˙}{-} b) \leq F (b \underset{˙}{-} a)$
122	79 121	chvarvv	$⊢ (φ \land (a \in X \land c \in X)) \to F (a \underset{˙}{-} c) \leq F (c \underset{˙}{-} a)$
123	122	adantrlr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} c) \leq F (c \underset{˙}{-} a)$
124		eleq1w	$⊢ a = b \to (a \in X \leftrightarrow b \in X)$
125	124	anbi1d	$⊢ a = b \to ((a \in X \land c \in X) \leftrightarrow (b \in X \land c \in X))$
126	125	anbi2d	$⊢ a = b \to ((φ \land (a \in X \land c \in X)) \leftrightarrow (φ \land (b \in X \land c \in X)))$
127		fvoveq1	$⊢ a = b \to F (a \underset{˙}{-} c) = F (b \underset{˙}{-} c)$
128		oveq2	$⊢ a = b \to c \underset{˙}{-} a = c \underset{˙}{-} b$
129	128	fveq2d	$⊢ a = b \to F (c \underset{˙}{-} a) = F (c \underset{˙}{-} b)$
130	127 129	breq12d	$⊢ a = b \to (F (a \underset{˙}{-} c) \leq F (c \underset{˙}{-} a) \leftrightarrow F (b \underset{˙}{-} c) \leq F (c \underset{˙}{-} b))$
131	126 130	imbi12d	$⊢ a = b \to (((φ \land (a \in X \land c \in X)) \to F (a \underset{˙}{-} c) \leq F (c \underset{˙}{-} a)) \leftrightarrow ((φ \land (b \in X \land c \in X)) \to F (b \underset{˙}{-} c) \leq F (c \underset{˙}{-} b)))$
132	131 122	chvarvv	$⊢ (φ \land (b \in X \land c \in X)) \to F (b \underset{˙}{-} c) \leq F (c \underset{˙}{-} b)$
133	132	adantrll	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (b \underset{˙}{-} c) \leq F (c \underset{˙}{-} b)$
134	42 46 50 53 123 133	le2addd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} c) + F (b \underset{˙}{-} c) \leq F (c \underset{˙}{-} a) + F (c \underset{˙}{-} b)$
135	36 47 54 71 134	letrd	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to F (a \underset{˙}{-} b) \leq F (c \underset{˙}{-} a) + F (c \underset{˙}{-} b)$
136	18	adantrr	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to a (F \circ \underset{˙}{-}) b = F (a \underset{˙}{-} b)$
137		opelxpi	$⊢ (c \in X \land a \in X) \to ⟨c, a⟩ \in (X \times X)$
138	39 38 137	syl2anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to ⟨c, a⟩ \in (X \times X)$
139		fvco3	$⊢ (\underset{˙}{-} : X \times X ⟶ X \land ⟨c, a⟩ \in (X \times X)) \to (F \circ \underset{˙}{-}) (⟨c, a⟩) = F (\underset{˙}{-} (⟨c, a⟩))$
140	9 138 139	syl2an2r	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to (F \circ \underset{˙}{-}) (⟨c, a⟩) = F (\underset{˙}{-} (⟨c, a⟩))$
141		df-ov	$⊢ c (F \circ \underset{˙}{-}) a = (F \circ \underset{˙}{-}) (⟨c, a⟩)$
142		df-ov	$⊢ c \underset{˙}{-} a = \underset{˙}{-} (⟨c, a⟩)$
143	142	fveq2i	$⊢ F (c \underset{˙}{-} a) = F (\underset{˙}{-} (⟨c, a⟩))$
144	140 141 143	3eqtr4g	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to c (F \circ \underset{˙}{-}) a = F (c \underset{˙}{-} a)$
145		opelxpi	$⊢ (c \in X \land b \in X) \to ⟨c, b⟩ \in (X \times X)$
146	39 43 145	syl2anc	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to ⟨c, b⟩ \in (X \times X)$
147		fvco3	$⊢ (\underset{˙}{-} : X \times X ⟶ X \land ⟨c, b⟩ \in (X \times X)) \to (F \circ \underset{˙}{-}) (⟨c, b⟩) = F (\underset{˙}{-} (⟨c, b⟩))$
148	9 146 147	syl2an2r	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to (F \circ \underset{˙}{-}) (⟨c, b⟩) = F (\underset{˙}{-} (⟨c, b⟩))$
149		df-ov	$⊢ c (F \circ \underset{˙}{-}) b = (F \circ \underset{˙}{-}) (⟨c, b⟩)$
150		df-ov	$⊢ c \underset{˙}{-} b = \underset{˙}{-} (⟨c, b⟩)$
151	150	fveq2i	$⊢ F (c \underset{˙}{-} b) = F (\underset{˙}{-} (⟨c, b⟩))$
152	148 149 151	3eqtr4g	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to c (F \circ \underset{˙}{-}) b = F (c \underset{˙}{-} b)$
153	144 152	oveq12d	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b) = F (c \underset{˙}{-} a) + F (c \underset{˙}{-} b)$
154	135 136 153	3brtr4d	$⊢ (φ \land ((a \in X \land b \in X) \land c \in X)) \to a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b)$
155	154	expr	$⊢ (φ \land (a \in X \land b \in X)) \to (c \in X \to a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b))$
156	155	ralrimiv	$⊢ (φ \land (a \in X \land b \in X)) \to \forall c \in X a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b)$
157	33 156	jca	$⊢ (φ \land (a \in X \land b \in X)) \to ((a (F \circ \underset{˙}{-}) b = 0 \leftrightarrow a = b) \land \forall c \in X a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b))$
158	157	ralrimivva	$⊢ φ \to \forall a \in X \forall b \in X ((a (F \circ \underset{˙}{-}) b = 0 \leftrightarrow a = b) \land \forall c \in X a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b))$
159	1	fvexi	$⊢ X \in V$
160		ismet	$⊢ X \in V \to (F \circ \underset{˙}{-} \in Met (X) \leftrightarrow ((F \circ \underset{˙}{-}) : X \times X ⟶ ℝ \land \forall a \in X \forall b \in X ((a (F \circ \underset{˙}{-}) b = 0 \leftrightarrow a = b) \land \forall c \in X a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b))))$
161	159 160	ax-mp	$⊢ F \circ \underset{˙}{-} \in Met (X) \leftrightarrow ((F \circ \underset{˙}{-}) : X \times X ⟶ ℝ \land \forall a \in X \forall b \in X ((a (F \circ \underset{˙}{-}) b = 0 \leftrightarrow a = b) \land \forall c \in X a (F \circ \underset{˙}{-}) b \leq (c (F \circ \underset{˙}{-}) a) + (c (F \circ \underset{˙}{-}) b)))$
162	11 158 161	sylanbrc	$⊢ φ \to F \circ \underset{˙}{-} \in Met (X)$

Metamath Proof Explorer

Theorem nrmmetd

Proof