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 )