# 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}_{\mathrm{OLD}}{W}$
nmlno0.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
nmlno0.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
nmlno0lem.u ${⊢}{U}\in \mathrm{NrmCVec}$
nmlno0lem.w ${⊢}{W}\in \mathrm{NrmCVec}$
nmlno0lem.l ${⊢}{T}\in {L}$
nmlno0lem.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmlno0lem.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmlno0lem.r ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
nmlno0lem.s ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
nmlno0lem.p ${⊢}{P}={0}_{\mathrm{vec}}\left({U}\right)$
nmlno0lem.q ${⊢}{Q}={0}_{\mathrm{vec}}\left({W}\right)$
nmlno0lem.k ${⊢}{K}={norm}_{CV}\left({U}\right)$
nmlno0lem.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
Assertion nmlno0lem ${⊢}{N}\left({T}\right)=0↔{T}={Z}$

### Proof

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