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