Metamath Proof Explorer

Theorem nmlno0lem

Description: Lemma for nmlno0i . (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmlno0.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmlno0.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
nmlno0.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
nmlno0lem.u ⊢ 𝑈 ∈ NrmCVec
nmlno0lem.w ⊢ 𝑊 ∈ NrmCVec
nmlno0lem.l ⊢ 𝑇 ∈ 𝐿
nmlno0lem.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmlno0lem.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmlno0lem.r ⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
nmlno0lem.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
nmlno0lem.p ⊢ 𝑃 = ( 0vec ‘ 𝑈 )
nmlno0lem.q ⊢ 𝑄 = ( 0vec ‘ 𝑊 )
nmlno0lem.k ⊢ 𝐾 = ( normCV ‘ 𝑈 )
nmlno0lem.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
Assertion nmlno0lem ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ 𝑇 = 𝑍 )

Proof

Step Hyp Ref Expression
1 nmlno0.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2 nmlno0.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
3 nmlno0.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
4 nmlno0lem.u ⊢ 𝑈 ∈ NrmCVec
5 nmlno0lem.w ⊢ 𝑊 ∈ NrmCVec
6 nmlno0lem.l ⊢ 𝑇 ∈ 𝐿
7 nmlno0lem.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
8 nmlno0lem.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
9 nmlno0lem.r ⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
10 nmlno0lem.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
11 nmlno0lem.p ⊢ 𝑃 = ( 0vec ‘ 𝑈 )
12 nmlno0lem.q ⊢ 𝑄 = ( 0vec ‘ 𝑊 )
13 nmlno0lem.k ⊢ 𝐾 = ( normCV ‘ 𝑈 )
14 nmlno0lem.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
15 7 13 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( 𝐾 ‘ 𝑥 ) ∈ ℝ )
16 4 15 mpan ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐾 ‘ 𝑥 ) ∈ ℝ )
17 16 recnd ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐾 ‘ 𝑥 ) ∈ ℂ )
18 17 adantr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝐾 ‘ 𝑥 ) ∈ ℂ )
19 7 11 13 nvz ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐾 ‘ 𝑥 ) = 0 ↔ 𝑥 = 𝑃 ) )
20 4 19 mpan ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐾 ‘ 𝑥 ) = 0 ↔ 𝑥 = 𝑃 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑃 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑃 ) )
22 7 8 11 12 3 lno0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑃 ) = 𝑄 )
23 4 5 6 22 mp3an ⊢ ( 𝑇 ‘ 𝑃 ) = 𝑄
24 21 23 eqtrdi ⊢ ( 𝑥 = 𝑃 → ( 𝑇 ‘ 𝑥 ) = 𝑄 )
25 20 24 syl6bi ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐾 ‘ 𝑥 ) = 0 → ( 𝑇 ‘ 𝑥 ) = 𝑄 ) )
26 25 necon3d ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 → ( 𝐾 ‘ 𝑥 ) ≠ 0 ) )
27 26 imp ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝐾 ‘ 𝑥 ) ≠ 0 )
28 18 27 recne0d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 1 / ( 𝐾 ‘ 𝑥 ) ) ≠ 0 )
29 simpr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 )
30 18 27 reccld ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ )
31 7 8 3 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ 𝑌 )
32 4 5 6 31 mp3an ⊢ 𝑇 : 𝑋 ⟶ 𝑌
33 32 ffvelrni ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 )
34 33 adantr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 )
35 8 10 12 nvmul0or ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) = 𝑄 ↔ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 𝑄 ) ) )
36 5 35 mp3an1 ⊢ ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) = 𝑄 ↔ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 𝑄 ) ) )
37 30 34 36 syl2anc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) = 𝑄 ↔ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 𝑄 ) ) )
38 37 necon3abid ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ≠ 𝑄 ↔ ¬ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 𝑄 ) ) )
39 neanior ⊢ ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ≠ 0 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) ↔ ¬ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) = 0 ∨ ( 𝑇 ‘ 𝑥 ) = 𝑄 ) )
40 38 39 bitr4di ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ≠ 𝑄 ↔ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ≠ 0 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) ) )
41 28 29 40 mpbir2and ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ≠ 𝑄 )
42 8 10 nvscl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ∈ 𝑌 )
43 5 42 mp3an1 ⊢ ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑌 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ∈ 𝑌 )
44 30 34 43 syl2anc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ∈ 𝑌 )
45 8 12 14 nvgt0 ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ∈ 𝑌 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ≠ 𝑄 ↔ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
46 5 44 45 sylancr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ≠ 𝑄 ↔ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
47 41 46 mpbid ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) )
48 47 ex ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 → 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
49 48 adantl ⊢ ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 → 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
50 8 14 nmosetre ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )
51 5 32 50 mp2an ⊢ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ
52 ressxr ⊢ ℝ ⊆ ℝ*
53 51 52 sstri ⊢ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ*
54 simpl ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → 𝑥 ∈ 𝑋 )
55 7 9 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ∈ 𝑋 )
56 4 55 mp3an1 ⊢ ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ∈ 𝑋 )
57 30 54 56 syl2anc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ∈ 𝑋 )
58 24 necon3i ⊢ ( ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 → 𝑥 ≠ 𝑃 )
59 7 9 11 13 nv1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑃 ) → ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = 1 )
60 4 59 mp3an1 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑃 ) → ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = 1 )
61 58 60 sylan2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = 1 )
62 1re ⊢ 1 ∈ ℝ
63 61 62 eqeltrdi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ∈ ℝ )
64 eqle ⊢ ( ( ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ∈ ℝ ∧ ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = 1 ) → ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ≤ 1 )
65 63 61 64 syl2anc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ≤ 1 )
66 4 5 6 3pm3.2i ⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 )
67 7 9 10 3 lnomul ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) )
68 66 67 mpan ⊢ ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) )
69 30 54 68 syl2anc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) )
70 69 eqcomd ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) = ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) )
71 70 fveq2d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ) )
72 fveq2 ⊢ ( 𝑧 = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) → ( 𝐾 ‘ 𝑧 ) = ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) )
73 72 breq1d ⊢ ( 𝑧 = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) → ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ↔ ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ≤ 1 ) )
74 2fveq3 ⊢ ( 𝑧 = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ) )
75 74 eqeq2d ⊢ ( 𝑧 = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) → ( ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ↔ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ) ) )
76 73 75 anbi12d ⊢ ( 𝑧 = ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) → ( ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ) ) ) )
77 76 rspcev ⊢ ( ( ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ∈ 𝑋 ∧ ( ( 𝐾 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑅 𝑥 ) ) ) ) ) → ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
78 57 65 71 77 syl12anc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
79 fvex ⊢ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ V
80 eqeq1 ⊢ ( 𝑦 = ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ↔ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
81 80 anbi2d ⊢ ( 𝑦 = ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) → ( ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) )
82 81 rexbidv ⊢ ( 𝑦 = ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) → ( ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) )
83 79 82 elab ⊢ ( ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) )
84 78 83 sylibr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } )
85 supxrub ⊢ ( ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ* ∧ ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
86 53 84 85 sylancr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
87 86 adantll ⊢ ( ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
88 7 8 13 14 1 nmooval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
89 4 5 32 88 mp3an ⊢ ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < )
90 89 eqeq1i ⊢ ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) = 0 )
91 90 biimpi ⊢ ( ( 𝑁 ‘ 𝑇 ) = 0 → sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) = 0 )
92 91 ad2antrr ⊢ ( ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → sup ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐾 ‘ 𝑧 ) ≤ 1 ∧ 𝑦 = ( 𝑀 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ* , < ) = 0 )
93 87 92 breqtrd ⊢ ( ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 )
94 8 14 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ∈ 𝑌 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
95 5 44 94 sylancr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
96 0re ⊢ 0 ∈ ℝ
97 lenlt ⊢ ( ( ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
98 95 96 97 sylancl ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
99 98 adantll ⊢ ( ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ( ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
100 93 99 mpbid ⊢ ( ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ) → ¬ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) )
101 100 ex ⊢ ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 → ¬ 0 < ( 𝑀 ‘ ( ( 1 / ( 𝐾 ‘ 𝑥 ) ) 𝑆 ( 𝑇 ‘ 𝑥 ) ) ) ) )
102 49 101 pm2.65d ⊢ ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) → ¬ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 )
103 nne ⊢ ( ¬ ( 𝑇 ‘ 𝑥 ) ≠ 𝑄 ↔ ( 𝑇 ‘ 𝑥 ) = 𝑄 )
104 102 103 sylib ⊢ ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑥 ) = 𝑄 )
105 7 12 2 0oval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( 𝑍 ‘ 𝑥 ) = 𝑄 )
106 4 5 105 mp3an12 ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑍 ‘ 𝑥 ) = 𝑄 )
107 106 adantl ⊢ ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑍 ‘ 𝑥 ) = 𝑄 )
108 104 107 eqtr4d ⊢ ( ( ( 𝑁 ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑍 ‘ 𝑥 ) )
109 108 ralrimiva ⊢ ( ( 𝑁 ‘ 𝑇 ) = 0 → ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 𝑍 ‘ 𝑥 ) )
110 ffn ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → 𝑇 Fn 𝑋 )
111 32 110 ax-mp ⊢ 𝑇 Fn 𝑋
112 7 8 2 0oo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : 𝑋 ⟶ 𝑌 )
113 4 5 112 mp2an ⊢ 𝑍 : 𝑋 ⟶ 𝑌
114 ffn ⊢ ( 𝑍 : 𝑋 ⟶ 𝑌 → 𝑍 Fn 𝑋 )
115 113 114 ax-mp ⊢ 𝑍 Fn 𝑋
116 eqfnfv ⊢ ( ( 𝑇 Fn 𝑋 ∧ 𝑍 Fn 𝑋 ) → ( 𝑇 = 𝑍 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 𝑍 ‘ 𝑥 ) ) )
117 111 115 116 mp2an ⊢ ( 𝑇 = 𝑍 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 𝑍 ‘ 𝑥 ) )
118 109 117 sylibr ⊢ ( ( 𝑁 ‘ 𝑇 ) = 0 → 𝑇 = 𝑍 )
119 fveq2 ⊢ ( 𝑇 = 𝑍 → ( 𝑁 ‘ 𝑇 ) = ( 𝑁 ‘ 𝑍 ) )
120 1 2 nmoo0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑁 ‘ 𝑍 ) = 0 )
121 4 5 120 mp2an ⊢ ( 𝑁 ‘ 𝑍 ) = 0
122 119 121 eqtrdi ⊢ ( 𝑇 = 𝑍 → ( 𝑁 ‘ 𝑇 ) = 0 )
123 118 122 impbii ⊢ ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ 𝑇 = 𝑍 )