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