Metamath Proof Explorer

Theorem nmcvcn

Description: The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007) (Proof shortened by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses nmcvcn.1 ⊒ 𝑁 = ( normCV β€˜ π‘ˆ )
nmcvcn.2 ⊒ 𝐢 = ( IndMet β€˜ π‘ˆ )
nmcvcn.j ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
nmcvcn.k ⊒ 𝐾 = ( topGen β€˜ ran (,) )
Assertion nmcvcn ( π‘ˆ ∈ NrmCVec β†’ 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 nmcvcn.1 ⊒ 𝑁 = ( normCV β€˜ π‘ˆ )
2 nmcvcn.2 ⊒ 𝐢 = ( IndMet β€˜ π‘ˆ )
3 nmcvcn.j ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
4 nmcvcn.k ⊒ 𝐾 = ( topGen β€˜ ran (,) )
5 eqid ⊒ ( BaseSet β€˜ π‘ˆ ) = ( BaseSet β€˜ π‘ˆ )
6 5 1 nvf ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝑁 : ( BaseSet β€˜ π‘ˆ ) ⟢ ℝ )
7 simprr ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ ( π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑒 ∈ ℝ+ ) ) β†’ 𝑒 ∈ ℝ+ )
8 5 1 nvcl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( 𝑁 β€˜ π‘₯ ) ∈ ℝ )
9 8 ex ⊒ ( π‘ˆ ∈ NrmCVec β†’ ( π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) β†’ ( 𝑁 β€˜ π‘₯ ) ∈ ℝ ) )
10 5 1 nvcl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ )
11 10 ex ⊒ ( π‘ˆ ∈ NrmCVec β†’ ( 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) β†’ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ ) )
12 9 11 anim12d ⊒ ( π‘ˆ ∈ NrmCVec β†’ ( ( π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ∈ ℝ ∧ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ ) ) )
13 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
14 13 remet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( Met β€˜ ℝ )
15 metcl ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( Met β€˜ ℝ ) ∧ ( 𝑁 β€˜ π‘₯ ) ∈ ℝ ∧ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ )
16 14 15 mp3an1 ⊒ ( ( ( 𝑁 β€˜ π‘₯ ) ∈ ℝ ∧ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ )
17 12 16 syl6 ⊒ ( π‘ˆ ∈ NrmCVec β†’ ( ( π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ) )
18 17 3impib ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ )
19 5 2 imsmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐢 ∈ ( Met β€˜ ( BaseSet β€˜ π‘ˆ ) ) )
20 metcl ⊒ ( ( 𝐢 ∈ ( Met β€˜ ( BaseSet β€˜ π‘ˆ ) ) ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ )
21 19 20 syl3an1 ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ )
22 eqid ⊒ ( +𝑣 β€˜ π‘ˆ ) = ( +𝑣 β€˜ π‘ˆ )
23 eqid ⊒ ( ·𝑠OLD β€˜ π‘ˆ ) = ( ·𝑠OLD β€˜ π‘ˆ )
24 5 22 23 1 nvabs ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( abs β€˜ ( ( 𝑁 β€˜ π‘₯ ) βˆ’ ( 𝑁 β€˜ 𝑦 ) ) ) ≀ ( 𝑁 β€˜ ( π‘₯ ( +𝑣 β€˜ π‘ˆ ) ( - 1 ( ·𝑠OLD β€˜ π‘ˆ ) 𝑦 ) ) ) )
25 12 3impib ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ∈ ℝ ∧ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ ) )
26 13 remetdval ⊒ ( ( ( 𝑁 β€˜ π‘₯ ) ∈ ℝ ∧ ( 𝑁 β€˜ 𝑦 ) ∈ ℝ ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) = ( abs β€˜ ( ( 𝑁 β€˜ π‘₯ ) βˆ’ ( 𝑁 β€˜ 𝑦 ) ) ) )
27 25 26 syl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) = ( abs β€˜ ( ( 𝑁 β€˜ π‘₯ ) βˆ’ ( 𝑁 β€˜ 𝑦 ) ) ) )
28 5 22 23 1 2 imsdval2 ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( π‘₯ 𝐢 𝑦 ) = ( 𝑁 β€˜ ( π‘₯ ( +𝑣 β€˜ π‘ˆ ) ( - 1 ( ·𝑠OLD β€˜ π‘ˆ ) 𝑦 ) ) ) )
29 24 27 28 3brtr4d ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) )
30 18 21 29 jca31 ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ∧ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) ) )
31 30 3expa ⊒ ( ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ∧ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) ) )
32 rpre ⊒ ( 𝑒 ∈ ℝ+ β†’ 𝑒 ∈ ℝ )
33 lelttr ⊒ ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ∧ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) β†’ ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) ∧ ( π‘₯ 𝐢 𝑦 ) < 𝑒 ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
34 33 3expa ⊒ ( ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ∧ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ ) ∧ 𝑒 ∈ ℝ ) β†’ ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) ∧ ( π‘₯ 𝐢 𝑦 ) < 𝑒 ) β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
35 34 expdimp ⊒ ( ( ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ∧ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ ) ∧ 𝑒 ∈ ℝ ) ∧ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) ) β†’ ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
36 35 an32s ⊒ ( ( ( ( ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ∈ ℝ ∧ ( π‘₯ 𝐢 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) ≀ ( π‘₯ 𝐢 𝑦 ) ) ∧ 𝑒 ∈ ℝ ) β†’ ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
37 31 32 36 syl2an ⊒ ( ( ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) ∧ 𝑒 ∈ ℝ+ ) β†’ ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
38 37 ex ⊒ ( ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ) ∧ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( 𝑒 ∈ ℝ+ β†’ ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) ) )
39 38 ralrimdva ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ) β†’ ( 𝑒 ∈ ℝ+ β†’ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) ) )
40 39 impr ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ ( π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑒 ∈ ℝ+ ) ) β†’ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
41 breq2 ⊒ ( 𝑑 = 𝑒 β†’ ( ( π‘₯ 𝐢 𝑦 ) < 𝑑 ↔ ( π‘₯ 𝐢 𝑦 ) < 𝑒 ) )
42 41 rspceaimv ⊒ ( ( 𝑒 ∈ ℝ+ ∧ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑒 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) ) β†’ βˆƒ 𝑑 ∈ ℝ+ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑑 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
43 7 40 42 syl2anc ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ ( π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) ∧ 𝑒 ∈ ℝ+ ) ) β†’ βˆƒ 𝑑 ∈ ℝ+ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑑 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
44 43 ralrimivva ⊒ ( π‘ˆ ∈ NrmCVec β†’ βˆ€ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) βˆ€ 𝑒 ∈ ℝ+ βˆƒ 𝑑 ∈ ℝ+ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑑 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) )
45 5 2 imsxmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐢 ∈ ( ∞Met β€˜ ( BaseSet β€˜ π‘ˆ ) ) )
46 13 rexmet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ )
47 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
48 13 47 tgioo ⊒ ( topGen β€˜ ran (,) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
49 4 48 eqtri ⊒ 𝐾 = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
50 3 49 metcn ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ ( BaseSet β€˜ π‘ˆ ) ) ∧ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ) β†’ ( 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑁 : ( BaseSet β€˜ π‘ˆ ) ⟢ ℝ ∧ βˆ€ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) βˆ€ 𝑒 ∈ ℝ+ βˆƒ 𝑑 ∈ ℝ+ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑑 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) ) ) )
51 45 46 50 sylancl ⊒ ( π‘ˆ ∈ NrmCVec β†’ ( 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑁 : ( BaseSet β€˜ π‘ˆ ) ⟢ ℝ ∧ βˆ€ π‘₯ ∈ ( BaseSet β€˜ π‘ˆ ) βˆ€ 𝑒 ∈ ℝ+ βˆƒ 𝑑 ∈ ℝ+ βˆ€ 𝑦 ∈ ( BaseSet β€˜ π‘ˆ ) ( ( π‘₯ 𝐢 𝑦 ) < 𝑑 β†’ ( ( 𝑁 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ( 𝑁 β€˜ 𝑦 ) ) < 𝑒 ) ) ) )
52 6 44 51 mpbir2and ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )