Theorem bracnvbra

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

	Ref	Expression
Assertion	bracnvbra	$$⊢T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \mathrm{bra}\left({\mathrm{bra}}^{-1}\left(T\right)\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		bra11	$$⊢\mathrm{bra}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}$$
2		f1ocnvfv2	$$⊢\left(\mathrm{bra}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}\wedge T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\right)\to \mathrm{bra}\left({\mathrm{bra}}^{-1}\left(T\right)\right)=T$$
3	1 2	mpan	$$⊢T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \mathrm{bra}\left({\mathrm{bra}}^{-1}\left(T\right)\right)=T$$