# Metamath Proof Explorer

## Theorem imsmetlem

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

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

### Proof

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