Theorem imsmetlem

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

	Ref	Expression
Hypotheses	imsmetlem.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	imsmetlem.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	imsmetlem.7	⊢ 𝑀 = ( inv ‘ 𝐺 )
	imsmetlem.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	imsmetlem.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	imsmetlem.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	imsmetlem.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	imsmetlem.9	⊢ 𝑈 ∈ NrmCVec
Assertion	imsmetlem	⊢ 𝐷 ∈ ( Met ‘ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		imsmetlem.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		imsmetlem.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		imsmetlem.7	⊢ 𝑀 = ( inv ‘ 𝐺 )
4		imsmetlem.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
5		imsmetlem.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
6		imsmetlem.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
7		imsmetlem.8	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
8		imsmetlem.9	⊢ 𝑈 ∈ NrmCVec
9	1	fvexi	⊢ 𝑋 ∈ V
10	1 7	imsdf	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
11	8 10	ax-mp	⊢ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ
12	1 2 4 6 7	imsdval2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
13	8 12	mp3an1	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
14	13	eqeq1d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) = 0 ) )
15		neg1cn	⊢ - 1 ∈ ℂ
16	1 4	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( - 1 𝑆 𝑦 ) ∈ 𝑋 )
17	8 15 16	mp3an12	⊢ ( 𝑦 ∈ 𝑋 → ( - 1 𝑆 𝑦 ) ∈ 𝑋 )
18	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
19	8 18	mp3an1	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
20	17 19	sylan2	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
21	1 5 6	nvz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) = 0 ↔ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ) )
22	8 20 21	sylancr	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) = 0 ↔ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ) )
23	1 5	nvzcl	⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
24	8 23	ax-mp	⊢ 𝑍 ∈ 𝑋
25	1 2	nvrcan	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑦 ) ↔ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ) )
26	8 25	mpan	⊢ ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑦 ) ↔ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ) )
27	24 26	mp3an2	⊢ ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑦 ) ↔ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ) )
28	20 27	sylancom	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑦 ) ↔ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ) )
29		simpl	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
30	17	adantl	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( - 1 𝑆 𝑦 ) ∈ 𝑋 )
31		simpr	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
32	1 2	nvass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑥 𝐺 ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) ) )
33	8 32	mpan	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑥 𝐺 ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) ) )
34	29 30 31 33	syl3anc	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑥 𝐺 ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) ) )
35	1 2 4 5	nvlinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) = 𝑍 )
36	8 35	mpan	⊢ ( 𝑦 ∈ 𝑋 → ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) = 𝑍 )
37	36	adantl	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) = 𝑍 )
38	37	oveq2d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 ( ( - 1 𝑆 𝑦 ) 𝐺 𝑦 ) ) = ( 𝑥 𝐺 𝑍 ) )
39	1 2 5	nv0rid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑍 ) = 𝑥 )
40	8 39	mpan	⊢ ( 𝑥 ∈ 𝑋 → ( 𝑥 𝐺 𝑍 ) = 𝑥 )
41	40	adantr	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑍 ) = 𝑥 )
42	34 38 41	3eqtrd	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = 𝑥 )
43	1 2 5	nv0lid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( 𝑍 𝐺 𝑦 ) = 𝑦 )
44	8 43	mpan	⊢ ( 𝑦 ∈ 𝑋 → ( 𝑍 𝐺 𝑦 ) = 𝑦 )
45	44	adantl	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑍 𝐺 𝑦 ) = 𝑦 )
46	42 45	eqeq12d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) 𝐺 𝑦 ) = ( 𝑍 𝐺 𝑦 ) ↔ 𝑥 = 𝑦 ) )
47	28 46	bitr3d	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = 𝑍 ↔ 𝑥 = 𝑦 ) )
48	14 22 47	3bitrd	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
49		simpr	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
50	1 4	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( - 1 𝑆 𝑧 ) ∈ 𝑋 )
51	8 15 50	mp3an12	⊢ ( 𝑧 ∈ 𝑋 → ( - 1 𝑆 𝑧 ) ∈ 𝑋 )
52	51	adantr	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( - 1 𝑆 𝑧 ) ∈ 𝑋 )
53	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑧 ) ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 )
54	8 53	mp3an1	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑧 ) ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 )
55	49 52 54	syl2anc	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 )
56	55	3adant3	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 )
57	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ) → ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
58	8 57	mp3an1	⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ) → ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
59	17 58	sylan2	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
60	59	3adant2	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 )
61	1 2 6	nvtri	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 ∧ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) + ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) )
62	8 61	mp3an1	⊢ ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 ∧ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) + ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) )
63	56 60 62	syl2anc	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) + ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) )
64	13	3adant1	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
65		simp1	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
66	17	3ad2ant3	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( - 1 𝑆 𝑦 ) ∈ 𝑋 )
67	1 2	nvass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ) ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) 𝐺 ( - 1 𝑆 𝑦 ) ) = ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
68	8 67	mpan	⊢ ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( - 1 𝑆 𝑦 ) ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) 𝐺 ( - 1 𝑆 𝑦 ) ) = ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
69	56 65 66 68	syl3anc	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) 𝐺 ( - 1 𝑆 𝑦 ) ) = ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
70		simpl	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
71	1 2	nvass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑧 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) ) )
72	8 71	mpan	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( - 1 𝑆 𝑧 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) ) )
73	49 52 70 72	syl3anc	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) ) )
74	1 2 4 5	nvlinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ) → ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) = 𝑍 )
75	8 74	mpan	⊢ ( 𝑧 ∈ 𝑋 → ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) = 𝑍 )
76	75	adantr	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) = 𝑍 )
77	76	oveq2d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐺 ( ( - 1 𝑆 𝑧 ) 𝐺 𝑧 ) ) = ( 𝑥 𝐺 𝑍 ) )
78	40	adantl	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑍 ) = 𝑥 )
79	73 77 78	3eqtrd	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) = 𝑥 )
80	79	3adant3	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) = 𝑥 )
81	80	oveq1d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 𝑧 ) 𝐺 ( - 1 𝑆 𝑦 ) ) = ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) )
82	69 81	eqtr3d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) = ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) )
83	82	fveq2d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
84	64 83	eqtr4d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) 𝐺 ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) )
85	1 2 4 6 7	imsdval2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑥 ) ) ) )
86	8 85	mp3an1	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑥 ) ) ) )
87	1 2 4 6	nvdif	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑥 ) ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) )
88	8 87	mp3an1	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑥 ) ) ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) )
89	86 88	eqtrd	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) )
90	89	3adant3	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) )
91	1 2 4 6 7	imsdval2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
92	8 91	mp3an1	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
93	92	3adant2	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) )
94	90 93	oveq12d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑁 ‘ ( 𝑥 𝐺 ( - 1 𝑆 𝑧 ) ) ) + ( 𝑁 ‘ ( 𝑧 𝐺 ( - 1 𝑆 𝑦 ) ) ) ) )
95	63 84 94	3brtr4d	⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
96	95	3coml	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
97	9 11 48 96	ismeti	⊢ 𝐷 ∈ ( Met ‘ 𝑋 )