Metamath Proof Explorer

Theorem bracnlnval

Description: The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bracnlnval 
|- ( T e. ( LinFn i^i ContFn ) -> T = ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) )

Proof

Step Hyp Ref Expression
1 cnvbraval 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )
2 cnvbracl 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) e. ~H )
3 1 2 eqeltrrd 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) e. ~H )
4 bra11 
 |-  bra : ~H -1-1-onto-> ( LinFn i^i ContFn )
5 f1ocnvfvb 
 |-  ( ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) /\ ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) e. ~H /\ T e. ( LinFn i^i ContFn ) ) -> ( ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) = T <-> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) )
6 4 5 mp3an1 
 |-  ( ( ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) e. ~H /\ T e. ( LinFn i^i ContFn ) ) -> ( ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) = T <-> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) )
7 3 6 mpancom 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) = T <-> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) )
8 1 7 mpbird 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) = T )
9 8 eqcomd 
 |-  ( T e. ( LinFn i^i ContFn ) -> T = ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) )