Metamath Proof Explorer

Theorem cnvbrabra

Description: The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvbrabra 
|- ( A e. ~H -> ( `' bra ` ( bra ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 bra11 
 |-  bra : ~H -1-1-onto-> ( LinFn i^i ContFn )
2 f1ocnvfv1 
 |-  ( ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) /\ A e. ~H ) -> ( `' bra ` ( bra ` A ) ) = A )
3 1 2 mpan 
 |-  ( A e. ~H -> ( `' bra ` ( bra ` A ) ) = A )