hstle

Description: Ordering property of a Hilbert-space-valued state. (Contributed by NM, 26-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hstle	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {norm}_{ℎ} (S (A)) \leq {norm}_{ℎ} (S (B))$

Proof

Step	Hyp	Ref	Expression
1		hstnmoc	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} = 1$
2	1	adantlr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} = 1$
3	2	oveq2d	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} = {{norm}_{ℎ} (S (A))}^{2} + 1$
4		hstcl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to S (A) \in ℋ$
5		normcl	$⊢ S (A) \in ℋ \to {norm}_{ℎ} (S (A)) \in ℝ$
6	4 5	syl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {norm}_{ℎ} (S (A)) \in ℝ$
7	6	resqcld	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} \in ℝ$
8	7	adantr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} \in ℝ$
9	8	recnd	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} \in ℂ$
10		hstcl	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to S (B) \in ℋ$
11		normcl	$⊢ S (B) \in ℋ \to {norm}_{ℎ} (S (B)) \in ℝ$
12	10 11	syl	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to {norm}_{ℎ} (S (B)) \in ℝ$
13	12	resqcld	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (B))}^{2} \in ℝ$
14	13	adantlr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (B))}^{2} \in ℝ$
15	14	recnd	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (B))}^{2} \in ℂ$
16		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
17		hstcl	$⊢ (S \in CHStates \land ⊥ (B) \in C_{ℋ}) \to S (⊥ (B)) \in ℋ$
18	16 17	sylan2	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to S (⊥ (B)) \in ℋ$
19		normcl	$⊢ S (⊥ (B)) \in ℋ \to {norm}_{ℎ} (S (⊥ (B))) \in ℝ$
20	18 19	syl	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to {norm}_{ℎ} (S (⊥ (B))) \in ℝ$
21	20	resqcld	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (⊥ (B)))}^{2} \in ℝ$
22	21	adantlr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (⊥ (B)))}^{2} \in ℝ$
23	22	recnd	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (⊥ (B)))}^{2} \in ℂ$
24	9 15 23	add12d	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} = {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2}$
25	3 24	eqtr3d	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} + 1 = {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2}$
26	25	adantrr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (A))}^{2} + 1 = {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2}$
27	16	adantr	$⊢ (B \in C_{ℋ} \land A \subseteq B) \to ⊥ (B) \in C_{ℋ}$
28		ococ	$⊢ B \in C_{ℋ} \to ⊥ (⊥ (B)) = B$
29	28	sseq2d	$⊢ B \in C_{ℋ} \to (A \subseteq ⊥ (⊥ (B)) \leftrightarrow A \subseteq B)$
30	29	biimpar	$⊢ (B \in C_{ℋ} \land A \subseteq B) \to A \subseteq ⊥ (⊥ (B))$
31	27 30	jca	$⊢ (B \in C_{ℋ} \land A \subseteq B) \to (⊥ (B) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (B)))$
32		hstpyth	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (⊥ (B) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (B)))) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} = {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2}$
33	31 32	sylan2	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} = {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2}$
34		chjcl	$⊢ (A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to A \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
35	16 34	sylan2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
36		hstcl	$⊢ (S \in CHStates \land A \lor_{ℋ} ⊥ (B) \in C_{ℋ}) \to S (A \lor_{ℋ} ⊥ (B)) \in ℋ$
37	35 36	sylan2	$⊢ (S \in CHStates \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to S (A \lor_{ℋ} ⊥ (B)) \in ℋ$
38	37	anassrs	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to S (A \lor_{ℋ} ⊥ (B)) \in ℋ$
39		normcl	$⊢ S (A \lor_{ℋ} ⊥ (B)) \in ℋ \to {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \in ℝ$
40	38 39	syl	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \in ℝ$
41		normge0	$⊢ S (A \lor_{ℋ} ⊥ (B)) \in ℋ \to 0 \leq {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))$
42	38 41	syl	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to 0 \leq {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))$
43		hstle1	$⊢ (S \in CHStates \land A \lor_{ℋ} ⊥ (B) \in C_{ℋ}) \to {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \leq 1$
44	35 43	sylan2	$⊢ (S \in CHStates \land (A \in C_{ℋ} \land B \in C_{ℋ})) \to {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \leq 1$
45	44	anassrs	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \leq 1$
46		1re	$⊢ 1 \in ℝ$
47		le2sq2	$⊢ (({norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \in ℝ \land 0 \leq {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))) \land (1 \in ℝ \land {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \leq 1)) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} \leq 1^{2}$
48	46 47	mpanr1	$⊢ (({norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \in ℝ \land 0 \leq {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))) \land {norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B))) \leq 1) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} \leq 1^{2}$
49	40 42 45 48	syl21anc	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} \leq 1^{2}$
50		sq1	$⊢ 1^{2} = 1$
51	49 50	breqtrdi	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} \leq 1$
52	51	adantrr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (A \lor_{ℋ} ⊥ (B)))}^{2} \leq 1$
53	33 52	eqbrtrrd	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq 1$
54	8 22	readdcld	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \in ℝ$
55		leadd2	$⊢ ({{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \in ℝ \land 1 \in ℝ \land {{norm}_{ℎ} (S (B))}^{2} \in ℝ) \to ({{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq 1 \leftrightarrow {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
56	46 55	mp3an2	$⊢ ({{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \in ℝ \land {{norm}_{ℎ} (S (B))}^{2} \in ℝ) \to ({{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq 1 \leftrightarrow {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
57	54 14 56	syl2anc	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ({{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq 1 \leftrightarrow {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
58	57	adantrr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to ({{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq 1 \leftrightarrow {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
59	53 58	mpbid	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (B))}^{2} + {{norm}_{ℎ} (S (A))}^{2} + {{norm}_{ℎ} (S (⊥ (B)))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} + 1$
60	26 59	eqbrtrd	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (A))}^{2} + 1 \leq {{norm}_{ℎ} (S (B))}^{2} + 1$
61		leadd1	$⊢ ({{norm}_{ℎ} (S (A))}^{2} \in ℝ \land {{norm}_{ℎ} (S (B))}^{2} \in ℝ \land 1 \in ℝ) \to ({{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} + 1 \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
62	46 61	mp3an3	$⊢ ({{norm}_{ℎ} (S (A))}^{2} \in ℝ \land {{norm}_{ℎ} (S (B))}^{2} \in ℝ) \to ({{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} + 1 \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
63	8 14 62	syl2anc	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ({{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} + 1 \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
64	63	adantrr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to ({{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2} \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} + 1 \leq {{norm}_{ℎ} (S (B))}^{2} + 1)$
65	60 64	mpbird	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2}$
66		normge0	$⊢ S (A) \in ℋ \to 0 \leq {norm}_{ℎ} (S (A))$
67	4 66	syl	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to 0 \leq {norm}_{ℎ} (S (A))$
68	6 67	jca	$⊢ (S \in CHStates \land A \in C_{ℋ}) \to ({norm}_{ℎ} (S (A)) \in ℝ \land 0 \leq {norm}_{ℎ} (S (A)))$
69	68	adantr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ({norm}_{ℎ} (S (A)) \in ℝ \land 0 \leq {norm}_{ℎ} (S (A)))$
70		normge0	$⊢ S (B) \in ℋ \to 0 \leq {norm}_{ℎ} (S (B))$
71	10 70	syl	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to 0 \leq {norm}_{ℎ} (S (B))$
72	12 71	jca	$⊢ (S \in CHStates \land B \in C_{ℋ}) \to ({norm}_{ℎ} (S (B)) \in ℝ \land 0 \leq {norm}_{ℎ} (S (B)))$
73	72	adantlr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ({norm}_{ℎ} (S (B)) \in ℝ \land 0 \leq {norm}_{ℎ} (S (B)))$
74		le2sq	$⊢ (({norm}_{ℎ} (S (A)) \in ℝ \land 0 \leq {norm}_{ℎ} (S (A))) \land ({norm}_{ℎ} (S (B)) \in ℝ \land 0 \leq {norm}_{ℎ} (S (B)))) \to ({norm}_{ℎ} (S (A)) \leq {norm}_{ℎ} (S (B)) \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2})$
75	69 73 74	syl2anc	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land B \in C_{ℋ}) \to ({norm}_{ℎ} (S (A)) \leq {norm}_{ℎ} (S (B)) \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2})$
76	75	adantrr	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to ({norm}_{ℎ} (S (A)) \leq {norm}_{ℎ} (S (B)) \leftrightarrow {{norm}_{ℎ} (S (A))}^{2} \leq {{norm}_{ℎ} (S (B))}^{2})$
77	65 76	mpbird	$⊢ ((S \in CHStates \land A \in C_{ℋ}) \land (B \in C_{ℋ} \land A \subseteq B)) \to {norm}_{ℎ} (S (A)) \leq {norm}_{ℎ} (S (B))$

Metamath Proof Explorer

Theorem hstle

Proof