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=UnormOpOLDW
nmlno0.0 ⊢Z=U0opW
nmlno0.7 ⊢L=ULnOpW
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=0vec⁡U
nmlno0lem.q ⊢Q=0vec⁡W
nmlno0lem.k ⊢K=normCV⁡U
nmlno0lem.m ⊢M=normCV⁡W
Assertion nmlno0lem ⊢N⁡T=0↔T=Z

Proof

Step Hyp Ref Expression
1 nmlno0.3 ⊢N=UnormOpOLDW
2 nmlno0.0 ⊢Z=U0opW
3 nmlno0.7 ⊢L=ULnOpW
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=0vec⁡U
12 nmlno0lem.q ⊢Q=0vec⁡W
13 nmlno0lem.k ⊢K=normCV⁡U
14 nmlno0lem.m ⊢M=normCV⁡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→1K⁡x≠0
29 simpr ⊢x∈X∧T⁡x≠Q→T⁡x≠Q
30 18 27 reccld ⊢x∈X∧T⁡x≠Q→1K⁡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 ffvelcdmi ⊢x∈X→T⁡x∈Y
34 33 adantr ⊢x∈X∧T⁡x≠Q→T⁡x∈Y
35 8 10 12 nvmul0or ⊢W∈NrmCVec∧1K⁡x∈ℂ∧T⁡x∈Y→1K⁡xST⁡x=Q↔1K⁡x=0∨T⁡x=Q
36 5 35 mp3an1 ⊢1K⁡x∈ℂ∧T⁡x∈Y→1K⁡xST⁡x=Q↔1K⁡x=0∨T⁡x=Q
37 30 34 36 syl2anc ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x=Q↔1K⁡x=0∨T⁡x=Q
38 37 necon3abid ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x≠Q↔¬1K⁡x=0∨T⁡x=Q
39 neanior ⊢1K⁡x≠0∧T⁡x≠Q↔¬1K⁡x=0∨T⁡x=Q
40 38 39 bitr4di ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x≠Q↔1K⁡x≠0∧T⁡x≠Q
41 28 29 40 mpbir2and ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x≠Q
42 8 10 nvscl ⊢W∈NrmCVec∧1K⁡x∈ℂ∧T⁡x∈Y→1K⁡xST⁡x∈Y
43 5 42 mp3an1 ⊢1K⁡x∈ℂ∧T⁡x∈Y→1K⁡xST⁡x∈Y
44 30 34 43 syl2anc ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x∈Y
45 8 12 14 nvgt0 ⊢W∈NrmCVec∧1K⁡xST⁡x∈Y→1K⁡xST⁡x≠Q↔0<M⁡1K⁡xST⁡x
46 5 44 45 sylancr ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x≠Q↔0<M⁡1K⁡xST⁡x
47 41 46 mpbid ⊢x∈X∧T⁡x≠Q→0<M⁡1K⁡xST⁡x
48 47 ex ⊢x∈X→T⁡x≠Q→0<M⁡1K⁡xST⁡x
49 48 adantl ⊢N⁡T=0∧x∈X→T⁡x≠Q→0<M⁡1K⁡xST⁡x
50 8 14 nmosetre ⊢W∈NrmCVec∧T:X⟶Y→y|∃z∈XK⁡z≤1∧y=M⁡T⁡z⊆ℝ
51 5 32 50 mp2an ⊢y|∃z∈XK⁡z≤1∧y=M⁡T⁡z⊆ℝ
52 ressxr ⊢ℝ⊆ℝ*
53 51 52 sstri ⊢y|∃z∈XK⁡z≤1∧y=M⁡T⁡z⊆ℝ*
54 simpl ⊢x∈X∧T⁡x≠Q→x∈X
55 7 9 nvscl ⊢U∈NrmCVec∧1K⁡x∈ℂ∧x∈X→1K⁡xRx∈X
56 4 55 mp3an1 ⊢1K⁡x∈ℂ∧x∈X→1K⁡xRx∈X
57 30 54 56 syl2anc ⊢x∈X∧T⁡x≠Q→1K⁡xRx∈X
58 24 necon3i ⊢T⁡x≠Q→x≠P
59 7 9 11 13 nv1 ⊢U∈NrmCVec∧x∈X∧x≠P→K⁡1K⁡xRx=1
60 4 59 mp3an1 ⊢x∈X∧x≠P→K⁡1K⁡xRx=1
61 58 60 sylan2 ⊢x∈X∧T⁡x≠Q→K⁡1K⁡xRx=1
62 1re ⊢1∈ℝ
63 61 62 eqeltrdi ⊢x∈X∧T⁡x≠Q→K⁡1K⁡xRx∈ℝ
64 eqle ⊢K⁡1K⁡xRx∈ℝ∧K⁡1K⁡xRx=1→K⁡1K⁡xRx≤1
65 63 61 64 syl2anc ⊢x∈X∧T⁡x≠Q→K⁡1K⁡xRx≤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∧1K⁡x∈ℂ∧x∈X→T⁡1K⁡xRx=1K⁡xST⁡x
68 66 67 mpan ⊢1K⁡x∈ℂ∧x∈X→T⁡1K⁡xRx=1K⁡xST⁡x
69 30 54 68 syl2anc ⊢x∈X∧T⁡x≠Q→T⁡1K⁡xRx=1K⁡xST⁡x
70 69 eqcomd ⊢x∈X∧T⁡x≠Q→1K⁡xST⁡x=T⁡1K⁡xRx
71 70 fveq2d ⊢x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x=M⁡T⁡1K⁡xRx
72 fveq2 ⊢z=1K⁡xRx→K⁡z=K⁡1K⁡xRx
73 72 breq1d ⊢z=1K⁡xRx→K⁡z≤1↔K⁡1K⁡xRx≤1
74 2fveq3 ⊢z=1K⁡xRx→M⁡T⁡z=M⁡T⁡1K⁡xRx
75 74 eqeq2d ⊢z=1K⁡xRx→M⁡1K⁡xST⁡x=M⁡T⁡z↔M⁡1K⁡xST⁡x=M⁡T⁡1K⁡xRx
76 73 75 anbi12d ⊢z=1K⁡xRx→K⁡z≤1∧M⁡1K⁡xST⁡x=M⁡T⁡z↔K⁡1K⁡xRx≤1∧M⁡1K⁡xST⁡x=M⁡T⁡1K⁡xRx
77 76 rspcev ⊢1K⁡xRx∈X∧K⁡1K⁡xRx≤1∧M⁡1K⁡xST⁡x=M⁡T⁡1K⁡xRx→∃z∈XK⁡z≤1∧M⁡1K⁡xST⁡x=M⁡T⁡z
78 57 65 71 77 syl12anc ⊢x∈X∧T⁡x≠Q→∃z∈XK⁡z≤1∧M⁡1K⁡xST⁡x=M⁡T⁡z
79 fvex ⊢M⁡1K⁡xST⁡x∈V
80 eqeq1 ⊢y=M⁡1K⁡xST⁡x→y=M⁡T⁡z↔M⁡1K⁡xST⁡x=M⁡T⁡z
81 80 anbi2d ⊢y=M⁡1K⁡xST⁡x→K⁡z≤1∧y=M⁡T⁡z↔K⁡z≤1∧M⁡1K⁡xST⁡x=M⁡T⁡z
82 81 rexbidv ⊢y=M⁡1K⁡xST⁡x→∃z∈XK⁡z≤1∧y=M⁡T⁡z↔∃z∈XK⁡z≤1∧M⁡1K⁡xST⁡x=M⁡T⁡z
83 79 82 elab ⊢M⁡1K⁡xST⁡x∈y|∃z∈XK⁡z≤1∧y=M⁡T⁡z↔∃z∈XK⁡z≤1∧M⁡1K⁡xST⁡x=M⁡T⁡z
84 78 83 sylibr ⊢x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x∈y|∃z∈XK⁡z≤1∧y=M⁡T⁡z
85 supxrub ⊢y|∃z∈XK⁡z≤1∧y=M⁡T⁡z⊆ℝ*∧M⁡1K⁡xST⁡x∈y|∃z∈XK⁡z≤1∧y=M⁡T⁡z→M⁡1K⁡xST⁡x≤supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<
86 53 84 85 sylancr ⊢x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x≤supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<
87 86 adantll ⊢N⁡T=0∧x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x≤supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<
88 7 8 13 14 1 nmooval ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T=supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<
89 4 5 32 88 mp3an ⊢N⁡T=supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<
90 89 eqeq1i ⊢N⁡T=0↔supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<=0
91 90 biimpi ⊢N⁡T=0→supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<=0
92 91 ad2antrr ⊢N⁡T=0∧x∈X∧T⁡x≠Q→supy|∃z∈XK⁡z≤1∧y=M⁡T⁡zℝ*<=0
93 87 92 breqtrd ⊢N⁡T=0∧x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x≤0
94 8 14 nvcl ⊢W∈NrmCVec∧1K⁡xST⁡x∈Y→M⁡1K⁡xST⁡x∈ℝ
95 5 44 94 sylancr ⊢x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x∈ℝ
96 0re ⊢0∈ℝ
97 lenlt ⊢M⁡1K⁡xST⁡x∈ℝ∧0∈ℝ→M⁡1K⁡xST⁡x≤0↔¬0<M⁡1K⁡xST⁡x
98 95 96 97 sylancl ⊢x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x≤0↔¬0<M⁡1K⁡xST⁡x
99 98 adantll ⊢N⁡T=0∧x∈X∧T⁡x≠Q→M⁡1K⁡xST⁡x≤0↔¬0<M⁡1K⁡xST⁡x
100 93 99 mpbid ⊢N⁡T=0∧x∈X∧T⁡x≠Q→¬0<M⁡1K⁡xST⁡x
101 100 ex ⊢N⁡T=0∧x∈X→T⁡x≠Q→¬0<M⁡1K⁡xST⁡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∈XT⁡x=Z⁡x
110 ffn ⊢T:X⟶Y→TFnX
111 32 110 ax-mp ⊢TFnX
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→ZFnX
115 113 114 ax-mp ⊢ZFnX
116 eqfnfv ⊢TFnX∧ZFnX→T=Z↔∀x∈XT⁡x=Z⁡x
117 111 115 116 mp2an ⊢T=Z↔∀x∈XT⁡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