Metamath Proof Explorer

Theorem nmcexi

Description: Lemma for nmcopexi and nmcfnexi . The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by Mario Carneiro, 17-Nov-2013) (Proof shortened by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcex.1 ⊢∃y∈ℝ+∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1
nmcex.2 ⊢S⁡T=supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ*<
nmcex.3 ⊢x∈ℋ→N⁡T⁡x∈ℝ
nmcex.4 ⊢N⁡T⁡0ℎ=0
nmcex.5 ⊢y2∈ℝ+∧x∈ℋ→y2⁢N⁡T⁡x=N⁡T⁡y2⋅ℎx
Assertion nmcexi ⊢S⁡T∈ℝ

Proof

Step Hyp Ref Expression
1 nmcex.1 ⊢∃y∈ℝ+∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1
2 nmcex.2 ⊢S⁡T=supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ*<
3 nmcex.3 ⊢x∈ℋ→N⁡T⁡x∈ℝ
4 nmcex.4 ⊢N⁡T⁡0ℎ=0
5 nmcex.5 ⊢y2∈ℝ+∧x∈ℋ→y2⁢N⁡T⁡x=N⁡T⁡y2⋅ℎx
6 eleq1 ⊢m=N⁡T⁡x→m∈ℝ↔N⁡T⁡x∈ℝ
7 3 6 syl5ibrcom ⊢x∈ℋ→m=N⁡T⁡x→m∈ℝ
8 7 imp ⊢x∈ℋ∧m=N⁡T⁡x→m∈ℝ
9 8 adantrl ⊢x∈ℋ∧normℎ⁡x≤1∧m=N⁡T⁡x→m∈ℝ
10 9 rexlimiva ⊢∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x→m∈ℝ
11 10 abssi ⊢m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x⊆ℝ
12 ax-hv0cl ⊢0ℎ∈ℋ
13 norm0 ⊢normℎ⁡0ℎ=0
14 0le1 ⊢0≤1
15 13 14 eqbrtri ⊢normℎ⁡0ℎ≤1
16 4 eqcomi ⊢0=N⁡T⁡0ℎ
17 15 16 pm3.2i ⊢normℎ⁡0ℎ≤1∧0=N⁡T⁡0ℎ
18 fveq2 ⊢x=0ℎ→normℎ⁡x=normℎ⁡0ℎ
19 18 breq1d ⊢x=0ℎ→normℎ⁡x≤1↔normℎ⁡0ℎ≤1
20 2fveq3 ⊢x=0ℎ→N⁡T⁡x=N⁡T⁡0ℎ
21 20 eqeq2d ⊢x=0ℎ→0=N⁡T⁡x↔0=N⁡T⁡0ℎ
22 19 21 anbi12d ⊢x=0ℎ→normℎ⁡x≤1∧0=N⁡T⁡x↔normℎ⁡0ℎ≤1∧0=N⁡T⁡0ℎ
23 22 rspcev ⊢0ℎ∈ℋ∧normℎ⁡0ℎ≤1∧0=N⁡T⁡0ℎ→∃x∈ℋnormℎ⁡x≤1∧0=N⁡T⁡x
24 12 17 23 mp2an ⊢∃x∈ℋnormℎ⁡x≤1∧0=N⁡T⁡x
25 c0ex ⊢0∈V
26 eqeq1 ⊢m=0→m=N⁡T⁡x↔0=N⁡T⁡x
27 26 anbi2d ⊢m=0→normℎ⁡x≤1∧m=N⁡T⁡x↔normℎ⁡x≤1∧0=N⁡T⁡x
28 27 rexbidv ⊢m=0→∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x↔∃x∈ℋnormℎ⁡x≤1∧0=N⁡T⁡x
29 25 28 elab ⊢0∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x↔∃x∈ℋnormℎ⁡x≤1∧0=N⁡T⁡x
30 24 29 mpbir ⊢0∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x
31 30 ne0ii ⊢m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x≠∅
32 2rp ⊢2∈ℝ+
33 rpdivcl ⊢2∈ℝ+∧y∈ℝ+→2y∈ℝ+
34 32 33 mpan ⊢y∈ℝ+→2y∈ℝ+
35 34 rpred ⊢y∈ℝ+→2y∈ℝ
36 35 adantr ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→2y∈ℝ
37 rpre ⊢y∈ℝ+→y∈ℝ
38 37 adantr ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y∈ℝ
39 38 rehalfcld ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2∈ℝ
40 39 recnd ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2∈ℂ
41 simprl ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→x∈ℋ
42 hvmulcl ⊢y2∈ℂ∧x∈ℋ→y2⋅ℎx∈ℋ
43 40 41 42 syl2anc ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⋅ℎx∈ℋ
44 normcl ⊢y2⋅ℎx∈ℋ→normℎ⁡y2⋅ℎx∈ℝ
45 43 44 syl ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡y2⋅ℎx∈ℝ
46 simprr ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡x≤1
47 normcl ⊢x∈ℋ→normℎ⁡x∈ℝ
48 47 ad2antrl ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡x∈ℝ
49 1red ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→1∈ℝ
50 rphalfcl ⊢y∈ℝ+→y2∈ℝ+
51 50 adantr ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2∈ℝ+
52 48 49 51 lemul2d ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡x≤1↔y2⁢normℎ⁡x≤y2⋅1
53 46 52 mpbid ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⁢normℎ⁡x≤y2⋅1
54 rpcn ⊢y2∈ℝ+→y2∈ℂ
55 norm-iii ⊢y2∈ℂ∧x∈ℋ→normℎ⁡y2⋅ℎx=y2⁢normℎ⁡x
56 54 55 sylan ⊢y2∈ℝ+∧x∈ℋ→normℎ⁡y2⋅ℎx=y2⁢normℎ⁡x
57 rpre ⊢y2∈ℝ+→y2∈ℝ
58 rpge0 ⊢y2∈ℝ+→0≤y2
59 57 58 absidd ⊢y2∈ℝ+→y2=y2
60 59 oveq1d ⊢y2∈ℝ+→y2⁢normℎ⁡x=y2⁢normℎ⁡x
61 60 adantr ⊢y2∈ℝ+∧x∈ℋ→y2⁢normℎ⁡x=y2⁢normℎ⁡x
62 56 61 eqtr2d ⊢y2∈ℝ+∧x∈ℋ→y2⁢normℎ⁡x=normℎ⁡y2⋅ℎx
63 51 41 62 syl2anc ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⁢normℎ⁡x=normℎ⁡y2⋅ℎx
64 40 mulridd ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⋅1=y2
65 53 63 64 3brtr3d ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡y2⋅ℎx≤y2
66 rphalflt ⊢y∈ℝ+→y2<y
67 66 adantr ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2<y
68 45 39 38 65 67 lelttrd ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡y2⋅ℎx<y
69 fveq2 ⊢z=y2⋅ℎx→normℎ⁡z=normℎ⁡y2⋅ℎx
70 69 breq1d ⊢z=y2⋅ℎx→normℎ⁡z<y↔normℎ⁡y2⋅ℎx<y
71 2fveq3 ⊢z=y2⋅ℎx→N⁡T⁡z=N⁡T⁡y2⋅ℎx
72 71 breq1d ⊢z=y2⋅ℎx→N⁡T⁡z<1↔N⁡T⁡y2⋅ℎx<1
73 70 72 imbi12d ⊢z=y2⋅ℎx→normℎ⁡z<y→N⁡T⁡z<1↔normℎ⁡y2⋅ℎx<y→N⁡T⁡y2⋅ℎx<1
74 73 rspcv ⊢y2⋅ℎx∈ℋ→∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→normℎ⁡y2⋅ℎx<y→N⁡T⁡y2⋅ℎx<1
75 43 74 syl ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→normℎ⁡y2⋅ℎx<y→N⁡T⁡y2⋅ℎx<1
76 68 75 mpid ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→N⁡T⁡y2⋅ℎx<1
77 3 ad2antrl ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→N⁡T⁡x∈ℝ
78 77 49 51 ltmuldiv2d ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⁢N⁡T⁡x<1↔N⁡T⁡x<1y2
79 51 rprecred ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→1y2∈ℝ
80 ltle ⊢N⁡T⁡x∈ℝ∧1y2∈ℝ→N⁡T⁡x<1y2→N⁡T⁡x≤1y2
81 77 79 80 syl2anc ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→N⁡T⁡x<1y2→N⁡T⁡x≤1y2
82 78 81 sylbid ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⁢N⁡T⁡x<1→N⁡T⁡x≤1y2
83 51 41 5 syl2anc ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⁢N⁡T⁡x=N⁡T⁡y2⋅ℎx
84 83 breq1d ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→y2⁢N⁡T⁡x<1↔N⁡T⁡y2⋅ℎx<1
85 rpcn ⊢y∈ℝ+→y∈ℂ
86 rpne0 ⊢y∈ℝ+→y≠0
87 2cn ⊢2∈ℂ
88 2ne0 ⊢2≠0
89 recdiv ⊢y∈ℂ∧y≠0∧2∈ℂ∧2≠0→1y2=2y
90 87 88 89 mpanr12 ⊢y∈ℂ∧y≠0→1y2=2y
91 85 86 90 syl2anc ⊢y∈ℝ+→1y2=2y
92 91 adantr ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→1y2=2y
93 92 breq2d ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→N⁡T⁡x≤1y2↔N⁡T⁡x≤2y
94 82 84 93 3imtr3d ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→N⁡T⁡y2⋅ℎx<1→N⁡T⁡x≤2y
95 76 94 syld ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1→∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→N⁡T⁡x≤2y
96 95 imp ⊢y∈ℝ+∧x∈ℋ∧normℎ⁡x≤1∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→N⁡T⁡x≤2y
97 96 an32s ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1∧x∈ℋ∧normℎ⁡x≤1→N⁡T⁡x≤2y
98 97 anassrs ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1∧x∈ℋ∧normℎ⁡x≤1→N⁡T⁡x≤2y
99 breq1 ⊢n=N⁡T⁡x→n≤2y↔N⁡T⁡x≤2y
100 98 99 syl5ibrcom ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1∧x∈ℋ∧normℎ⁡x≤1→n=N⁡T⁡x→n≤2y
101 100 expimpd ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1∧x∈ℋ→normℎ⁡x≤1∧n=N⁡T⁡x→n≤2y
102 101 rexlimdva ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤2y
103 102 alrimiv ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→∀n∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤2y
104 eqeq1 ⊢m=n→m=N⁡T⁡x↔n=N⁡T⁡x
105 104 anbi2d ⊢m=n→normℎ⁡x≤1∧m=N⁡T⁡x↔normℎ⁡x≤1∧n=N⁡T⁡x
106 105 rexbidv ⊢m=n→∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x↔∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x
107 106 ralab ⊢∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z↔∀n∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤z
108 breq2 ⊢z=2y→n≤z↔n≤2y
109 108 imbi2d ⊢z=2y→∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤z↔∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤2y
110 109 albidv ⊢z=2y→∀n∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤z↔∀n∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤2y
111 107 110 bitrid ⊢z=2y→∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z↔∀n∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤2y
112 111 rspcev ⊢2y∈ℝ∧∀n∃x∈ℋnormℎ⁡x≤1∧n=N⁡T⁡x→n≤2y→∃z∈ℝ∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z
113 36 103 112 syl2anc ⊢y∈ℝ+∧∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→∃z∈ℝ∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z
114 113 rexlimiva ⊢∃y∈ℝ+∀z∈ℋnormℎ⁡z<y→N⁡T⁡z<1→∃z∈ℝ∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z
115 1 114 ax-mp ⊢∃z∈ℝ∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z
116 supxrre ⊢m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x⊆ℝ∧m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x≠∅∧∃z∈ℝ∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z→supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ*<=supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ<
117 11 31 115 116 mp3an ⊢supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ*<=supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ<
118 2 117 eqtri ⊢S⁡T=supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ<
119 suprcl ⊢m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x⊆ℝ∧m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡x≠∅∧∃z∈ℝ∀n∈m|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xn≤z→supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ<∈ℝ
120 11 31 115 119 mp3an ⊢supm|∃x∈ℋnormℎ⁡x≤1∧m=N⁡T⁡xℝ<∈ℝ
121 118 120 eqeltri ⊢S⁡T∈ℝ