Metamath Proof Explorer


Theorem nlmvscnlem1

Description: Lemma for nlmvscn . (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nlmvscn.f 𝐹 = ( Scalar ‘ 𝑊 )
nlmvscn.v 𝑉 = ( Base ‘ 𝑊 )
nlmvscn.k 𝐾 = ( Base ‘ 𝐹 )
nlmvscn.d 𝐷 = ( dist ‘ 𝑊 )
nlmvscn.e 𝐸 = ( dist ‘ 𝐹 )
nlmvscn.n 𝑁 = ( norm ‘ 𝑊 )
nlmvscn.a 𝐴 = ( norm ‘ 𝐹 )
nlmvscn.s · = ( ·𝑠𝑊 )
nlmvscn.t 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝐴𝐵 ) + 1 ) )
nlmvscn.u 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁𝑋 ) + 𝑇 ) )
nlmvscn.w ( 𝜑𝑊 ∈ NrmMod )
nlmvscn.r ( 𝜑𝑅 ∈ ℝ+ )
nlmvscn.b ( 𝜑𝐵𝐾 )
nlmvscn.x ( 𝜑𝑋𝑉 )
Assertion nlmvscnlem1 ( 𝜑 → ∃ 𝑟 ∈ ℝ+𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 nlmvscn.f 𝐹 = ( Scalar ‘ 𝑊 )
2 nlmvscn.v 𝑉 = ( Base ‘ 𝑊 )
3 nlmvscn.k 𝐾 = ( Base ‘ 𝐹 )
4 nlmvscn.d 𝐷 = ( dist ‘ 𝑊 )
5 nlmvscn.e 𝐸 = ( dist ‘ 𝐹 )
6 nlmvscn.n 𝑁 = ( norm ‘ 𝑊 )
7 nlmvscn.a 𝐴 = ( norm ‘ 𝐹 )
8 nlmvscn.s · = ( ·𝑠𝑊 )
9 nlmvscn.t 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝐴𝐵 ) + 1 ) )
10 nlmvscn.u 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁𝑋 ) + 𝑇 ) )
11 nlmvscn.w ( 𝜑𝑊 ∈ NrmMod )
12 nlmvscn.r ( 𝜑𝑅 ∈ ℝ+ )
13 nlmvscn.b ( 𝜑𝐵𝐾 )
14 nlmvscn.x ( 𝜑𝑋𝑉 )
15 12 rphalfcld ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ+ )
16 1 nlmngp2 ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )
17 11 16 syl ( 𝜑𝐹 ∈ NrmGrp )
18 3 7 nmcl ( ( 𝐹 ∈ NrmGrp ∧ 𝐵𝐾 ) → ( 𝐴𝐵 ) ∈ ℝ )
19 17 13 18 syl2anc ( 𝜑 → ( 𝐴𝐵 ) ∈ ℝ )
20 3 7 nmge0 ( ( 𝐹 ∈ NrmGrp ∧ 𝐵𝐾 ) → 0 ≤ ( 𝐴𝐵 ) )
21 17 13 20 syl2anc ( 𝜑 → 0 ≤ ( 𝐴𝐵 ) )
22 19 21 ge0p1rpd ( 𝜑 → ( ( 𝐴𝐵 ) + 1 ) ∈ ℝ+ )
23 15 22 rpdivcld ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝐴𝐵 ) + 1 ) ) ∈ ℝ+ )
24 9 23 eqeltrid ( 𝜑𝑇 ∈ ℝ+ )
25 nlmngp ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
26 11 25 syl ( 𝜑𝑊 ∈ NrmGrp )
27 2 6 nmcl ( ( 𝑊 ∈ NrmGrp ∧ 𝑋𝑉 ) → ( 𝑁𝑋 ) ∈ ℝ )
28 26 14 27 syl2anc ( 𝜑 → ( 𝑁𝑋 ) ∈ ℝ )
29 24 rpred ( 𝜑𝑇 ∈ ℝ )
30 28 29 readdcld ( 𝜑 → ( ( 𝑁𝑋 ) + 𝑇 ) ∈ ℝ )
31 0red ( 𝜑 → 0 ∈ ℝ )
32 2 6 nmge0 ( ( 𝑊 ∈ NrmGrp ∧ 𝑋𝑉 ) → 0 ≤ ( 𝑁𝑋 ) )
33 26 14 32 syl2anc ( 𝜑 → 0 ≤ ( 𝑁𝑋 ) )
34 28 24 ltaddrpd ( 𝜑 → ( 𝑁𝑋 ) < ( ( 𝑁𝑋 ) + 𝑇 ) )
35 31 28 30 33 34 lelttrd ( 𝜑 → 0 < ( ( 𝑁𝑋 ) + 𝑇 ) )
36 30 35 elrpd ( 𝜑 → ( ( 𝑁𝑋 ) + 𝑇 ) ∈ ℝ+ )
37 15 36 rpdivcld ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝑁𝑋 ) + 𝑇 ) ) ∈ ℝ+ )
38 10 37 eqeltrid ( 𝜑𝑈 ∈ ℝ+ )
39 24 38 ifcld ( 𝜑 → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ )
40 11 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ NrmMod )
41 12 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑅 ∈ ℝ+ )
42 13 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐵𝐾 )
43 14 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑋𝑉 )
44 simprll ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑥𝐾 )
45 simprlr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑦𝑉 )
46 17 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐹 ∈ NrmGrp )
47 ngpms ( 𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp )
48 46 47 syl ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐹 ∈ MetSp )
49 3 5 mscl ( ( 𝐹 ∈ MetSp ∧ 𝐵𝐾𝑥𝐾 ) → ( 𝐵 𝐸 𝑥 ) ∈ ℝ )
50 48 42 44 49 syl3anc ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐸 𝑥 ) ∈ ℝ )
51 39 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ )
52 51 rpred ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∈ ℝ )
53 38 rpred ( 𝜑𝑈 ∈ ℝ )
54 53 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑈 ∈ ℝ )
55 simprrl ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) )
56 29 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑇 ∈ ℝ )
57 min2 ( ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ≤ 𝑈 )
58 56 54 57 syl2anc ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ≤ 𝑈 )
59 50 52 54 55 58 ltletrd ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐸 𝑥 ) < 𝑈 )
60 ngpms ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
61 26 60 syl ( 𝜑𝑊 ∈ MetSp )
62 61 adantr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ MetSp )
63 2 4 mscl ( ( 𝑊 ∈ MetSp ∧ 𝑋𝑉𝑦𝑉 ) → ( 𝑋 𝐷 𝑦 ) ∈ ℝ )
64 62 43 45 63 syl3anc ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝑋 𝐷 𝑦 ) ∈ ℝ )
65 simprrr ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) )
66 min1 ( ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ≤ 𝑇 )
67 56 54 66 syl2anc ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ≤ 𝑇 )
68 64 52 56 65 67 ltletrd ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < 𝑇 )
69 1 2 3 4 5 6 7 8 9 10 40 41 42 43 44 45 59 68 nlmvscnlem2 ( ( 𝜑 ∧ ( ( 𝑥𝐾𝑦𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 )
70 69 expr ( ( 𝜑 ∧ ( 𝑥𝐾𝑦𝑉 ) ) → ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )
71 70 ralrimivva ( 𝜑 → ∀ 𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )
72 breq2 ( 𝑟 = if ( 𝑇𝑈 , 𝑇 , 𝑈 ) → ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ↔ ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) )
73 breq2 ( 𝑟 = if ( 𝑇𝑈 , 𝑇 , 𝑈 ) → ( ( 𝑋 𝐷 𝑦 ) < 𝑟 ↔ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) )
74 72 73 anbi12d ( 𝑟 = if ( 𝑇𝑈 , 𝑇 , 𝑈 ) → ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) ↔ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) ) )
75 74 imbi1d ( 𝑟 = if ( 𝑇𝑈 , 𝑇 , 𝑈 ) → ( ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ↔ ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ) )
76 75 2ralbidv ( 𝑟 = if ( 𝑇𝑈 , 𝑇 , 𝑈 ) → ( ∀ 𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ↔ ∀ 𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ) )
77 76 rspcev ( ( if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ ∧ ∀ 𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ) → ∃ 𝑟 ∈ ℝ+𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )
78 39 71 77 syl2anc ( 𝜑 → ∃ 𝑟 ∈ ℝ+𝑥𝐾𝑦𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )