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 normOpOLD W )
nmlno0.0 
|- Z = ( U 0op W )
nmlno0.7 
|- L = ( U LnOp W )
nmlno0lem.u 
|- U e. NrmCVec
nmlno0lem.w 
|- W e. NrmCVec
nmlno0lem.l 
|- T e. L
nmlno0lem.1 
|- X = ( BaseSet ` U )
nmlno0lem.2 
|- Y = ( BaseSet ` W )
nmlno0lem.r 
|- R = ( .sOLD ` U )
nmlno0lem.s 
|- S = ( .sOLD ` 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 = ( U normOpOLD W )
2 nmlno0.0 
 |-  Z = ( U 0op W )
3 nmlno0.7 
 |-  L = ( U LnOp W )
4 nmlno0lem.u 
 |-  U e. NrmCVec
5 nmlno0lem.w 
 |-  W e. NrmCVec
6 nmlno0lem.l 
 |-  T e. L
7 nmlno0lem.1 
 |-  X = ( BaseSet ` U )
8 nmlno0lem.2 
 |-  Y = ( BaseSet ` W )
9 nmlno0lem.r 
 |-  R = ( .sOLD ` U )
10 nmlno0lem.s 
 |-  S = ( .sOLD ` 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 e. NrmCVec /\ x e. X ) -> ( K ` x ) e. RR )
16 4 15 mpan 
 |-  ( x e. X -> ( K ` x ) e. RR )
17 16 recnd 
 |-  ( x e. X -> ( K ` x ) e. CC )
18 17 adantr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( K ` x ) e. CC )
19 7 11 13 nvz 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> ( ( K ` x ) = 0 <-> x = P ) )
20 4 19 mpan 
 |-  ( x e. X -> ( ( K ` x ) = 0 <-> x = P ) )
21 fveq2 
 |-  ( x = P -> ( T ` x ) = ( T ` P ) )
22 7 8 11 12 3 lno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. 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 e. X -> ( ( K ` x ) = 0 -> ( T ` x ) = Q ) )
26 25 necon3d 
 |-  ( x e. X -> ( ( T ` x ) =/= Q -> ( K ` x ) =/= 0 ) )
27 26 imp 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( K ` x ) =/= 0 )
28 18 27 recne0d 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( 1 / ( K ` x ) ) =/= 0 )
29 simpr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( T ` x ) =/= Q )
30 18 27 reccld 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( 1 / ( K ` x ) ) e. CC )
31 7 8 3 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> Y )
32 4 5 6 31 mp3an 
 |-  T : X --> Y
33 32 ffvelrni 
 |-  ( x e. X -> ( T ` x ) e. Y )
34 33 adantr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( T ` x ) e. Y )
35 8 10 12 nvmul0or 
 |-  ( ( W e. NrmCVec /\ ( 1 / ( K ` x ) ) e. CC /\ ( T ` x ) e. Y ) -> ( ( ( 1 / ( K ` x ) ) S ( T ` x ) ) = Q <-> ( ( 1 / ( K ` x ) ) = 0 \/ ( T ` x ) = Q ) ) )
36 5 35 mp3an1 
 |-  ( ( ( 1 / ( K ` x ) ) e. CC /\ ( T ` x ) e. Y ) -> ( ( ( 1 / ( K ` x ) ) S ( T ` x ) ) = Q <-> ( ( 1 / ( K ` x ) ) = 0 \/ ( T ` x ) = Q ) ) )
37 30 34 36 syl2anc 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( ( ( 1 / ( K ` x ) ) S ( T ` x ) ) = Q <-> ( ( 1 / ( K ` x ) ) = 0 \/ ( T ` x ) = Q ) ) )
38 37 necon3abid 
 |-  ( ( x e. 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 e. X /\ ( T ` x ) =/= Q ) -> ( ( ( 1 / ( K ` x ) ) S ( T ` x ) ) =/= Q <-> ( ( 1 / ( K ` x ) ) =/= 0 /\ ( T ` x ) =/= Q ) ) )
41 28 29 40 mpbir2and 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( ( 1 / ( K ` x ) ) S ( T ` x ) ) =/= Q )
42 8 10 nvscl 
 |-  ( ( W e. NrmCVec /\ ( 1 / ( K ` x ) ) e. CC /\ ( T ` x ) e. Y ) -> ( ( 1 / ( K ` x ) ) S ( T ` x ) ) e. Y )
43 5 42 mp3an1 
 |-  ( ( ( 1 / ( K ` x ) ) e. CC /\ ( T ` x ) e. Y ) -> ( ( 1 / ( K ` x ) ) S ( T ` x ) ) e. Y )
44 30 34 43 syl2anc 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( ( 1 / ( K ` x ) ) S ( T ` x ) ) e. Y )
45 8 12 14 nvgt0 
 |-  ( ( W e. NrmCVec /\ ( ( 1 / ( K ` x ) ) S ( T ` x ) ) e. Y ) -> ( ( ( 1 / ( K ` x ) ) S ( T ` x ) ) =/= Q <-> 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) ) )
46 5 44 45 sylancr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( ( ( 1 / ( K ` x ) ) S ( T ` x ) ) =/= Q <-> 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) ) )
47 41 46 mpbid 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) )
48 47 ex 
 |-  ( x e. X -> ( ( T ` x ) =/= Q -> 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) ) )
49 48 adantl 
 |-  ( ( ( N ` T ) = 0 /\ x e. X ) -> ( ( T ` x ) =/= Q -> 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) ) )
50 8 14 nmosetre 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } C_ RR )
51 5 32 50 mp2an 
 |-  { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } C_ RR
52 ressxr 
 |-  RR C_ RR*
53 51 52 sstri 
 |-  { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } C_ RR*
54 simpl 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> x e. X )
55 7 9 nvscl 
 |-  ( ( U e. NrmCVec /\ ( 1 / ( K ` x ) ) e. CC /\ x e. X ) -> ( ( 1 / ( K ` x ) ) R x ) e. X )
56 4 55 mp3an1 
 |-  ( ( ( 1 / ( K ` x ) ) e. CC /\ x e. X ) -> ( ( 1 / ( K ` x ) ) R x ) e. X )
57 30 54 56 syl2anc 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( ( 1 / ( K ` x ) ) R x ) e. X )
58 24 necon3i 
 |-  ( ( T ` x ) =/= Q -> x =/= P )
59 7 9 11 13 nv1 
 |-  ( ( U e. NrmCVec /\ x e. X /\ x =/= P ) -> ( K ` ( ( 1 / ( K ` x ) ) R x ) ) = 1 )
60 4 59 mp3an1 
 |-  ( ( x e. X /\ x =/= P ) -> ( K ` ( ( 1 / ( K ` x ) ) R x ) ) = 1 )
61 58 60 sylan2 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( K ` ( ( 1 / ( K ` x ) ) R x ) ) = 1 )
62 1re 
 |-  1 e. RR
63 61 62 eqeltrdi 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( K ` ( ( 1 / ( K ` x ) ) R x ) ) e. RR )
64 eqle 
 |-  ( ( ( K ` ( ( 1 / ( K ` x ) ) R x ) ) e. RR /\ ( K ` ( ( 1 / ( K ` x ) ) R x ) ) = 1 ) -> ( K ` ( ( 1 / ( K ` x ) ) R x ) ) <_ 1 )
65 63 61 64 syl2anc 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( K ` ( ( 1 / ( K ` x ) ) R x ) ) <_ 1 )
66 4 5 6 3pm3.2i 
 |-  ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L )
67 7 9 10 3 lnomul 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( ( 1 / ( K ` x ) ) e. CC /\ x e. X ) ) -> ( T ` ( ( 1 / ( K ` x ) ) R x ) ) = ( ( 1 / ( K ` x ) ) S ( T ` x ) ) )
68 66 67 mpan 
 |-  ( ( ( 1 / ( K ` x ) ) e. CC /\ x e. X ) -> ( T ` ( ( 1 / ( K ` x ) ) R x ) ) = ( ( 1 / ( K ` x ) ) S ( T ` x ) ) )
69 30 54 68 syl2anc 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( T ` ( ( 1 / ( K ` x ) ) R x ) ) = ( ( 1 / ( K ` x ) ) S ( T ` x ) ) )
70 69 eqcomd 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( ( 1 / ( K ` x ) ) S ( T ` x ) ) = ( T ` ( ( 1 / ( K ` x ) ) R x ) ) )
71 70 fveq2d 
 |-  ( ( x e. 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 ) e. X /\ ( ( K ` ( ( 1 / ( K ` x ) ) R x ) ) <_ 1 /\ ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) = ( M ` ( T ` ( ( 1 / ( K ` x ) ) R x ) ) ) ) ) -> E. z e. X ( ( K ` z ) <_ 1 /\ ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) = ( M ` ( T ` z ) ) ) )
78 57 65 71 77 syl12anc 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> E. z e. X ( ( K ` z ) <_ 1 /\ ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) = ( M ` ( T ` z ) ) ) )
79 fvex 
 |-  ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) e. _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 ) ) ) -> ( E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) <-> E. z e. 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 ) ) ) e. { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } <-> E. z e. X ( ( K ` z ) <_ 1 /\ ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) = ( M ` ( T ` z ) ) ) )
84 78 83 sylibr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) e. { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } )
85 supxrub 
 |-  ( ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } C_ RR* /\ ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) e. { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) <_ sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) )
86 53 84 85 sylancr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) <_ sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) )
87 86 adantll 
 |-  ( ( ( ( N ` T ) = 0 /\ x e. X ) /\ ( T ` x ) =/= Q ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) <_ sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) )
88 7 8 13 14 1 nmooval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) )
89 4 5 32 88 mp3an 
 |-  ( N ` T ) = sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < )
90 89 eqeq1i 
 |-  ( ( N ` T ) = 0 <-> sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) = 0 )
91 90 biimpi 
 |-  ( ( N ` T ) = 0 -> sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) = 0 )
92 91 ad2antrr 
 |-  ( ( ( ( N ` T ) = 0 /\ x e. X ) /\ ( T ` x ) =/= Q ) -> sup ( { y | E. z e. X ( ( K ` z ) <_ 1 /\ y = ( M ` ( T ` z ) ) ) } , RR* , < ) = 0 )
93 87 92 breqtrd 
 |-  ( ( ( ( N ` T ) = 0 /\ x e. X ) /\ ( T ` x ) =/= Q ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) <_ 0 )
94 8 14 nvcl 
 |-  ( ( W e. NrmCVec /\ ( ( 1 / ( K ` x ) ) S ( T ` x ) ) e. Y ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) e. RR )
95 5 44 94 sylancr 
 |-  ( ( x e. X /\ ( T ` x ) =/= Q ) -> ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) e. RR )
96 0re 
 |-  0 e. RR
97 lenlt 
 |-  ( ( ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) e. RR /\ 0 e. RR ) -> ( ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) <_ 0 <-> -. 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) ) )
98 95 96 97 sylancl 
 |-  ( ( x e. 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 e. 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 e. X ) /\ ( T ` x ) =/= Q ) -> -. 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) )
101 100 ex 
 |-  ( ( ( N ` T ) = 0 /\ x e. X ) -> ( ( T ` x ) =/= Q -> -. 0 < ( M ` ( ( 1 / ( K ` x ) ) S ( T ` x ) ) ) ) )
102 49 101 pm2.65d 
 |-  ( ( ( N ` T ) = 0 /\ x e. X ) -> -. ( T ` x ) =/= Q )
103 nne 
 |-  ( -. ( T ` x ) =/= Q <-> ( T ` x ) = Q )
104 102 103 sylib 
 |-  ( ( ( N ` T ) = 0 /\ x e. X ) -> ( T ` x ) = Q )
105 7 12 2 0oval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ x e. X ) -> ( Z ` x ) = Q )
106 4 5 105 mp3an12 
 |-  ( x e. X -> ( Z ` x ) = Q )
107 106 adantl 
 |-  ( ( ( N ` T ) = 0 /\ x e. X ) -> ( Z ` x ) = Q )
108 104 107 eqtr4d 
 |-  ( ( ( N ` T ) = 0 /\ x e. X ) -> ( T ` x ) = ( Z ` x ) )
109 108 ralrimiva 
 |-  ( ( N ` T ) = 0 -> A. x e. 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 e. NrmCVec /\ W e. 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 <-> A. x e. X ( T ` x ) = ( Z ` x ) ) )
117 111 115 116 mp2an 
 |-  ( T = Z <-> A. x e. 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 e. NrmCVec /\ W e. 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 )