This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipblnfi

Description: A function F generated by varying the first argument of an inner product (with its second argument a fixed vector A ) is a bounded linear functional, i.e. a bounded linear operator from the vector space to CC . (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ipblnfi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ipblnfi.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ipblnfi.9 ⊢ 𝑈 ∈ CPreHilOLD
ipblnfi.c ⊢ 𝐶 = ⟨ ⟨ + , · ⟩ , abs ⟩
ipblnfi.l ⊢ 𝐵 = ( 𝑈 BLnOp 𝐶 )
ipblnfi.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝑃 𝐴 ) )
Assertion ipblnfi ( 𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ipblnfi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ipblnfi.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3 ipblnfi.9 ⊢ 𝑈 ∈ CPreHilOLD
4 ipblnfi.c ⊢ 𝐶 = ⟨ ⟨ + , · ⟩ , abs ⟩
5 ipblnfi.l ⊢ 𝐵 = ( 𝑈 BLnOp 𝐶 )
6 ipblnfi.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝑃 𝐴 ) )
7 3 phnvi ⊢ 𝑈 ∈ NrmCVec
8 1 2 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑃 𝐴 ) ∈ ℂ )
9 7 8 mp3an1 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑃 𝐴 ) ∈ ℂ )
10 9 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝑃 𝐴 ) ∈ ℂ )
11 10 6 fmptd ⊢ ( 𝐴 ∈ 𝑋 → 𝐹 : 𝑋 ⟶ ℂ )
12 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
13 1 12 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
14 7 13 mp3an1 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
15 14 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
16 simprr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑤 ∈ 𝑋 )
17 simpll ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
18 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
19 1 18 2 dipdir ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) )
20 3 19 mpan ⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) )
21 15 16 17 20 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) )
22 simplr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑦 ∈ ℂ )
23 simprl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
24 1 18 12 2 3 ipassi ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) = ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) )
25 22 23 17 24 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) = ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) )
26 25 oveq1d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) 𝑃 𝐴 ) + ( 𝑤 𝑃 𝐴 ) ) = ( ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) + ( 𝑤 𝑃 𝐴 ) ) )
27 21 26 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) = ( ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) + ( 𝑤 𝑃 𝐴 ) ) )
28 14 adantll ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 )
29 1 18 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
30 7 29 mp3an1 ⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
31 28 30 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
32 31 anasss ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
33 oveq1 ⊢ ( 𝑥 = ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) → ( 𝑥 𝑃 𝐴 ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) )
34 ovex ⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) ∈ V
35 33 6 34 fvmpt ⊢ ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 → ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) )
36 32 35 syl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) 𝑃 𝐴 ) )
37 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑃 𝐴 ) = ( 𝑧 𝑃 𝐴 ) )
38 ovex ⊢ ( 𝑧 𝑃 𝐴 ) ∈ V
39 37 6 38 fvmpt ⊢ ( 𝑧 ∈ 𝑋 → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝑃 𝐴 ) )
40 39 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝑃 𝐴 ) )
41 40 oveq2d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) = ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) )
42 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝑃 𝐴 ) = ( 𝑤 𝑃 𝐴 ) )
43 ovex ⊢ ( 𝑤 𝑃 𝐴 ) ∈ V
44 42 6 43 fvmpt ⊢ ( 𝑤 ∈ 𝑋 → ( 𝐹 ‘ 𝑤 ) = ( 𝑤 𝑃 𝐴 ) )
45 44 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝑤 𝑃 𝐴 ) )
46 41 45 oveq12d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝑦 · ( 𝑧 𝑃 𝐴 ) ) + ( 𝑤 𝑃 𝐴 ) ) )
47 27 36 46 3eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) )
48 47 ralrimivva ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) )
49 48 ralrimiva ⊢ ( 𝐴 ∈ 𝑋 → ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) )
50 4 cnnv ⊢ 𝐶 ∈ NrmCVec
51 4 cnnvba ⊢ ℂ = ( BaseSet ‘ 𝐶 )
52 4 cnnvg ⊢ + = ( +𝑣 ‘ 𝐶 )
53 4 cnnvs ⊢ · = ( ·𝑠OLD ‘ 𝐶 )
54 eqid ⊢ ( 𝑈 LnOp 𝐶 ) = ( 𝑈 LnOp 𝐶 )
55 1 51 18 52 12 53 54 islno ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ NrmCVec ) → ( 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) ↔ ( 𝐹 : 𝑋 ⟶ ℂ ∧ ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) ) ) )
56 7 50 55 mp2an ⊢ ( 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) ↔ ( 𝐹 : 𝑋 ⟶ ℂ ∧ ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝐹 ‘ ( ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑧 ) ( +𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑦 · ( 𝐹 ‘ 𝑧 ) ) + ( 𝐹 ‘ 𝑤 ) ) ) )
57 11 49 56 sylanbrc ⊢ ( 𝐴 ∈ 𝑋 → 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) )
58 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
59 1 58 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ )
60 7 59 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ )
61 1 58 2 3 sii ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( abs ‘ ( 𝑧 𝑃 𝐴 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
62 61 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( abs ‘ ( 𝑧 𝑃 𝐴 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
63 39 adantl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 𝑃 𝐴 ) )
64 63 fveq2d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) = ( abs ‘ ( 𝑧 𝑃 𝐴 ) ) )
65 60 recnd ⊢ ( 𝐴 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℂ )
66 1 58 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
67 7 66 mpan ⊢ ( 𝑧 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℝ )
68 67 recnd ⊢ ( 𝑧 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ )
69 mulcom ⊢ ( ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
70 65 68 69 syl2an ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ) )
71 62 64 70 3brtr4d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
72 71 ralrimiva ⊢ ( 𝐴 ∈ 𝑋 → ∀ 𝑧 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) )
73 4 cnnvnm ⊢ abs = ( normCV ‘ 𝐶 )
74 1 58 73 54 5 7 50 blo3i ⊢ ( ( 𝐹 ∈ ( 𝑈 LnOp 𝐶 ) ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑧 ) ) ) → 𝐹 ∈ 𝐵 )
75 57 60 72 74 syl3anc ⊢ ( 𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵 )