hstrlem3a

Description: Lemma for strong set of CH states theorem: the function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	hstrlem3a.1	$⊢ S = (x \in C_{ℋ} ⟼ {proj}_{ℎ} (x) (u))$
	Assertion	hstrlem3a	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to S \in CHStates$

Proof

Step	Hyp	Ref	Expression
1		hstrlem3a.1	$⊢ S = (x \in C_{ℋ} ⟼ {proj}_{ℎ} (x) (u))$
2		pjhcl	$⊢ (x \in C_{ℋ} \land u \in ℋ) \to {proj}_{ℎ} (x) (u) \in ℋ$
3	2	ancoms	$⊢ (u \in ℋ \land x \in C_{ℋ}) \to {proj}_{ℎ} (x) (u) \in ℋ$
4	3	adantlr	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {proj}_{ℎ} (x) (u) \in ℋ$
5	4 1	fmptd	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to S : C_{ℋ} ⟶ ℋ$
6		helch	$⊢ ℋ \in C_{ℋ}$
7	1	hstrlem2	$⊢ ℋ \in C_{ℋ} \to S (ℋ) = {proj}_{ℎ} (ℋ) (u)$
8	6 7	ax-mp	$⊢ S (ℋ) = {proj}_{ℎ} (ℋ) (u)$
9	8	fveq2i	$⊢ {norm}_{ℎ} (S (ℋ)) = {norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u))$
10		pjch1	$⊢ u \in ℋ \to {proj}_{ℎ} (ℋ) (u) = u$
11	10	fveq2d	$⊢ u \in ℋ \to {norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u)) = {norm}_{ℎ} (u)$
12		id	$⊢ {norm}_{ℎ} (u) = 1 \to {norm}_{ℎ} (u) = 1$
13	11 12	sylan9eq	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to {norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u)) = 1$
14	9 13	eqtrid	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to {norm}_{ℎ} (S (ℋ)) = 1$
15	1	hstrlem2	$⊢ z \in C_{ℋ} \to S (z) = {proj}_{ℎ} (z) (u)$
16	1	hstrlem2	$⊢ w \in C_{ℋ} \to S (w) = {proj}_{ℎ} (w) (u)$
17	15 16	oveqan12d	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ}) \to S (z) \cdot_{ih} S (w) = {proj}_{ℎ} (z) (u) \cdot_{ih} {proj}_{ℎ} (w) (u)$
18	17	3adant3	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to S (z) \cdot_{ih} S (w) = {proj}_{ℎ} (z) (u) \cdot_{ih} {proj}_{ℎ} (w) (u)$
19	18	adantr	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z) \cdot_{ih} S (w) = {proj}_{ℎ} (z) (u) \cdot_{ih} {proj}_{ℎ} (w) (u)$
20		pjoi0	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to {proj}_{ℎ} (z) (u) \cdot_{ih} {proj}_{ℎ} (w) (u) = 0$
21	19 20	eqtrd	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z) \cdot_{ih} S (w) = 0$
22		pjcjt2	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to (z \subseteq ⊥ (w) \to {proj}_{ℎ} (z \lor_{ℋ} w) (u) = {proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u))$
23	22	imp	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to {proj}_{ℎ} (z \lor_{ℋ} w) (u) = {proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u)$
24		chjcl	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ}) \to z \lor_{ℋ} w \in C_{ℋ}$
25	1	hstrlem2	$⊢ z \lor_{ℋ} w \in C_{ℋ} \to S (z \lor_{ℋ} w) = {proj}_{ℎ} (z \lor_{ℋ} w) (u)$
26	24 25	syl	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ}) \to S (z \lor_{ℋ} w) = {proj}_{ℎ} (z \lor_{ℋ} w) (u)$
27	26	3adant3	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to S (z \lor_{ℋ} w) = {proj}_{ℎ} (z \lor_{ℋ} w) (u)$
28	27	adantr	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z \lor_{ℋ} w) = {proj}_{ℎ} (z \lor_{ℋ} w) (u)$
29	15 16	oveqan12d	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ}) \to S (z) +_{ℎ} S (w) = {proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u)$
30	29	3adant3	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to S (z) +_{ℎ} S (w) = {proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u)$
31	30	adantr	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z) +_{ℎ} S (w) = {proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u)$
32	23 28 31	3eqtr4d	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w)$
33	21 32	jca	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w))$
34	33	3exp1	$⊢ z \in C_{ℋ} \to (w \in C_{ℋ} \to (u \in ℋ \to (z \subseteq ⊥ (w) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w)))))$
35	34	com3r	$⊢ u \in ℋ \to (z \in C_{ℋ} \to (w \in C_{ℋ} \to (z \subseteq ⊥ (w) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w)))))$
36	35	adantr	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (z \in C_{ℋ} \to (w \in C_{ℋ} \to (z \subseteq ⊥ (w) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w)))))$
37	36	ralrimdv	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (z \in C_{ℋ} \to \forall w \in C_{ℋ} (z \subseteq ⊥ (w) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w))))$
38	37	ralrimiv	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to \forall z \in C_{ℋ} \forall w \in C_{ℋ} (z \subseteq ⊥ (w) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w)))$
39		ishst	$⊢ S \in CHStates \leftrightarrow (S : C_{ℋ} ⟶ ℋ \land {norm}_{ℎ} (S (ℋ)) = 1 \land \forall z \in C_{ℋ} \forall w \in C_{ℋ} (z \subseteq ⊥ (w) \to (S (z) \cdot_{ih} S (w) = 0 \land S (z \lor_{ℋ} w) = S (z) +_{ℎ} S (w))))$
40	5 14 38 39	syl3anbrc	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to S \in CHStates$

Metamath Proof Explorer

Theorem hstrlem3a

Proof