Metamath Proof Explorer

Theorem nlmvscnlem1

Description: Lemma for nlmvscn . (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 )
Assertion nlmvscnlem1 
|- ( ph -> E. r e. RR+ A. x e. K A. y e. V ( ( ( B E x ) < r /\ ( X D y ) < r ) -> ( ( B .x. X ) D ( x .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 12 rphalfcld 
 |-  ( ph -> ( R / 2 ) e. RR+ )
16 1 nlmngp2 
 |-  ( W e. NrmMod -> F e. NrmGrp )
17 11 16 syl 
 |-  ( ph -> F e. NrmGrp )
18 3 7 nmcl 
 |-  ( ( F e. NrmGrp /\ B e. K ) -> ( A ` B ) e. RR )
19 17 13 18 syl2anc 
 |-  ( ph -> ( A ` B ) e. RR )
20 3 7 nmge0 
 |-  ( ( F e. NrmGrp /\ B e. K ) -> 0 <_ ( A ` B ) )
21 17 13 20 syl2anc 
 |-  ( ph -> 0 <_ ( A ` B ) )
22 19 21 ge0p1rpd 
 |-  ( ph -> ( ( A ` B ) + 1 ) e. RR+ )
23 15 22 rpdivcld 
 |-  ( ph -> ( ( R / 2 ) / ( ( A ` B ) + 1 ) ) e. RR+ )
24 9 23 eqeltrid 
 |-  ( ph -> T e. RR+ )
25 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
26 11 25 syl 
 |-  ( ph -> W e. NrmGrp )
27 2 6 nmcl 
 |-  ( ( W e. NrmGrp /\ X e. V ) -> ( N ` X ) e. RR )
28 26 14 27 syl2anc 
 |-  ( ph -> ( N ` X ) e. RR )
29 24 rpred 
 |-  ( ph -> T e. RR )
30 28 29 readdcld 
 |-  ( ph -> ( ( N ` X ) + T ) e. RR )
31 0red 
 |-  ( ph -> 0 e. RR )
32 2 6 nmge0 
 |-  ( ( W e. NrmGrp /\ X e. V ) -> 0 <_ ( N ` X ) )
33 26 14 32 syl2anc 
 |-  ( ph -> 0 <_ ( N ` X ) )
34 28 24 ltaddrpd 
 |-  ( ph -> ( N ` X ) < ( ( N ` X ) + T ) )
35 31 28 30 33 34 lelttrd 
 |-  ( ph -> 0 < ( ( N ` X ) + T ) )
36 30 35 elrpd 
 |-  ( ph -> ( ( N ` X ) + T ) e. RR+ )
37 15 36 rpdivcld 
 |-  ( ph -> ( ( R / 2 ) / ( ( N ` X ) + T ) ) e. RR+ )
38 10 37 eqeltrid 
 |-  ( ph -> U e. RR+ )
39 24 38 ifcld 
 |-  ( ph -> if ( T <_ U , T , U ) e. RR+ )
40 11 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> W e. NrmMod )
41 12 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> R e. RR+ )
42 13 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> B e. K )
43 14 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> X e. V )
44 simprll 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> x e. K )
45 simprlr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> y e. V )
46 17 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> F e. NrmGrp )
47 ngpms 
 |-  ( F e. NrmGrp -> F e. MetSp )
48 46 47 syl 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> F e. MetSp )
49 3 5 mscl 
 |-  ( ( F e. MetSp /\ B e. K /\ x e. K ) -> ( B E x ) e. RR )
50 48 42 44 49 syl3anc 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( B E x ) e. RR )
51 39 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) e. RR+ )
52 51 rpred 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) e. RR )
53 38 rpred 
 |-  ( ph -> U e. RR )
54 53 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> U e. RR )
55 simprrl 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( B E x ) < if ( T <_ U , T , U ) )
56 29 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> T e. RR )
57 min2 
 |-  ( ( T e. RR /\ U e. RR ) -> if ( T <_ U , T , U ) <_ U )
58 56 54 57 syl2anc 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) <_ U )
59 50 52 54 55 58 ltletrd 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( B E x ) < U )
60 ngpms 
 |-  ( W e. NrmGrp -> W e. MetSp )
61 26 60 syl 
 |-  ( ph -> W e. MetSp )
62 61 adantr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> W e. MetSp )
63 2 4 mscl 
 |-  ( ( W e. MetSp /\ X e. V /\ y e. V ) -> ( X D y ) e. RR )
64 62 43 45 63 syl3anc 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( X D y ) e. RR )
65 simprrr 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( X D y ) < if ( T <_ U , T , U ) )
66 min1 
 |-  ( ( T e. RR /\ U e. RR ) -> if ( T <_ U , T , U ) <_ T )
67 56 54 66 syl2anc 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) <_ T )
68 64 52 56 65 67 ltletrd 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( X D y ) < T )
69 1 2 3 4 5 6 7 8 9 10 40 41 42 43 44 45 59 68 nlmvscnlem2 
 |-  ( ( ph /\ ( ( x e. K /\ y e. V ) /\ ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) ) -> ( ( B .x. X ) D ( x .x. y ) ) < R )
70 69 expr 
 |-  ( ( ph /\ ( x e. K /\ y e. V ) ) -> ( ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) )
71 70 ralrimivva 
 |-  ( ph -> A. x e. K A. y e. V ( ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) )
72 breq2 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( B E x ) < r <-> ( B E x ) < if ( T <_ U , T , U ) ) )
73 breq2 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( X D y ) < r <-> ( X D y ) < if ( T <_ U , T , U ) ) )
74 72 73 anbi12d 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( ( B E x ) < r /\ ( X D y ) < r ) <-> ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) ) )
75 74 imbi1d 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( ( ( B E x ) < r /\ ( X D y ) < r ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) <-> ( ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) ) )
76 75 2ralbidv 
 |-  ( r = if ( T <_ U , T , U ) -> ( A. x e. K A. y e. V ( ( ( B E x ) < r /\ ( X D y ) < r ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) <-> A. x e. K A. y e. V ( ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) ) )
77 76 rspcev 
 |-  ( ( if ( T <_ U , T , U ) e. RR+ /\ A. x e. K A. y e. V ( ( ( B E x ) < if ( T <_ U , T , U ) /\ ( X D y ) < if ( T <_ U , T , U ) ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) ) -> E. r e. RR+ A. x e. K A. y e. V ( ( ( B E x ) < r /\ ( X D y ) < r ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) )
78 39 71 77 syl2anc 
 |-  ( ph -> E. r e. RR+ A. x e. K A. y e. V ( ( ( B E x ) < r /\ ( X D y ) < r ) -> ( ( B .x. X ) D ( x .x. y ) ) < R ) )