Step |
Hyp |
Ref |
Expression |
1 |
|
lnfncnbd |
|- ( t e. LinFn -> ( t e. ContFn <-> ( normfn ` t ) e. RR ) ) |
2 |
1
|
pm5.32i |
|- ( ( t e. LinFn /\ t e. ContFn ) <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) |
3 |
|
elin |
|- ( t e. ( LinFn i^i ContFn ) <-> ( t e. LinFn /\ t e. ContFn ) ) |
4 |
|
ax-hilex |
|- ~H e. _V |
5 |
4
|
mptex |
|- ( y e. ~H |-> ( y .ih x ) ) e. _V |
6 |
|
df-bra |
|- bra = ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) ) |
7 |
5 6
|
fnmpti |
|- bra Fn ~H |
8 |
|
fvelrnb |
|- ( bra Fn ~H -> ( t e. ran bra <-> E. x e. ~H ( bra ` x ) = t ) ) |
9 |
7 8
|
ax-mp |
|- ( t e. ran bra <-> E. x e. ~H ( bra ` x ) = t ) |
10 |
|
bralnfn |
|- ( x e. ~H -> ( bra ` x ) e. LinFn ) |
11 |
|
brabn |
|- ( x e. ~H -> ( normfn ` ( bra ` x ) ) e. RR ) |
12 |
10 11
|
jca |
|- ( x e. ~H -> ( ( bra ` x ) e. LinFn /\ ( normfn ` ( bra ` x ) ) e. RR ) ) |
13 |
|
eleq1 |
|- ( ( bra ` x ) = t -> ( ( bra ` x ) e. LinFn <-> t e. LinFn ) ) |
14 |
|
fveq2 |
|- ( ( bra ` x ) = t -> ( normfn ` ( bra ` x ) ) = ( normfn ` t ) ) |
15 |
14
|
eleq1d |
|- ( ( bra ` x ) = t -> ( ( normfn ` ( bra ` x ) ) e. RR <-> ( normfn ` t ) e. RR ) ) |
16 |
13 15
|
anbi12d |
|- ( ( bra ` x ) = t -> ( ( ( bra ` x ) e. LinFn /\ ( normfn ` ( bra ` x ) ) e. RR ) <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) ) |
17 |
12 16
|
syl5ibcom |
|- ( x e. ~H -> ( ( bra ` x ) = t -> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) ) |
18 |
17
|
rexlimiv |
|- ( E. x e. ~H ( bra ` x ) = t -> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) |
19 |
|
riesz1 |
|- ( t e. LinFn -> ( ( normfn ` t ) e. RR <-> E. x e. ~H A. y e. ~H ( t ` y ) = ( y .ih x ) ) ) |
20 |
19
|
biimpa |
|- ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> E. x e. ~H A. y e. ~H ( t ` y ) = ( y .ih x ) ) |
21 |
|
braval |
|- ( ( x e. ~H /\ y e. ~H ) -> ( ( bra ` x ) ` y ) = ( y .ih x ) ) |
22 |
|
eqtr3 |
|- ( ( ( ( bra ` x ) ` y ) = ( y .ih x ) /\ ( t ` y ) = ( y .ih x ) ) -> ( ( bra ` x ) ` y ) = ( t ` y ) ) |
23 |
22
|
ex |
|- ( ( ( bra ` x ) ` y ) = ( y .ih x ) -> ( ( t ` y ) = ( y .ih x ) -> ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
24 |
21 23
|
syl |
|- ( ( x e. ~H /\ y e. ~H ) -> ( ( t ` y ) = ( y .ih x ) -> ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
25 |
24
|
ralimdva |
|- ( x e. ~H -> ( A. y e. ~H ( t ` y ) = ( y .ih x ) -> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
26 |
25
|
adantl |
|- ( ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) /\ x e. ~H ) -> ( A. y e. ~H ( t ` y ) = ( y .ih x ) -> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
27 |
|
brafn |
|- ( x e. ~H -> ( bra ` x ) : ~H --> CC ) |
28 |
|
lnfnf |
|- ( t e. LinFn -> t : ~H --> CC ) |
29 |
28
|
adantr |
|- ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> t : ~H --> CC ) |
30 |
|
ffn |
|- ( ( bra ` x ) : ~H --> CC -> ( bra ` x ) Fn ~H ) |
31 |
|
ffn |
|- ( t : ~H --> CC -> t Fn ~H ) |
32 |
|
eqfnfv |
|- ( ( ( bra ` x ) Fn ~H /\ t Fn ~H ) -> ( ( bra ` x ) = t <-> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
33 |
30 31 32
|
syl2an |
|- ( ( ( bra ` x ) : ~H --> CC /\ t : ~H --> CC ) -> ( ( bra ` x ) = t <-> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
34 |
27 29 33
|
syl2anr |
|- ( ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) /\ x e. ~H ) -> ( ( bra ` x ) = t <-> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) ) |
35 |
26 34
|
sylibrd |
|- ( ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) /\ x e. ~H ) -> ( A. y e. ~H ( t ` y ) = ( y .ih x ) -> ( bra ` x ) = t ) ) |
36 |
35
|
reximdva |
|- ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> ( E. x e. ~H A. y e. ~H ( t ` y ) = ( y .ih x ) -> E. x e. ~H ( bra ` x ) = t ) ) |
37 |
20 36
|
mpd |
|- ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> E. x e. ~H ( bra ` x ) = t ) |
38 |
18 37
|
impbii |
|- ( E. x e. ~H ( bra ` x ) = t <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) |
39 |
9 38
|
bitri |
|- ( t e. ran bra <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) |
40 |
2 3 39
|
3bitr4ri |
|- ( t e. ran bra <-> t e. ( LinFn i^i ContFn ) ) |
41 |
40
|
eqriv |
|- ran bra = ( LinFn i^i ContFn ) |