Metamath Proof Explorer

Theorem nlmvscnlem2

Description: Lemma for nlmvscn . Compare this proof with the similar elementary proof mulcn2 for continuity of multiplication on CC . (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nlmvscn.f 
|- F = ( Scalar ` W )
nlmvscn.v 
|- V = ( Base ` W )
nlmvscn.k 
|- K = ( Base ` F )
nlmvscn.d 
|- D = ( dist ` W )
nlmvscn.e 
|- E = ( dist ` F )
nlmvscn.n 
|- N = ( norm ` W )
nlmvscn.a 
|- A = ( norm ` F )
nlmvscn.s 
|- .x. = ( .s ` W )
nlmvscn.t 
|- T = ( ( R / 2 ) / ( ( A ` B ) + 1 ) )
nlmvscn.u 
|- U = ( ( R / 2 ) / ( ( N ` X ) + T ) )
nlmvscn.w 
|- ( ph -> W e. NrmMod )
nlmvscn.r 
|- ( ph -> R e. RR+ )
nlmvscn.b 
|- ( ph -> B e. K )
nlmvscn.x 
|- ( ph -> X e. V )
nlmvscn.c 
|- ( ph -> C e. K )
nlmvscn.y 
|- ( ph -> Y e. V )
nlmvscn.1 
|- ( ph -> ( B E C ) < U )
nlmvscn.2 
|- ( ph -> ( X D Y ) < T )
Assertion nlmvscnlem2 
|- ( ph -> ( ( B .x. X ) D ( C .x. Y ) ) < R )

Proof

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 )