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\in \mathscr{H}\to {\mathrm{bra}}^{-1}\left(\mathrm{bra}\left(A\right)\right)=A$$

Proof

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