Metamath Proof Explorer

Theorem nmlno0lem

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

Ref Expression
Hypotheses nmlno0.3 ⊢ N = U normOp OLD W
nmlno0.0 ⊢ Z = U 0 op W
nmlno0.7 ⊢ L = U LnOp W
nmlno0lem.u ⊢ U ∈ NrmCVec
nmlno0lem.w ⊢ W ∈ NrmCVec
nmlno0lem.l ⊢ T ∈ L
nmlno0lem.1 ⊢ X = BaseSet ⁡ U
nmlno0lem.2 ⊢ Y = BaseSet ⁡ W
nmlno0lem.r ⊢ R = ⋅ 𝑠OLD ⁡ U
nmlno0lem.s ⊢ S = ⋅ 𝑠OLD ⁡ W
nmlno0lem.p ⊢ P = 0 vec ⁡ U
nmlno0lem.q ⊢ Q = 0 vec ⁡ W
nmlno0lem.k ⊢ K = norm CV ⁡ U
nmlno0lem.m ⊢ M = norm CV ⁡ W
Assertion nmlno0lem ⊢ N ⁡ T = 0 ↔ T = Z

Proof

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