Theorem imsmetlem 8319

Description: Lemma for imsmet 8320.

Hypotheses

Ref	Expression
imsmetlem.1	|- X = (Base` U)
imsmetlem.2	|- G = (+v` U)
imsmetlem.7	|- M = (inv` G)
imsmetlem.4	|- S = (.s` U)
imsmetlem.5	|- Z = (0v` U)
imsmetlem.6	|- N = (norm` U)
imsmetlem.8	|- D = (IndMet` U)
imsmetlem.9	|- U e. NrmCVec

Assertion

Ref	Expression
imsmetlem	|- D e. Met

Proof of Theorem imsmetlem

Step	Hyp	Ref	Expression
1		imsmetlem.1	. . 3 |- X = (Base` U)
2		fvex 3738	. . 3 |- (Base` U) e. V
3	1, 2	eqeltr 1547	. 2 |- X e. V
4		imsmetlem.9	. . 3 |- U e. NrmCVec
5		imsmetlem.8	. . . 4 |- D = (IndMet` U)
6	1, 5	imsdf 8316	. . 3 |- (U e. NrmCVec -> D:(X X. X)-->RR)
7	4, 6	ax-mp 7	. 2 |- D:(X X. X)-->RR
8		imsmetlem.2	. . . . . 6 |- G = (+v` U)
9		imsmetlem.4	. . . . . 6 |- S = (.s` U)
10		imsmetlem.6	. . . . . 6 |- N = (norm` U)
11	1, 8, 9, 10, 5	imsdval2 8314	. . . . 5 |- ((U e. NrmCVec /\ x e. X /\ y e. X) -> (xDy) = (N` (xG(-u1Sy))))
12	4, 11	mp3an1 905	. . . 4 |- ((x e. X /\ y e. X) -> (xDy) = (N` (xG(-u1Sy))))
13	12	eqeq1d 1486	. . 3 |- ((x e. X /\ y e. X) -> ((xDy) = 0 <-> (N` (xG(-u1Sy))) = 0))
14	1, 8	nvgcl 8235	. . . . . 6 |- ((U e. NrmCVec /\ x e. X /\ (-u1Sy) e. X) -> (xG(-u1Sy)) e. X)
15	4, 14	mp3an1 905	. . . . 5 |- ((x e. X /\ (-u1Sy) e. X) -> (xG(-u1Sy)) e. X)
16		ax1cn 5281	. . . . . . 7 |- 1 e. CC
17	16	negcl 5381	. . . . . 6 |- -u1 e. CC
18	1, 9	nvscl 8243	. . . . . 6 |- ((U e. NrmCVec /\ -u1 e. CC /\ y e. X) -> (-u1Sy) e. X)
19	4, 17, 18	mp3an12 908	. . . . 5 |- (y e. X -> (-u1Sy) e. X)
20	15, 19	sylan2 453	. . . 4 |- ((x e. X /\ y e. X) -> (xG(-u1Sy)) e. X)
21		imsmetlem.5	. . . . . 6 |- Z = (0v` U)
22	1, 21, 10	nvz 8293	. . . . 5 |- ((U e. NrmCVec /\ (xG(-u1Sy)) e. X) -> ((N` (xG(-u1Sy))) = 0 <-> (xG(-u1Sy)) = Z))
23	4, 22	mpan 697	. . . 4 |- ((xG(-u1Sy)) e. X -> ((N` (xG(-u1Sy))) = 0 <-> (xG(-u1Sy)) = Z))
24	20, 23	syl 10	. . 3 |- ((x e. X /\ y e. X) -> ((N` (xG(-u1Sy))) = 0 <-> (xG(-u1Sy)) = Z))
25	1, 21	nvzcl 8251	. . . . . . 7 |- (U e. NrmCVec -> Z e. X)
26	4, 25	ax-mp 7	. . . . . 6 |- Z e. X
27	1, 8	nvrcan 8240	. . . . . . 7 |- ((U e. NrmCVec /\ ((xG(-u1Sy)) e. X /\ Z e. X /\ y e. X)) -> (((xG(-u1Sy))Gy) = (ZGy) <-> (xG(-u1Sy)) = Z))
28	4, 27	mpan 697	. . . . . 6 |- (((xG(-u1Sy)) e. X /\ Z e. X /\ y e. X) -> (((xG(-u1Sy))Gy) = (ZGy) <-> (xG(-u1Sy)) = Z))
29	26, 28	mp3an2 906	. . . . 5 |- (((xG(-u1Sy)) e. X /\ y e. X) -> (((xG(-u1Sy))Gy) = (ZGy) <-> (xG(-u1Sy)) = Z))
30	20, 29	sylancom 477	. . . 4 |- ((x e. X /\ y e. X) -> (((xG(-u1Sy))Gy) = (ZGy) <-> (xG(-u1Sy)) = Z))
31	1, 8	nvass 8237	. . . . . . . 8 |- ((U e. NrmCVec /\ (x e. X /\ (-u1Sy) e. X /\ y e. X)) -> ((xG(-u1Sy))Gy) = (xG((-u1Sy)Gy)))
32	4, 31	mpan 697	. . . . . . 7 |- ((x e. X /\ (-u1Sy) e. X /\ y e. X) -> ((xG(-u1Sy))Gy) = (xG((-u1Sy)Gy)))
33		pm3.26 319	. . . . . . 7 |- ((x e. X /\ y e. X) -> x e. X)
34	19	adantl 390	. . . . . . 7 |- ((x e. X /\ y e. X) -> (-u1Sy) e. X)
35		pm3.27 323	. . . . . . 7 |- ((x e. X /\ y e. X) -> y e. X)
36	32, 33, 34, 35	syl3anc 860	. . . . . 6 |- ((x e. X /\ y e. X) -> ((xG(-u1Sy))Gy) = (xG((-u1Sy)Gy)))
37	1, 8, 9, 21	nvlinv 8270	. . . . . . . . 9 |- ((U e. NrmCVec /\ y e. X) -> ((-u1Sy)Gy) = Z)
38	4, 37	mpan 697	. . . . . . . 8 |- (y e. X -> ((-u1Sy)Gy) = Z)
39	38	adantl 390	. . . . . . 7 |- ((x e. X /\ y e. X) -> ((-u1Sy)Gy) = Z)
40	39	opreq2d 3982	. . . . . 6 |- ((x e. X /\ y e. X) -> (xG((-u1Sy)Gy)) = (xGZ))
41	1, 8, 21	nv0rid 8252	. . . . . . . 8 |- ((U e. NrmCVec /\ x e. X) -> (xGZ) = x)
42	4, 41	mpan 697	. . . . . . 7 |- (x e. X -> (xGZ) = x)
43	42	adantr 391	. . . . . 6 |- ((x e. X /\ y e. X) -> (xGZ) = x)
44	36, 40, 43	3eqtrd 1514	. . . . 5 |- ((x e. X /\ y e. X) -> ((xG(-u1Sy))Gy) = x)
45	1, 8, 21	nv0lid 8253	. . . . . . 7 |- ((U e. NrmCVec /\ y e. X) -> (ZGy) = y)
46	4, 45	mpan 697	. . . . . 6 |- (y e. X -> (ZGy) = y)
47	46	adantl 390	. . . . 5 |- ((x e. X /\ y e. X) -> (ZGy) = y)
48	44, 47	eqeq12d 1492	. . . 4 |- ((x e. X /\ y e. X) -> (((xG(-u1Sy))Gy) = (ZGy) <-> x = y))
49	30, 48	bitr3d 532	. . 3 |- ((x e. X /\ y e. X) -> ((xG(-u1Sy)) = Z <-> x = y))
50	13, 24, 49	3bitrd 546	. 2 |- ((x e. X /\ y e. X) -> ((xDy) = 0 <-> x = y))
51	1, 8, 10	nvtri 8294	. . . . . 6 |- ((U e. NrmCVec /\ (xG(-u1Sz)) e. X /\ (zG(-u1Sy)) e. X) -> (N` ((xG(-u1Sz))G(zG(-u1Sy)))) <_ ((N` (xG(-u1Sz))) + (N` (zG(-u1Sy)))))
52	4, 51	mp3an1 905	. . . . 5 |- (((xG(-u1Sz)) e. X /\ (zG(-u1Sy)) e. X) -> (N` ((xG(-u1Sz))G(zG(-u1Sy)))) <_ ((N` (xG(-u1Sz))) + (N` (zG(-u1Sy)))))
53	1, 8	nvgcl 8235	. . . . . . . 8 |- ((U e. NrmCVec /\ x e. X /\ (-u1Sz) e. X) -> (xG(-u1Sz)) e. X)
54	4, 53	mp3an1 905	. . . . . . 7 |- ((x e. X /\ (-u1Sz) e. X) -> (xG(-u1Sz)) e. X)
55		pm3.27 323	. . . . . . 7 |- ((z e. X /\ x e. X) -> x e. X)
56	1, 9	nvscl 8243	. . . . . . . . 9 |- ((U e. NrmCVec /\ -u1 e. CC /\ z e. X) -> (-u1Sz) e. X)
57	4, 17, 56	mp3an12 908	. . . . . . . 8 |- (z e. X -> (-u1Sz) e. X)
58	57	adantr 391	. . . . . . 7 |- ((z e. X /\ x e. X) -> (-u1Sz) e. X)
59	54, 55, 58	sylanc 473	. . . . . 6 |- ((z e. X /\ x e. X) -> (xG(-u1Sz)) e. X)
60	59	3adant3 801	. . . . 5 |- ((z e. X /\ x e. X /\ y e. X) -> (xG(-u1Sz)) e. X)
61	1, 8	nvgcl 8235	. . . . . . . 8 |- ((U e. NrmCVec /\ z e. X /\ (-u1Sy) e. X) -> (zG(-u1Sy)) e. X)
62	4, 61	mp3an1 905	. . . . . . 7 |- ((z e. X /\ (-u1Sy) e. X) -> (zG(-u1Sy)) e. X)
63	62, 19	sylan2 453	. . . . . 6 |- ((z e. X /\ y e. X) -> (zG(-u1Sy)) e. X)
64	63	3adant2 800	. . . . 5 |- ((z e. X /\ x e. X /\ y e. X) -> (zG(-u1Sy)) e. X)
65	52, 60, 64	sylanc 473	. . . 4 |- ((z e. X /\ x e. X /\ y e. X) -> (N` ((xG(-u1Sz))G(zG(-u1Sy)))) <_ ((N` (xG(-u1Sz))) + (N` (zG(-u1Sy)))))
66	12	3adant1 799	. . . . 5 |- ((z e. X /\ x e. X /\ y e. X) -> (xDy) = (N` (xG(-u1Sy))))
67	1, 8	nvass 8237	. . . . . . . . 9 |- ((U e. NrmCVec /\ ((xG(-u1Sz)) e. X /\ z e. X /\ (-u1Sy) e. X)) -> (((xG(-u1Sz))Gz)G(-u1Sy)) = ((xG(-u1Sz))G(zG(-u1Sy))))
68	4, 67	mpan