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 \in (LinFn \cap ContFn) \to T = bra ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y))$

Step	Hyp	Ref	Expression
1		cnvbraval	$⊢ T \in (LinFn \cap ContFn) \to {bra}^{-1} (T) = (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)$
2		cnvbracl	$⊢ T \in (LinFn \cap ContFn) \to {bra}^{-1} (T) \in ℋ$
3	1 2	eqeltrrd	$⊢ T \in (LinFn \cap ContFn) \to (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y) \in ℋ$
4		bra11	$⊢ bra : ℋ \underset{1-1 onto}{⟶} LinFn \cap ContFn$
5		f1ocnvfvb	$⊢ (bra : ℋ \underset{1-1 onto}{⟶} LinFn \cap ContFn \land (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y) \in ℋ \land T \in (LinFn \cap ContFn)) \to (bra ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)) = T \leftrightarrow {bra}^{-1} (T) = (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y))$
6	4 5	mp3an1	$⊢ ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y) \in ℋ \land T \in (LinFn \cap ContFn)) \to (bra ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)) = T \leftrightarrow {bra}^{-1} (T) = (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y))$
7	3 6	mpancom	$⊢ T \in (LinFn \cap ContFn) \to (bra ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)) = T \leftrightarrow {bra}^{-1} (T) = (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y))$
8	1 7	mpbird	$⊢ T \in (LinFn \cap ContFn) \to bra ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)) = T$
9	8	eqcomd	$⊢ T \in (LinFn \cap ContFn) \to T = bra ((ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y))$

Metamath Proof Explorer