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	⊢ ( 𝐴 ∈ ℋ → ( ◡ bra ‘ ( bra ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bra11	⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )
2		f1ocnvfv1	⊢ ( ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ∧ 𝐴 ∈ ℋ ) → ( ◡ bra ‘ ( bra ‘ 𝐴 ) ) = 𝐴 )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℋ → ( ◡ bra ‘ ( bra ‘ 𝐴 ) ) = 𝐴 )