Step |
Hyp |
Ref |
Expression |
1 |
|
nlmvscn.f |
|- F = ( Scalar ` W ) |
2 |
|
nlmvscn.v |
|- V = ( Base ` W ) |
3 |
|
nlmvscn.k |
|- K = ( Base ` F ) |
4 |
|
nlmvscn.d |
|- D = ( dist ` W ) |
5 |
|
nlmvscn.e |
|- E = ( dist ` F ) |
6 |
|
nlmvscn.n |
|- N = ( norm ` W ) |
7 |
|
nlmvscn.a |
|- A = ( norm ` F ) |
8 |
|
nlmvscn.s |
|- .x. = ( .s ` W ) |
9 |
|
nlmvscn.t |
|- T = ( ( R / 2 ) / ( ( A ` B ) + 1 ) ) |
10 |
|
nlmvscn.u |
|- U = ( ( R / 2 ) / ( ( N ` X ) + T ) ) |
11 |
|
nlmvscn.w |
|- ( ph -> W e. NrmMod ) |
12 |
|
nlmvscn.r |
|- ( ph -> R e. RR+ ) |
13 |
|
nlmvscn.b |
|- ( ph -> B e. K ) |
14 |
|
nlmvscn.x |
|- ( ph -> X e. V ) |
15 |
|
nlmvscn.c |
|- ( ph -> C e. K ) |
16 |
|
nlmvscn.y |
|- ( ph -> Y e. V ) |
17 |
|
nlmvscn.1 |
|- ( ph -> ( B E C ) < U ) |
18 |
|
nlmvscn.2 |
|- ( ph -> ( X D Y ) < T ) |
19 |
|
nlmngp |
|- ( W e. NrmMod -> W e. NrmGrp ) |
20 |
11 19
|
syl |
|- ( ph -> W e. NrmGrp ) |
21 |
|
ngpms |
|- ( W e. NrmGrp -> W e. MetSp ) |
22 |
20 21
|
syl |
|- ( ph -> W e. MetSp ) |
23 |
|
nlmlmod |
|- ( W e. NrmMod -> W e. LMod ) |
24 |
11 23
|
syl |
|- ( ph -> W e. LMod ) |
25 |
2 1 8 3
|
lmodvscl |
|- ( ( W e. LMod /\ B e. K /\ X e. V ) -> ( B .x. X ) e. V ) |
26 |
24 13 14 25
|
syl3anc |
|- ( ph -> ( B .x. X ) e. V ) |
27 |
2 1 8 3
|
lmodvscl |
|- ( ( W e. LMod /\ C e. K /\ Y e. V ) -> ( C .x. Y ) e. V ) |
28 |
24 15 16 27
|
syl3anc |
|- ( ph -> ( C .x. Y ) e. V ) |
29 |
2 4
|
mscl |
|- ( ( W e. MetSp /\ ( B .x. X ) e. V /\ ( C .x. Y ) e. V ) -> ( ( B .x. X ) D ( C .x. Y ) ) e. RR ) |
30 |
22 26 28 29
|
syl3anc |
|- ( ph -> ( ( B .x. X ) D ( C .x. Y ) ) e. RR ) |
31 |
2 1 8 3
|
lmodvscl |
|- ( ( W e. LMod /\ B e. K /\ Y e. V ) -> ( B .x. Y ) e. V ) |
32 |
24 13 16 31
|
syl3anc |
|- ( ph -> ( B .x. Y ) e. V ) |
33 |
2 4
|
mscl |
|- ( ( W e. MetSp /\ ( B .x. X ) e. V /\ ( B .x. Y ) e. V ) -> ( ( B .x. X ) D ( B .x. Y ) ) e. RR ) |
34 |
22 26 32 33
|
syl3anc |
|- ( ph -> ( ( B .x. X ) D ( B .x. Y ) ) e. RR ) |
35 |
2 4
|
mscl |
|- ( ( W e. MetSp /\ ( B .x. Y ) e. V /\ ( C .x. Y ) e. V ) -> ( ( B .x. Y ) D ( C .x. Y ) ) e. RR ) |
36 |
22 32 28 35
|
syl3anc |
|- ( ph -> ( ( B .x. Y ) D ( C .x. Y ) ) e. RR ) |
37 |
34 36
|
readdcld |
|- ( ph -> ( ( ( B .x. X ) D ( B .x. Y ) ) + ( ( B .x. Y ) D ( C .x. Y ) ) ) e. RR ) |
38 |
12
|
rpred |
|- ( ph -> R e. RR ) |
39 |
2 4
|
mstri |
|- ( ( W e. MetSp /\ ( ( B .x. X ) e. V /\ ( C .x. Y ) e. V /\ ( B .x. Y ) e. V ) ) -> ( ( B .x. X ) D ( C .x. Y ) ) <_ ( ( ( B .x. X ) D ( B .x. Y ) ) + ( ( B .x. Y ) D ( C .x. Y ) ) ) ) |
40 |
22 26 28 32 39
|
syl13anc |
|- ( ph -> ( ( B .x. X ) D ( C .x. Y ) ) <_ ( ( ( B .x. X ) D ( B .x. Y ) ) + ( ( B .x. Y ) D ( C .x. Y ) ) ) ) |
41 |
1
|
nlmngp2 |
|- ( W e. NrmMod -> F e. NrmGrp ) |
42 |
11 41
|
syl |
|- ( ph -> F e. NrmGrp ) |
43 |
3 7
|
nmcl |
|- ( ( F e. NrmGrp /\ B e. K ) -> ( A ` B ) e. RR ) |
44 |
42 13 43
|
syl2anc |
|- ( ph -> ( A ` B ) e. RR ) |
45 |
3 7
|
nmge0 |
|- ( ( F e. NrmGrp /\ B e. K ) -> 0 <_ ( A ` B ) ) |
46 |
42 13 45
|
syl2anc |
|- ( ph -> 0 <_ ( A ` B ) ) |
47 |
44 46
|
ge0p1rpd |
|- ( ph -> ( ( A ` B ) + 1 ) e. RR+ ) |
48 |
47
|
rpred |
|- ( ph -> ( ( A ` B ) + 1 ) e. RR ) |
49 |
2 4
|
mscl |
|- ( ( W e. MetSp /\ X e. V /\ Y e. V ) -> ( X D Y ) e. RR ) |
50 |
22 14 16 49
|
syl3anc |
|- ( ph -> ( X D Y ) e. RR ) |
51 |
48 50
|
remulcld |
|- ( ph -> ( ( ( A ` B ) + 1 ) x. ( X D Y ) ) e. RR ) |
52 |
38
|
rehalfcld |
|- ( ph -> ( R / 2 ) e. RR ) |
53 |
2 8 1 3 4 7
|
nlmdsdi |
|- ( ( W e. NrmMod /\ ( B e. K /\ X e. V /\ Y e. V ) ) -> ( ( A ` B ) x. ( X D Y ) ) = ( ( B .x. X ) D ( B .x. Y ) ) ) |
54 |
11 13 14 16 53
|
syl13anc |
|- ( ph -> ( ( A ` B ) x. ( X D Y ) ) = ( ( B .x. X ) D ( B .x. Y ) ) ) |
55 |
|
msxms |
|- ( W e. MetSp -> W e. *MetSp ) |
56 |
22 55
|
syl |
|- ( ph -> W e. *MetSp ) |
57 |
2 4
|
xmsge0 |
|- ( ( W e. *MetSp /\ X e. V /\ Y e. V ) -> 0 <_ ( X D Y ) ) |
58 |
56 14 16 57
|
syl3anc |
|- ( ph -> 0 <_ ( X D Y ) ) |
59 |
44
|
lep1d |
|- ( ph -> ( A ` B ) <_ ( ( A ` B ) + 1 ) ) |
60 |
44 48 50 58 59
|
lemul1ad |
|- ( ph -> ( ( A ` B ) x. ( X D Y ) ) <_ ( ( ( A ` B ) + 1 ) x. ( X D Y ) ) ) |
61 |
54 60
|
eqbrtrrd |
|- ( ph -> ( ( B .x. X ) D ( B .x. Y ) ) <_ ( ( ( A ` B ) + 1 ) x. ( X D Y ) ) ) |
62 |
18 9
|
breqtrdi |
|- ( ph -> ( X D Y ) < ( ( R / 2 ) / ( ( A ` B ) + 1 ) ) ) |
63 |
50 52 47
|
ltmuldiv2d |
|- ( ph -> ( ( ( ( A ` B ) + 1 ) x. ( X D Y ) ) < ( R / 2 ) <-> ( X D Y ) < ( ( R / 2 ) / ( ( A ` B ) + 1 ) ) ) ) |
64 |
62 63
|
mpbird |
|- ( ph -> ( ( ( A ` B ) + 1 ) x. ( X D Y ) ) < ( R / 2 ) ) |
65 |
34 51 52 61 64
|
lelttrd |
|- ( ph -> ( ( B .x. X ) D ( B .x. Y ) ) < ( R / 2 ) ) |
66 |
|
ngpms |
|- ( F e. NrmGrp -> F e. MetSp ) |
67 |
42 66
|
syl |
|- ( ph -> F e. MetSp ) |
68 |
3 5
|
mscl |
|- ( ( F e. MetSp /\ B e. K /\ C e. K ) -> ( B E C ) e. RR ) |
69 |
67 13 15 68
|
syl3anc |
|- ( ph -> ( B E C ) e. RR ) |
70 |
2 6
|
nmcl |
|- ( ( W e. NrmGrp /\ X e. V ) -> ( N ` X ) e. RR ) |
71 |
20 14 70
|
syl2anc |
|- ( ph -> ( N ` X ) e. RR ) |
72 |
12
|
rphalfcld |
|- ( ph -> ( R / 2 ) e. RR+ ) |
73 |
72 47
|
rpdivcld |
|- ( ph -> ( ( R / 2 ) / ( ( A ` B ) + 1 ) ) e. RR+ ) |
74 |
9 73
|
eqeltrid |
|- ( ph -> T e. RR+ ) |
75 |
74
|
rpred |
|- ( ph -> T e. RR ) |
76 |
71 75
|
readdcld |
|- ( ph -> ( ( N ` X ) + T ) e. RR ) |
77 |
69 76
|
remulcld |
|- ( ph -> ( ( B E C ) x. ( ( N ` X ) + T ) ) e. RR ) |
78 |
2 8 1 3 4 6 5
|
nlmdsdir |
|- ( ( W e. NrmMod /\ ( B e. K /\ C e. K /\ Y e. V ) ) -> ( ( B E C ) x. ( N ` Y ) ) = ( ( B .x. Y ) D ( C .x. Y ) ) ) |
79 |
11 13 15 16 78
|
syl13anc |
|- ( ph -> ( ( B E C ) x. ( N ` Y ) ) = ( ( B .x. Y ) D ( C .x. Y ) ) ) |
80 |
2 6
|
nmcl |
|- ( ( W e. NrmGrp /\ Y e. V ) -> ( N ` Y ) e. RR ) |
81 |
20 16 80
|
syl2anc |
|- ( ph -> ( N ` Y ) e. RR ) |
82 |
|
msxms |
|- ( F e. MetSp -> F e. *MetSp ) |
83 |
67 82
|
syl |
|- ( ph -> F e. *MetSp ) |
84 |
3 5
|
xmsge0 |
|- ( ( F e. *MetSp /\ B e. K /\ C e. K ) -> 0 <_ ( B E C ) ) |
85 |
83 13 15 84
|
syl3anc |
|- ( ph -> 0 <_ ( B E C ) ) |
86 |
81 71
|
resubcld |
|- ( ph -> ( ( N ` Y ) - ( N ` X ) ) e. RR ) |
87 |
|
eqid |
|- ( -g ` W ) = ( -g ` W ) |
88 |
2 6 87
|
nm2dif |
|- ( ( W e. NrmGrp /\ Y e. V /\ X e. V ) -> ( ( N ` Y ) - ( N ` X ) ) <_ ( N ` ( Y ( -g ` W ) X ) ) ) |
89 |
20 16 14 88
|
syl3anc |
|- ( ph -> ( ( N ` Y ) - ( N ` X ) ) <_ ( N ` ( Y ( -g ` W ) X ) ) ) |
90 |
6 2 87 4
|
ngpdsr |
|- ( ( W e. NrmGrp /\ X e. V /\ Y e. V ) -> ( X D Y ) = ( N ` ( Y ( -g ` W ) X ) ) ) |
91 |
20 14 16 90
|
syl3anc |
|- ( ph -> ( X D Y ) = ( N ` ( Y ( -g ` W ) X ) ) ) |
92 |
89 91
|
breqtrrd |
|- ( ph -> ( ( N ` Y ) - ( N ` X ) ) <_ ( X D Y ) ) |
93 |
50 75 18
|
ltled |
|- ( ph -> ( X D Y ) <_ T ) |
94 |
86 50 75 92 93
|
letrd |
|- ( ph -> ( ( N ` Y ) - ( N ` X ) ) <_ T ) |
95 |
81 71 75
|
lesubadd2d |
|- ( ph -> ( ( ( N ` Y ) - ( N ` X ) ) <_ T <-> ( N ` Y ) <_ ( ( N ` X ) + T ) ) ) |
96 |
94 95
|
mpbid |
|- ( ph -> ( N ` Y ) <_ ( ( N ` X ) + T ) ) |
97 |
81 76 69 85 96
|
lemul2ad |
|- ( ph -> ( ( B E C ) x. ( N ` Y ) ) <_ ( ( B E C ) x. ( ( N ` X ) + T ) ) ) |
98 |
79 97
|
eqbrtrrd |
|- ( ph -> ( ( B .x. Y ) D ( C .x. Y ) ) <_ ( ( B E C ) x. ( ( N ` X ) + T ) ) ) |
99 |
17 10
|
breqtrdi |
|- ( ph -> ( B E C ) < ( ( R / 2 ) / ( ( N ` X ) + T ) ) ) |
100 |
|
0red |
|- ( ph -> 0 e. RR ) |
101 |
2 6
|
nmge0 |
|- ( ( W e. NrmGrp /\ X e. V ) -> 0 <_ ( N ` X ) ) |
102 |
20 14 101
|
syl2anc |
|- ( ph -> 0 <_ ( N ` X ) ) |
103 |
71 74
|
ltaddrpd |
|- ( ph -> ( N ` X ) < ( ( N ` X ) + T ) ) |
104 |
100 71 76 102 103
|
lelttrd |
|- ( ph -> 0 < ( ( N ` X ) + T ) ) |
105 |
|
ltmuldiv |
|- ( ( ( B E C ) e. RR /\ ( R / 2 ) e. RR /\ ( ( ( N ` X ) + T ) e. RR /\ 0 < ( ( N ` X ) + T ) ) ) -> ( ( ( B E C ) x. ( ( N ` X ) + T ) ) < ( R / 2 ) <-> ( B E C ) < ( ( R / 2 ) / ( ( N ` X ) + T ) ) ) ) |
106 |
69 52 76 104 105
|
syl112anc |
|- ( ph -> ( ( ( B E C ) x. ( ( N ` X ) + T ) ) < ( R / 2 ) <-> ( B E C ) < ( ( R / 2 ) / ( ( N ` X ) + T ) ) ) ) |
107 |
99 106
|
mpbird |
|- ( ph -> ( ( B E C ) x. ( ( N ` X ) + T ) ) < ( R / 2 ) ) |
108 |
36 77 52 98 107
|
lelttrd |
|- ( ph -> ( ( B .x. Y ) D ( C .x. Y ) ) < ( R / 2 ) ) |
109 |
34 36 38 65 108
|
lt2halvesd |
|- ( ph -> ( ( ( B .x. X ) D ( B .x. Y ) ) + ( ( B .x. Y ) D ( C .x. Y ) ) ) < R ) |
110 |
30 37 38 40 109
|
lelttrd |
|- ( ph -> ( ( B .x. X ) D ( C .x. Y ) ) < R ) |