strlem3a

Description: Lemma for strong state 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, 28-Oct-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		strlem3a.1	$⊢ S = (x \in C_{ℋ} ⟼ {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2})$
2		id	$⊢ x \in C_{ℋ} \to x \in C_{ℋ}$
3		simpl	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to u \in ℋ$
4		pjhcl	$⊢ (x \in C_{ℋ} \land u \in ℋ) \to {proj}_{ℎ} (x) (u) \in ℋ$
5	2 3 4	syl2anr	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {proj}_{ℎ} (x) (u) \in ℋ$
6		normcl	$⊢ {proj}_{ℎ} (x) (u) \in ℋ \to {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \in ℝ$
7	5 6	syl	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \in ℝ$
8	7	resqcld	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \in ℝ$
9	7	sqge0d	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to 0 \leq {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2}$
10		normge0	$⊢ {proj}_{ℎ} (x) (u) \in ℋ \to 0 \leq {norm}_{ℎ} ({proj}_{ℎ} (x) (u))$
11	5 10	syl	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to 0 \leq {norm}_{ℎ} ({proj}_{ℎ} (x) (u))$
12		pjnorm	$⊢ (x \in C_{ℋ} \land u \in ℋ) \to {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \leq {norm}_{ℎ} (u)$
13	2 3 12	syl2anr	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \leq {norm}_{ℎ} (u)$
14		simplr	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {norm}_{ℎ} (u) = 1$
15	13 14	breqtrd	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \leq 1$
16		2nn0	$⊢ 2 \in ℕ_{0}$
17		exple1	$⊢ (({norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \in ℝ \land 0 \leq {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \land {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \leq 1) \land 2 \in ℕ_{0}) \to {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \leq 1$
18	16 17	mpan2	$⊢ ({norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \in ℝ \land 0 \leq {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \land {norm}_{ℎ} ({proj}_{ℎ} (x) (u)) \leq 1) \to {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \leq 1$
19	7 11 15 18	syl3anc	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \leq 1$
20		elicc01	$⊢ {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \in [0, 1] \leftrightarrow ({{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \in ℝ \land 0 \leq {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \land {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \leq 1)$
21	8 9 19 20	syl3anbrc	$⊢ ((u \in ℋ \land {norm}_{ℎ} (u) = 1) \land x \in C_{ℋ}) \to {{norm}_{ℎ} ({proj}_{ℎ} (x) (u))}^{2} \in [0, 1]$
22	21 1	fmptd	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to S : C_{ℋ} ⟶ [0, 1]$
23		helch	$⊢ ℋ \in C_{ℋ}$
24	1	strlem2	$⊢ ℋ \in C_{ℋ} \to S (ℋ) = {{norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u))}^{2}$
25	23 24	ax-mp	$⊢ S (ℋ) = {{norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u))}^{2}$
26		pjch1	$⊢ u \in ℋ \to {proj}_{ℎ} (ℋ) (u) = u$
27	26	fveq2d	$⊢ u \in ℋ \to {norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u)) = {norm}_{ℎ} (u)$
28	27	oveq1d	$⊢ u \in ℋ \to {{norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u))}^{2} = {{norm}_{ℎ} (u)}^{2}$
29		oveq1	$⊢ {norm}_{ℎ} (u) = 1 \to {{norm}_{ℎ} (u)}^{2} = 1^{2}$
30		sq1	$⊢ 1^{2} = 1$
31	29 30	eqtrdi	$⊢ {norm}_{ℎ} (u) = 1 \to {{norm}_{ℎ} (u)}^{2} = 1$
32	28 31	sylan9eq	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to {{norm}_{ℎ} ({proj}_{ℎ} (ℋ) (u))}^{2} = 1$
33	25 32	syl5eq	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to S (ℋ) = 1$
34		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))$
35	34	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)$
36	35	fveq2d	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to {norm}_{ℎ} ({proj}_{ℎ} (z \lor_{ℋ} w) (u)) = {norm}_{ℎ} ({proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u))$
37	36	oveq1d	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to {{norm}_{ℎ} ({proj}_{ℎ} (z \lor_{ℋ} w) (u))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u))}^{2}$
38		pjopyth	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to (z \subseteq ⊥ (w) \to {{norm}_{ℎ} ({proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (w) (u))}^{2})$
39	38	imp	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to {{norm}_{ℎ} ({proj}_{ℎ} (z) (u) +_{ℎ} {proj}_{ℎ} (w) (u))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (w) (u))}^{2}$
40	37 39	eqtrd	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to {{norm}_{ℎ} ({proj}_{ℎ} (z \lor_{ℋ} w) (u))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (w) (u))}^{2}$
41		chjcl	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ}) \to z \lor_{ℋ} w \in C_{ℋ}$
42	41	3adant3	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to z \lor_{ℋ} w \in C_{ℋ}$
43	42	adantr	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to z \lor_{ℋ} w \in C_{ℋ}$
44	1	strlem2	$⊢ z \lor_{ℋ} w \in C_{ℋ} \to S (z \lor_{ℋ} w) = {{norm}_{ℎ} ({proj}_{ℎ} (z \lor_{ℋ} w) (u))}^{2}$
45	43 44	syl	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z \lor_{ℋ} w) = {{norm}_{ℎ} ({proj}_{ℎ} (z \lor_{ℋ} w) (u))}^{2}$
46		3simpa	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \to (z \in C_{ℋ} \land w \in C_{ℋ})$
47	46	adantr	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to (z \in C_{ℋ} \land w \in C_{ℋ})$
48	1	strlem2	$⊢ z \in C_{ℋ} \to S (z) = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u))}^{2}$
49	1	strlem2	$⊢ w \in C_{ℋ} \to S (w) = {{norm}_{ℎ} ({proj}_{ℎ} (w) (u))}^{2}$
50	48 49	oveqan12d	$⊢ (z \in C_{ℋ} \land w \in C_{ℋ}) \to S (z) + S (w) = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (w) (u))}^{2}$
51	47 50	syl	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z) + S (w) = {{norm}_{ℎ} ({proj}_{ℎ} (z) (u))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (w) (u))}^{2}$
52	40 45 51	3eqtr4d	$⊢ ((z \in C_{ℋ} \land w \in C_{ℋ} \land u \in ℋ) \land z \subseteq ⊥ (w)) \to S (z \lor_{ℋ} w) = S (z) + S (w)$
53	52	3exp1	$⊢ z \in C_{ℋ} \to (w \in C_{ℋ} \to (u \in ℋ \to (z \subseteq ⊥ (w) \to S (z \lor_{ℋ} w) = S (z) + S (w))))$
54	53	com3r	$⊢ u \in ℋ \to (z \in C_{ℋ} \to (w \in C_{ℋ} \to (z \subseteq ⊥ (w) \to S (z \lor_{ℋ} w) = S (z) + S (w))))$
55	54	adantr	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (z \in C_{ℋ} \to (w \in C_{ℋ} \to (z \subseteq ⊥ (w) \to S (z \lor_{ℋ} w) = S (z) + S (w))))$
56	55	ralrimdv	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to (z \in C_{ℋ} \to \forall w \in C_{ℋ} (z \subseteq ⊥ (w) \to S (z \lor_{ℋ} w) = S (z) + S (w)))$
57	56	ralrimiv	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to \forall z \in C_{ℋ} \forall w \in C_{ℋ} (z \subseteq ⊥ (w) \to S (z \lor_{ℋ} w) = S (z) + S (w))$
58		isst	$⊢ S \in States \leftrightarrow (S : C_{ℋ} ⟶ [0, 1] \land S (ℋ) = 1 \land \forall z \in C_{ℋ} \forall w \in C_{ℋ} (z \subseteq ⊥ (w) \to S (z \lor_{ℋ} w) = S (z) + S (w)))$
59	22 33 57 58	syl3anbrc	$⊢ (u \in ℋ \land {norm}_{ℎ} (u) = 1) \to S \in States$

Metamath Proof Explorer

Theorem strlem3a

Proof