Metamath Proof Explorer

Theorem riesz3i

Description: A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of Beran p. 104. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nlelch.1 ⊢T∈LinFn
nlelch.2 ⊢T∈ContFn
Assertion riesz3i ⊢∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw

Proof

Step Hyp Ref Expression
1 nlelch.1 ⊢T∈LinFn
2 nlelch.2 ⊢T∈ContFn
3 ax-hv0cl ⊢0ℎ∈ℋ
4 1 lnfnfi ⊢T:ℋ⟶ℂ
5 fveq2 ⊢⊥⁡null⁡T=0ℋ→⊥⁡⊥⁡null⁡T=⊥⁡0ℋ
6 1 2 nlelchi ⊢null⁡T∈Cℋ
7 6 ococi ⊢⊥⁡⊥⁡null⁡T=null⁡T
8 choc0 ⊢⊥⁡0ℋ=ℋ
9 5 7 8 3eqtr3g ⊢⊥⁡null⁡T=0ℋ→null⁡T=ℋ
10 9 eleq2d ⊢⊥⁡null⁡T=0ℋ→v∈null⁡T↔v∈ℋ
11 10 biimpar ⊢⊥⁡null⁡T=0ℋ∧v∈ℋ→v∈null⁡T
12 elnlfn2 ⊢T:ℋ⟶ℂ∧v∈null⁡T→T⁡v=0
13 4 11 12 sylancr ⊢⊥⁡null⁡T=0ℋ∧v∈ℋ→T⁡v=0
14 hi02 ⊢v∈ℋ→v⋅ih0ℎ=0
15 14 adantl ⊢⊥⁡null⁡T=0ℋ∧v∈ℋ→v⋅ih0ℎ=0
16 13 15 eqtr4d ⊢⊥⁡null⁡T=0ℋ∧v∈ℋ→T⁡v=v⋅ih0ℎ
17 16 ralrimiva ⊢⊥⁡null⁡T=0ℋ→∀v∈ℋT⁡v=v⋅ih0ℎ
18 oveq2 ⊢w=0ℎ→v⋅ihw=v⋅ih0ℎ
19 18 eqeq2d ⊢w=0ℎ→T⁡v=v⋅ihw↔T⁡v=v⋅ih0ℎ
20 19 ralbidv ⊢w=0ℎ→∀v∈ℋT⁡v=v⋅ihw↔∀v∈ℋT⁡v=v⋅ih0ℎ
21 20 rspcev ⊢0ℎ∈ℋ∧∀v∈ℋT⁡v=v⋅ih0ℎ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
22 3 17 21 sylancr ⊢⊥⁡null⁡T=0ℋ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
23 6 choccli ⊢⊥⁡null⁡T∈Cℋ
24 23 chne0i ⊢⊥⁡null⁡T≠0ℋ↔∃u∈⊥⁡null⁡Tu≠0ℎ
25 23 cheli ⊢u∈⊥⁡null⁡T→u∈ℋ
26 4 ffvelcdmi ⊢u∈ℋ→T⁡u∈ℂ
27 26 adantr ⊢u∈ℋ∧u≠0ℎ→T⁡u∈ℂ
28 hicl ⊢u∈ℋ∧u∈ℋ→u⋅ihu∈ℂ
29 28 anidms ⊢u∈ℋ→u⋅ihu∈ℂ
30 29 adantr ⊢u∈ℋ∧u≠0ℎ→u⋅ihu∈ℂ
31 his6 ⊢u∈ℋ→u⋅ihu=0↔u=0ℎ
32 31 necon3bid ⊢u∈ℋ→u⋅ihu≠0↔u≠0ℎ
33 32 biimpar ⊢u∈ℋ∧u≠0ℎ→u⋅ihu≠0
34 27 30 33 divcld ⊢u∈ℋ∧u≠0ℎ→T⁡uu⋅ihu∈ℂ
35 34 cjcld ⊢u∈ℋ∧u≠0ℎ→T⁡uu⋅ihu‾∈ℂ
36 simpl ⊢u∈ℋ∧u≠0ℎ→u∈ℋ
37 hvmulcl ⊢T⁡uu⋅ihu‾∈ℂ∧u∈ℋ→T⁡uu⋅ihu‾⋅ℎu∈ℋ
38 35 36 37 syl2anc ⊢u∈ℋ∧u≠0ℎ→T⁡uu⋅ihu‾⋅ℎu∈ℋ
39 38 adantll ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ→T⁡uu⋅ihu‾⋅ℎu∈ℋ
40 hvmulcl ⊢T⁡u∈ℂ∧v∈ℋ→T⁡u⋅ℎv∈ℋ
41 26 40 sylan ⊢u∈ℋ∧v∈ℋ→T⁡u⋅ℎv∈ℋ
42 4 ffvelcdmi ⊢v∈ℋ→T⁡v∈ℂ
43 hvmulcl ⊢T⁡v∈ℂ∧u∈ℋ→T⁡v⋅ℎu∈ℋ
44 42 43 sylan ⊢v∈ℋ∧u∈ℋ→T⁡v⋅ℎu∈ℋ
45 44 ancoms ⊢u∈ℋ∧v∈ℋ→T⁡v⋅ℎu∈ℋ
46 simpl ⊢u∈ℋ∧v∈ℋ→u∈ℋ
47 his2sub ⊢T⁡u⋅ℎv∈ℋ∧T⁡v⋅ℎu∈ℋ∧u∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=T⁡u⋅ℎv⋅ihu−T⁡v⋅ℎu⋅ihu
48 41 45 46 47 syl3anc ⊢u∈ℋ∧v∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=T⁡u⋅ℎv⋅ihu−T⁡v⋅ℎu⋅ihu
49 26 adantr ⊢u∈ℋ∧v∈ℋ→T⁡u∈ℂ
50 simpr ⊢u∈ℋ∧v∈ℋ→v∈ℋ
51 ax-his3 ⊢T⁡u∈ℂ∧v∈ℋ∧u∈ℋ→T⁡u⋅ℎv⋅ihu=T⁡u⁢v⋅ihu
52 49 50 46 51 syl3anc ⊢u∈ℋ∧v∈ℋ→T⁡u⋅ℎv⋅ihu=T⁡u⁢v⋅ihu
53 42 adantl ⊢u∈ℋ∧v∈ℋ→T⁡v∈ℂ
54 ax-his3 ⊢T⁡v∈ℂ∧u∈ℋ∧u∈ℋ→T⁡v⋅ℎu⋅ihu=T⁡v⁢u⋅ihu
55 53 46 46 54 syl3anc ⊢u∈ℋ∧v∈ℋ→T⁡v⋅ℎu⋅ihu=T⁡v⁢u⋅ihu
56 52 55 oveq12d ⊢u∈ℋ∧v∈ℋ→T⁡u⋅ℎv⋅ihu−T⁡v⋅ℎu⋅ihu=T⁡u⁢v⋅ihu−T⁡v⁢u⋅ihu
57 48 56 eqtr2d ⊢u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu−T⁡v⁢u⋅ihu=T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu
58 57 adantll ⊢u∈⊥⁡null⁡T∧u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu−T⁡v⁢u⋅ihu=T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu
59 hvsubcl ⊢T⁡u⋅ℎv∈ℋ∧T⁡v⋅ℎu∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈ℋ
60 41 45 59 syl2anc ⊢u∈ℋ∧v∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈ℋ
61 1 lnfnsubi ⊢T⁡u⋅ℎv∈ℋ∧T⁡v⋅ℎu∈ℋ→T⁡T⁡u⋅ℎv-ℎT⁡v⋅ℎu=T⁡T⁡u⋅ℎv−T⁡T⁡v⋅ℎu
62 41 45 61 syl2anc ⊢u∈ℋ∧v∈ℋ→T⁡T⁡u⋅ℎv-ℎT⁡v⋅ℎu=T⁡T⁡u⋅ℎv−T⁡T⁡v⋅ℎu
63 1 lnfnmuli ⊢T⁡u∈ℂ∧v∈ℋ→T⁡T⁡u⋅ℎv=T⁡u⁢T⁡v
64 26 63 sylan ⊢u∈ℋ∧v∈ℋ→T⁡T⁡u⋅ℎv=T⁡u⁢T⁡v
65 1 lnfnmuli ⊢T⁡v∈ℂ∧u∈ℋ→T⁡T⁡v⋅ℎu=T⁡v⁢T⁡u
66 mulcom ⊢T⁡v∈ℂ∧T⁡u∈ℂ→T⁡v⁢T⁡u=T⁡u⁢T⁡v
67 26 66 sylan2 ⊢T⁡v∈ℂ∧u∈ℋ→T⁡v⁢T⁡u=T⁡u⁢T⁡v
68 65 67 eqtrd ⊢T⁡v∈ℂ∧u∈ℋ→T⁡T⁡v⋅ℎu=T⁡u⁢T⁡v
69 42 68 sylan ⊢v∈ℋ∧u∈ℋ→T⁡T⁡v⋅ℎu=T⁡u⁢T⁡v
70 69 ancoms ⊢u∈ℋ∧v∈ℋ→T⁡T⁡v⋅ℎu=T⁡u⁢T⁡v
71 64 70 oveq12d ⊢u∈ℋ∧v∈ℋ→T⁡T⁡u⋅ℎv−T⁡T⁡v⋅ℎu=T⁡u⁢T⁡v−T⁡u⁢T⁡v
72 mulcl ⊢T⁡u∈ℂ∧T⁡v∈ℂ→T⁡u⁢T⁡v∈ℂ
73 26 42 72 syl2an ⊢u∈ℋ∧v∈ℋ→T⁡u⁢T⁡v∈ℂ
74 73 subidd ⊢u∈ℋ∧v∈ℋ→T⁡u⁢T⁡v−T⁡u⁢T⁡v=0
75 62 71 74 3eqtrd ⊢u∈ℋ∧v∈ℋ→T⁡T⁡u⋅ℎv-ℎT⁡v⋅ℎu=0
76 elnlfn ⊢T:ℋ⟶ℂ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈null⁡T↔T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈ℋ∧T⁡T⁡u⋅ℎv-ℎT⁡v⋅ℎu=0
77 4 76 ax-mp ⊢T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈null⁡T↔T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈ℋ∧T⁡T⁡u⋅ℎv-ℎT⁡v⋅ℎu=0
78 60 75 77 sylanbrc ⊢u∈ℋ∧v∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈null⁡T
79 6 chssii ⊢null⁡T⊆ℋ
80 ocorth ⊢null⁡T⊆ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈null⁡T∧u∈⊥⁡null⁡T→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=0
81 79 80 ax-mp ⊢T⁡u⋅ℎv-ℎT⁡v⋅ℎu∈null⁡T∧u∈⊥⁡null⁡T→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=0
82 78 81 sylan ⊢u∈ℋ∧v∈ℋ∧u∈⊥⁡null⁡T→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=0
83 82 ancoms ⊢u∈⊥⁡null⁡T∧u∈ℋ∧v∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=0
84 83 anassrs ⊢u∈⊥⁡null⁡T∧u∈ℋ∧v∈ℋ→T⁡u⋅ℎv-ℎT⁡v⋅ℎu⋅ihu=0
85 58 84 eqtrd ⊢u∈⊥⁡null⁡T∧u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu−T⁡v⁢u⋅ihu=0
86 hicl ⊢v∈ℋ∧u∈ℋ→v⋅ihu∈ℂ
87 86 ancoms ⊢u∈ℋ∧v∈ℋ→v⋅ihu∈ℂ
88 49 87 mulcld ⊢u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu∈ℂ
89 mulcl ⊢T⁡v∈ℂ∧u⋅ihu∈ℂ→T⁡v⁢u⋅ihu∈ℂ
90 42 29 89 syl2anr ⊢u∈ℋ∧v∈ℋ→T⁡v⁢u⋅ihu∈ℂ
91 88 90 subeq0ad ⊢u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu−T⁡v⁢u⋅ihu=0↔T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
92 91 adantll ⊢u∈⊥⁡null⁡T∧u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu−T⁡v⁢u⋅ihu=0↔T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
93 85 92 mpbid ⊢u∈⊥⁡null⁡T∧u∈ℋ∧v∈ℋ→T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
94 93 adantlr ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
95 88 adantlr ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihu∈ℂ
96 42 adantl ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡v∈ℂ
97 30 33 jca ⊢u∈ℋ∧u≠0ℎ→u⋅ihu∈ℂ∧u⋅ihu≠0
98 97 adantr ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→u⋅ihu∈ℂ∧u⋅ihu≠0
99 divmul3 ⊢T⁡u⁢v⋅ihu∈ℂ∧T⁡v∈ℂ∧u⋅ihu∈ℂ∧u⋅ihu≠0→T⁡u⁢v⋅ihuu⋅ihu=T⁡v↔T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
100 95 96 98 99 syl3anc ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihuu⋅ihu=T⁡v↔T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
101 100 adantlll ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihuu⋅ihu=T⁡v↔T⁡u⁢v⋅ihu=T⁡v⁢u⋅ihu
102 94 101 mpbird ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihuu⋅ihu=T⁡v
103 27 adantr ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u∈ℂ
104 87 adantlr ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→v⋅ihu∈ℂ
105 div23 ⊢T⁡u∈ℂ∧v⋅ihu∈ℂ∧u⋅ihu∈ℂ∧u⋅ihu≠0→T⁡u⁢v⋅ihuu⋅ihu=T⁡uu⋅ihu⁢v⋅ihu
106 103 104 98 105 syl3anc ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihuu⋅ihu=T⁡uu⋅ihu⁢v⋅ihu
107 34 adantr ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡uu⋅ihu∈ℂ
108 simpr ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→v∈ℋ
109 simpll ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→u∈ℋ
110 his52 ⊢T⁡uu⋅ihu∈ℂ∧v∈ℋ∧u∈ℋ→v⋅ihT⁡uu⋅ihu‾⋅ℎu=T⁡uu⋅ihu⁢v⋅ihu
111 107 108 109 110 syl3anc ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→v⋅ihT⁡uu⋅ihu‾⋅ℎu=T⁡uu⋅ihu⁢v⋅ihu
112 106 111 eqtr4d ⊢u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihuu⋅ihu=v⋅ihT⁡uu⋅ihu‾⋅ℎu
113 112 adantlll ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡u⁢v⋅ihuu⋅ihu=v⋅ihT⁡uu⋅ihu‾⋅ℎu
114 102 113 eqtr3d ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ∧v∈ℋ→T⁡v=v⋅ihT⁡uu⋅ihu‾⋅ℎu
115 114 ralrimiva ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ→∀v∈ℋT⁡v=v⋅ihT⁡uu⋅ihu‾⋅ℎu
116 oveq2 ⊢w=T⁡uu⋅ihu‾⋅ℎu→v⋅ihw=v⋅ihT⁡uu⋅ihu‾⋅ℎu
117 116 eqeq2d ⊢w=T⁡uu⋅ihu‾⋅ℎu→T⁡v=v⋅ihw↔T⁡v=v⋅ihT⁡uu⋅ihu‾⋅ℎu
118 117 ralbidv ⊢w=T⁡uu⋅ihu‾⋅ℎu→∀v∈ℋT⁡v=v⋅ihw↔∀v∈ℋT⁡v=v⋅ihT⁡uu⋅ihu‾⋅ℎu
119 118 rspcev ⊢T⁡uu⋅ihu‾⋅ℎu∈ℋ∧∀v∈ℋT⁡v=v⋅ihT⁡uu⋅ihu‾⋅ℎu→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
120 39 115 119 syl2anc ⊢u∈⊥⁡null⁡T∧u∈ℋ∧u≠0ℎ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
121 120 ex ⊢u∈⊥⁡null⁡T∧u∈ℋ→u≠0ℎ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
122 25 121 mpdan ⊢u∈⊥⁡null⁡T→u≠0ℎ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
123 122 rexlimiv ⊢∃u∈⊥⁡null⁡Tu≠0ℎ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
124 24 123 sylbi ⊢⊥⁡null⁡T≠0ℋ→∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
125 22 124 pm2.61ine ⊢∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw