cnvbraval

Description: Value of the converse of the bra function. Based on the Riesz Lemma riesz4 , this very important theorem not only justifies the Dirac bra-ket notation, but allows to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store"all of the information contained in any entire continuous linear functional (mapping from ~H to CC ). (Contributed by NM, 26-May-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	cnvbraval	$⊢ T \in (LinFn \cap ContFn) \to {bra}^{-1} (T) = (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)$

Proof

Step	Hyp	Ref	Expression
1		bra11	$⊢ bra : ℋ \underset{1-1 onto}{⟶} LinFn \cap ContFn$
2		f1ocnvfv	$⊢ (bra : ℋ \underset{1-1 onto}{⟶} LinFn \cap ContFn \land y \in ℋ) \to (bra (y) = T \to {bra}^{-1} (T) = y)$
3	1 2	mpan	$⊢ y \in ℋ \to (bra (y) = T \to {bra}^{-1} (T) = y)$
4	3	imp	$⊢ (y \in ℋ \land bra (y) = T) \to {bra}^{-1} (T) = y$
5	4	oveq2d	$⊢ (y \in ℋ \land bra (y) = T) \to x \cdot_{ih} {bra}^{-1} (T) = x \cdot_{ih} y$
6	5	adantll	$⊢ (((T \in (LinFn \cap ContFn) \land x \in ℋ) \land y \in ℋ) \land bra (y) = T) \to x \cdot_{ih} {bra}^{-1} (T) = x \cdot_{ih} y$
7		braval	$⊢ (y \in ℋ \land x \in ℋ) \to bra (y) (x) = x \cdot_{ih} y$
8	7	ancoms	$⊢ (x \in ℋ \land y \in ℋ) \to bra (y) (x) = x \cdot_{ih} y$
9	8	adantll	$⊢ ((T \in (LinFn \cap ContFn) \land x \in ℋ) \land y \in ℋ) \to bra (y) (x) = x \cdot_{ih} y$
10	9	adantr	$⊢ (((T \in (LinFn \cap ContFn) \land x \in ℋ) \land y \in ℋ) \land bra (y) = T) \to bra (y) (x) = x \cdot_{ih} y$
11		fveq1	$⊢ bra (y) = T \to bra (y) (x) = T (x)$
12	11	adantl	$⊢ (((T \in (LinFn \cap ContFn) \land x \in ℋ) \land y \in ℋ) \land bra (y) = T) \to bra (y) (x) = T (x)$
13	6 10 12	3eqtr2rd	$⊢ (((T \in (LinFn \cap ContFn) \land x \in ℋ) \land y \in ℋ) \land bra (y) = T) \to T (x) = x \cdot_{ih} {bra}^{-1} (T)$
14		rnbra	$⊢ ran bra = LinFn \cap ContFn$
15	14	eleq2i	$⊢ T \in ran bra \leftrightarrow T \in (LinFn \cap ContFn)$
16		f1of	$⊢ bra : ℋ \underset{1-1 onto}{⟶} LinFn \cap ContFn \to bra : ℋ ⟶ LinFn \cap ContFn$
17	1 16	ax-mp	$⊢ bra : ℋ ⟶ LinFn \cap ContFn$
18		ffn	$⊢ bra : ℋ ⟶ LinFn \cap ContFn \to bra Fn ℋ$
19	17 18	ax-mp	$⊢ bra Fn ℋ$
20		fvelrnb	$⊢ bra Fn ℋ \to (T \in ran bra \leftrightarrow \exists y \in ℋ bra (y) = T)$
21	19 20	ax-mp	$⊢ T \in ran bra \leftrightarrow \exists y \in ℋ bra (y) = T$
22	15 21	sylbb1	$⊢ T \in (LinFn \cap ContFn) \to \exists y \in ℋ bra (y) = T$
23	22	adantr	$⊢ (T \in (LinFn \cap ContFn) \land x \in ℋ) \to \exists y \in ℋ bra (y) = T$
24	13 23	r19.29a	$⊢ (T \in (LinFn \cap ContFn) \land x \in ℋ) \to T (x) = x \cdot_{ih} {bra}^{-1} (T)$
25	24	ralrimiva	$⊢ T \in (LinFn \cap ContFn) \to \forall x \in ℋ T (x) = x \cdot_{ih} {bra}^{-1} (T)$
26		f1ocnvdm	$⊢ (bra : ℋ \underset{1-1 onto}{⟶} LinFn \cap ContFn \land T \in (LinFn \cap ContFn)) \to {bra}^{-1} (T) \in ℋ$
27	1 26	mpan	$⊢ T \in (LinFn \cap ContFn) \to {bra}^{-1} (T) \in ℋ$
28		riesz4	$⊢ T \in (LinFn \cap ContFn) \to \exists! y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y$
29		oveq2	$⊢ y = {bra}^{-1} (T) \to x \cdot_{ih} y = x \cdot_{ih} {bra}^{-1} (T)$
30	29	eqeq2d	$⊢ y = {bra}^{-1} (T) \to (T (x) = x \cdot_{ih} y \leftrightarrow T (x) = x \cdot_{ih} {bra}^{-1} (T))$
31	30	ralbidv	$⊢ y = {bra}^{-1} (T) \to (\forall x \in ℋ T (x) = x \cdot_{ih} y \leftrightarrow \forall x \in ℋ T (x) = x \cdot_{ih} {bra}^{-1} (T))$
32	31	riota2	$⊢ ({bra}^{-1} (T) \in ℋ \land \exists! y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y) \to (\forall x \in ℋ T (x) = x \cdot_{ih} {bra}^{-1} (T) \leftrightarrow (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y) = {bra}^{-1} (T))$
33	27 28 32	syl2anc	$⊢ T \in (LinFn \cap ContFn) \to (\forall x \in ℋ T (x) = x \cdot_{ih} {bra}^{-1} (T) \leftrightarrow (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y) = {bra}^{-1} (T))$
34	25 33	mpbid	$⊢ T \in (LinFn \cap ContFn) \to (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y) = {bra}^{-1} (T)$
35	34	eqcomd	$⊢ T \in (LinFn \cap ContFn) \to {bra}^{-1} (T) = (ι y \in ℋ \| \forall x \in ℋ T (x) = x \cdot_{ih} y)$

Metamath Proof Explorer

Theorem cnvbraval

Proof