Metamath Proof Explorer

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 ‘ 𝑋 )