imsmetlem

Description: Lemma for imsmet . (Contributed by NM, 29-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsmetlem.1	$⊢ X = BaseSet (U)$
	imsmetlem.2	$⊢ G = +_{v} (U)$
	imsmetlem.7	$⊢ M = inv (G)$
	imsmetlem.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	imsmetlem.5	$⊢ Z = 0_{vec} (U)$
	imsmetlem.6	$⊢ N = {norm}_{CV} (U)$
	imsmetlem.8	$⊢ D = IndMet (U)$
	imsmetlem.9	$⊢ U \in NrmCVec$
Assertion	imsmetlem	$⊢ D \in Met (X)$

Proof

Step	Hyp	Ref	Expression
1		imsmetlem.1	$⊢ X = BaseSet (U)$
2		imsmetlem.2	$⊢ G = +_{v} (U)$
3		imsmetlem.7	$⊢ M = inv (G)$
4		imsmetlem.4	$⊢ S = \cdot_{𝑠OLD} (U)$
5		imsmetlem.5	$⊢ Z = 0_{vec} (U)$
6		imsmetlem.6	$⊢ N = {norm}_{CV} (U)$
7		imsmetlem.8	$⊢ D = IndMet (U)$
8		imsmetlem.9	$⊢ U \in NrmCVec$
9	1	fvexi	$⊢ X \in V$
10	1 7	imsdf	$⊢ U \in NrmCVec \to D : X \times X ⟶ ℝ$
11	8 10	ax-mp	$⊢ D : X \times X ⟶ ℝ$
12	1 2 4 6 7	imsdval2	$⊢ (U \in NrmCVec \land x \in X \land y \in X) \to x D y = N (x G (-1 S y))$
13	8 12	mp3an1	$⊢ (x \in X \land y \in X) \to x D y = N (x G (-1 S y))$
14	13	eqeq1d	$⊢ (x \in X \land y \in X) \to (x D y = 0 \leftrightarrow N (x G (-1 S y)) = 0)$
15		neg1cn	$⊢ - 1 \in ℂ$
16	1 4	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land y \in X) \to -1 S y \in X$
17	8 15 16	mp3an12	$⊢ y \in X \to -1 S y \in X$
18	1 2	nvgcl	$⊢ (U \in NrmCVec \land x \in X \land -1 S y \in X) \to x G (-1 S y) \in X$
19	8 18	mp3an1	$⊢ (x \in X \land -1 S y \in X) \to x G (-1 S y) \in X$
20	17 19	sylan2	$⊢ (x \in X \land y \in X) \to x G (-1 S y) \in X$
21	1 5 6	nvz	$⊢ (U \in NrmCVec \land x G (-1 S y) \in X) \to (N (x G (-1 S y)) = 0 \leftrightarrow x G (-1 S y) = Z)$
22	8 20 21	sylancr	$⊢ (x \in X \land y \in X) \to (N (x G (-1 S y)) = 0 \leftrightarrow x G (-1 S y) = Z)$
23	1 5	nvzcl	$⊢ U \in NrmCVec \to Z \in X$
24	8 23	ax-mp	$⊢ Z \in X$
25	1 2	nvrcan	$⊢ (U \in NrmCVec \land (x G (-1 S y) \in X \land Z \in X \land y \in X)) \to ((x G (-1 S y)) G y = Z G y \leftrightarrow x G (-1 S y) = Z)$
26	8 25	mpan	$⊢ (x G (-1 S y) \in X \land Z \in X \land y \in X) \to ((x G (-1 S y)) G y = Z G y \leftrightarrow x G (-1 S y) = Z)$
27	24 26	mp3an2	$⊢ (x G (-1 S y) \in X \land y \in X) \to ((x G (-1 S y)) G y = Z G y \leftrightarrow x G (-1 S y) = Z)$
28	20 27	sylancom	$⊢ (x \in X \land y \in X) \to ((x G (-1 S y)) G y = Z G y \leftrightarrow x G (-1 S y) = Z)$
29		simpl	$⊢ (x \in X \land y \in X) \to x \in X$
30	17	adantl	$⊢ (x \in X \land y \in X) \to -1 S y \in X$
31		simpr	$⊢ (x \in X \land y \in X) \to y \in X$
32	1 2	nvass	$⊢ (U \in NrmCVec \land (x \in X \land -1 S y \in X \land y \in X)) \to (x G (-1 S y)) G y = x G ((-1 S y) G y)$
33	8 32	mpan	$⊢ (x \in X \land -1 S y \in X \land y \in X) \to (x G (-1 S y)) G y = x G ((-1 S y) G y)$
34	29 30 31 33	syl3anc	$⊢ (x \in X \land y \in X) \to (x G (-1 S y)) G y = x G ((-1 S y) G y)$
35	1 2 4 5	nvlinv	$⊢ (U \in NrmCVec \land y \in X) \to (-1 S y) G y = Z$
36	8 35	mpan	$⊢ y \in X \to (-1 S y) G y = Z$
37	36	adantl	$⊢ (x \in X \land y \in X) \to (-1 S y) G y = Z$
38	37	oveq2d	$⊢ (x \in X \land y \in X) \to x G ((-1 S y) G y) = x G Z$
39	1 2 5	nv0rid	$⊢ (U \in NrmCVec \land x \in X) \to x G Z = x$
40	8 39	mpan	$⊢ x \in X \to x G Z = x$
41	40	adantr	$⊢ (x \in X \land y \in X) \to x G Z = x$
42	34 38 41	3eqtrd	$⊢ (x \in X \land y \in X) \to (x G (-1 S y)) G y = x$
43	1 2 5	nv0lid	$⊢ (U \in NrmCVec \land y \in X) \to Z G y = y$
44	8 43	mpan	$⊢ y \in X \to Z G y = y$
45	44	adantl	$⊢ (x \in X \land y \in X) \to Z G y = y$
46	42 45	eqeq12d	$⊢ (x \in X \land y \in X) \to ((x G (-1 S y)) G y = Z G y \leftrightarrow x = y)$
47	28 46	bitr3d	$⊢ (x \in X \land y \in X) \to (x G (-1 S y) = Z \leftrightarrow x = y)$
48	14 22 47	3bitrd	$⊢ (x \in X \land y \in X) \to (x D y = 0 \leftrightarrow x = y)$
49		simpr	$⊢ (z \in X \land x \in X) \to x \in X$
50	1 4	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land z \in X) \to -1 S z \in X$
51	8 15 50	mp3an12	$⊢ z \in X \to -1 S z \in X$
52	51	adantr	$⊢ (z \in X \land x \in X) \to -1 S z \in X$
53	1 2	nvgcl	$⊢ (U \in NrmCVec \land x \in X \land -1 S z \in X) \to x G (-1 S z) \in X$
54	8 53	mp3an1	$⊢ (x \in X \land -1 S z \in X) \to x G (-1 S z) \in X$
55	49 52 54	syl2anc	$⊢ (z \in X \land x \in X) \to x G (-1 S z) \in X$
56	55	3adant3	$⊢ (z \in X \land x \in X \land y \in X) \to x G (-1 S z) \in X$
57	1 2	nvgcl	$⊢ (U \in NrmCVec \land z \in X \land -1 S y \in X) \to z G (-1 S y) \in X$
58	8 57	mp3an1	$⊢ (z \in X \land -1 S y \in X) \to z G (-1 S y) \in X$
59	17 58	sylan2	$⊢ (z \in X \land y \in X) \to z G (-1 S y) \in X$
60	59	3adant2	$⊢ (z \in X \land x \in X \land y \in X) \to z G (-1 S y) \in X$
61	1 2 6	nvtri	$⊢ (U \in NrmCVec \land x G (-1 S z) \in X \land z G (-1 S y) \in X) \to N ((x G (-1 S z)) G (z G (-1 S y))) \leq N (x G (-1 S z)) + N (z G (-1 S y))$
62	8 61	mp3an1	$⊢ (x G (-1 S z) \in X \land z G (-1 S y) \in X) \to N ((x G (-1 S z)) G (z G (-1 S y))) \leq N (x G (-1 S z)) + N (z G (-1 S y))$
63	56 60 62	syl2anc	$⊢ (z \in X \land x \in X \land y \in X) \to N ((x G (-1 S z)) G (z G (-1 S y))) \leq N (x G (-1 S z)) + N (z G (-1 S y))$
64	13	3adant1	$⊢ (z \in X \land x \in X \land y \in X) \to x D y = N (x G (-1 S y))$
65		simp1	$⊢ (z \in X \land x \in X \land y \in X) \to z \in X$
66	17	3ad2ant3	$⊢ (z \in X \land x \in X \land y \in X) \to -1 S y \in X$
67	1 2	nvass	$⊢ (U \in NrmCVec \land (x G (-1 S z) \in X \land z \in X \land -1 S y \in X)) \to ((x G (-1 S z)) G z) G (-1 S y) = (x G (-1 S z)) G (z G (-1 S y))$
68	8 67	mpan	$⊢ (x G (-1 S z) \in X \land z \in X \land -1 S y \in X) \to ((x G (-1 S z)) G z) G (-1 S y) = (x G (-1 S z)) G (z G (-1 S y))$
69	56 65 66 68	syl3anc	$⊢ (z \in X \land x \in X \land y \in X) \to ((x G (-1 S z)) G z) G (-1 S y) = (x G (-1 S z)) G (z G (-1 S y))$
70		simpl	$⊢ (z \in X \land x \in X) \to z \in X$
71	1 2	nvass	$⊢ (U \in NrmCVec \land (x \in X \land -1 S z \in X \land z \in X)) \to (x G (-1 S z)) G z = x G ((-1 S z) G z)$
72	8 71	mpan	$⊢ (x \in X \land -1 S z \in X \land z \in X) \to (x G (-1 S z)) G z = x G ((-1 S z) G z)$
73	49 52 70 72	syl3anc	$⊢ (z \in X \land x \in X) \to (x G (-1 S z)) G z = x G ((-1 S z) G z)$
74	1 2 4 5	nvlinv	$⊢ (U \in NrmCVec \land z \in X) \to (-1 S z) G z = Z$
75	8 74	mpan	$⊢ z \in X \to (-1 S z) G z = Z$
76	75	adantr	$⊢ (z \in X \land x \in X) \to (-1 S z) G z = Z$
77	76	oveq2d	$⊢ (z \in X \land x \in X) \to x G ((-1 S z) G z) = x G Z$
78	40	adantl	$⊢ (z \in X \land x \in X) \to x G Z = x$
79	73 77 78	3eqtrd	$⊢ (z \in X \land x \in X) \to (x G (-1 S z)) G z = x$
80	79	3adant3	$⊢ (z \in X \land x \in X \land y \in X) \to (x G (-1 S z)) G z = x$
81	80	oveq1d	$⊢ (z \in X \land x \in X \land y \in X) \to ((x G (-1 S z)) G z) G (-1 S y) = x G (-1 S y)$
82	69 81	eqtr3d	$⊢ (z \in X \land x \in X \land y \in X) \to (x G (-1 S z)) G (z G (-1 S y)) = x G (-1 S y)$
83	82	fveq2d	$⊢ (z \in X \land x \in X \land y \in X) \to N ((x G (-1 S z)) G (z G (-1 S y))) = N (x G (-1 S y))$
84	64 83	eqtr4d	$⊢ (z \in X \land x \in X \land y \in X) \to x D y = N ((x G (-1 S z)) G (z G (-1 S y)))$
85	1 2 4 6 7	imsdval2	$⊢ (U \in NrmCVec \land z \in X \land x \in X) \to z D x = N (z G (-1 S x))$
86	8 85	mp3an1	$⊢ (z \in X \land x \in X) \to z D x = N (z G (-1 S x))$
87	1 2 4 6	nvdif	$⊢ (U \in NrmCVec \land z \in X \land x \in X) \to N (z G (-1 S x)) = N (x G (-1 S z))$
88	8 87	mp3an1	$⊢ (z \in X \land x \in X) \to N (z G (-1 S x)) = N (x G (-1 S z))$
89	86 88	eqtrd	$⊢ (z \in X \land x \in X) \to z D x = N (x G (-1 S z))$
90	89	3adant3	$⊢ (z \in X \land x \in X \land y \in X) \to z D x = N (x G (-1 S z))$
91	1 2 4 6 7	imsdval2	$⊢ (U \in NrmCVec \land z \in X \land y \in X) \to z D y = N (z G (-1 S y))$
92	8 91	mp3an1	$⊢ (z \in X \land y \in X) \to z D y = N (z G (-1 S y))$
93	92	3adant2	$⊢ (z \in X \land x \in X \land y \in X) \to z D y = N (z G (-1 S y))$
94	90 93	oveq12d	$⊢ (z \in X \land x \in X \land y \in X) \to (z D x) + (z D y) = N (x G (-1 S z)) + N (z G (-1 S y))$
95	63 84 94	3brtr4d	$⊢ (z \in X \land x \in X \land y \in X) \to x D y \leq (z D x) + (z D y)$
96	95	3coml	$⊢ (x \in X \land y \in X \land z \in X) \to x D y \leq (z D x) + (z D y)$
97	9 11 48 96	ismeti	$⊢ D \in Met (X)$

Metamath Proof Explorer

Theorem imsmetlem

Proof