Theorem strlem3a 5693

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.

Hypothesis

Ref	Expression
strlem3a.1	|- S = {<.x, y>. | (x e. CH /\ y = ((norm` ((Proj` x)` u))^2))}

Assertion

Ref	Expression
strlem3a	|- ((u e. H~ /\ (norm` u) = 1) -> S e. States)

Distinct variable group(s):   x,u,y

Proof of Theorem strlem3a

Step	Hyp	Ref	Expression
1		pjhclt 5248	. . . . . . . . . 10 |- ((x e. CH /\ u e. H~) -> ((Proj` x)` u) e. H~)
2	1	adantrr 312	. . . . . . . . 9 |- ((x e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((Proj` x)` u) e. H~)
3		normclt 5076	. . . . . . . . 9 |- (((Proj` x)` u) e. H~ -> (norm` ((Proj` x)` u)) e. RR)
4		sqreclt 4697	. . . . . . . . 9 |- ((norm` ((Proj` x)` u)) e. RR -> ((norm` ((Proj` x)` u))^2) e. RR)
5	2, 3, 4	3syl 21	. . . . . . . 8 |- ((x e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((norm` ((Proj` x)` u))^2) e. RR)
6	5	exp 291	. . . . . . 7 |- (x e. CH -> ((u e. H~ /\ (norm` u) = 1) -> ((norm` ((Proj` x)` u))^2) e. RR))
7	6	com12 13	. . . . . 6 |- ((u e. H~ /\ (norm` u) = 1) -> (x e. CH -> ((norm` ((Proj` x)` u))^2) e. RR))
8	7	r19.21aiv 1259	. . . . 5 |- ((u e. H~ /\ (norm` u) = 1) -> A.x e. CH ((norm` ((Proj` x)` u))^2) e. RR)
9		strlem3a.1	. . . . . 6 |- S = {<.x, y>. | (x e. CH /\ y = ((norm` ((Proj` x)` u))^2))}
10	9	fopab2 2891	. . . . 5 |- (A.x e. CH ((norm` ((Proj` x)` u))^2) e. RR <-> S:CH-->RR)
11	8, 10	sylib 173	. . . 4 |- ((u e. H~ /\ (norm` u) = 1) -> S:CH-->RR)
12		pjhclt 5248	. . . . . . . . . . 11 |- ((z e. CH /\ u e. H~) -> ((Proj` z)` u) e. H~)
13	12	adantrr 312	. . . . . . . . . 10 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((Proj` z)` u) e. H~)
14		normclt 5076	. . . . . . . . . 10 |- (((Proj` z)` u) e. H~ -> (norm` ((Proj` z)` u)) e. RR)
15		sqege0t 4708	. . . . . . . . . 10 |- ((norm` ((Proj` z)` u)) e. RR -> 0 <_ ((norm` ((Proj` z)` u))^2))
16	13, 14, 15	3syl 21	. . . . . . . . 9 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> 0 <_ ((norm` ((Proj` z)` u))^2))
17	9	strlem2 5692	. . . . . . . . . 10 |- (z e. CH -> (S` z) = ((norm` ((Proj` z)` u))^2))
18	17	adantr 306	. . . . . . . . 9 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (S` z) = ((norm` ((Proj` z)` u))^2))
19	16, 18	breqtrrd 2083	. . . . . . . 8 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> 0 <_ (S` z))
20		pjnormt 5666	. . . . . . . . . . . . 13 |- ((z e. CH /\ u e. H~) -> (norm` ((Proj` z)` u)) <_ (norm` u))
21	20	adantrr 312	. . . . . . . . . . . 12 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (norm` ((Proj` z)` u)) <_ (norm` u))
22		pm3.27 260	. . . . . . . . . . . . 13 |- ((u e. H~ /\ (norm` u) = 1) -> (norm` u) = 1)
23	22	adantl 305	. . . . . . . . . . . 12 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (norm` u) = 1)
24	21, 23	breqtrd 2081	. . . . . . . . . . 11 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (norm` ((Proj` z)` u)) <_ 1)
25		le2sqet 4707	. . . . . . . . . . . 12 |- (((norm` ((Proj` z)` u)) e. RR /\ 1 e. RR) -> ((0 <_ (norm` ((Proj` z)` u)) /\ 0 <_ 1) -> ((norm` ((Proj` z)` u)) <_ 1 <-> ((norm` ((Proj` z)` u))^2) <_ (1^2))))
26	13, 14	syl 12	. . . . . . . . . . . . 13 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (norm` ((Proj` z)` u)) e. RR)
27		ax1re 4064	. . . . . . . . . . . . 13 |- 1 e. RR
28	26, 27	jctir 241	. . . . . . . . . . . 12 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((norm` ((Proj` z)` u)) e. RR /\ 1 e. RR))
29		normge0t 5077	. . . . . . . . . . . . . 14 |- (((Proj` z)` u) e. H~ -> 0 <_ (norm` ((Proj` z)` u)))
30	13, 29	syl 12	. . . . . . . . . . . . 13 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> 0 <_ (norm` ((Proj` z)` u)))
31		ax0re 4063	. . . . . . . . . . . . . 14 |- 0 e. RR
32		lt01 4377	. . . . . . . . . . . . . 14 |- 0 < 1
33	31, 27, 32	ltlei 4303	. . . . . . . . . . . . 13 |- 0 <_ 1
34	30, 33	jctir 241	. . . . . . . . . . . 12 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (0 <_ (norm` ((Proj` z)` u)) /\ 0 <_ 1))
35	25, 28, 34	sylc 62	. . . . . . . . . . 11 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((norm` ((Proj` z)` u)) <_ 1 <-> ((norm` ((Proj` z)` u))^2) <_ (1^2)))
36	24, 35	mpbid 170	. . . . . . . . . 10 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((norm` ((Proj` z)` u))^2) <_ (1^2))
37		sq1 4709	. . . . . . . . . 10 |- (1^2) = 1
38	36, 37	syl6breq 2093	. . . . . . . . 9 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> ((norm` ((Proj` z)` u))^2) <_ 1)
39	18, 38	eqbrtrd 2077	. . . . . . . 8 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (S` z) <_ 1)
40	19, 39	jca 236	. . . . . . 7 |- ((z e. CH /\ (u e. H~ /\ (norm` u) = 1)) -> (0 <_ (S` z) /\ (S` z) <_ 1))
41	40	exp 291	. . . . . 6 |- (z e. CH -> ((u e. H~ /\ (norm` u) = 1) -> (0 <_ (S` z) /\ (S` z) <_ 1)))
42	41	com12 13	. . . . 5 |- ((u e. H~ /\ (norm` u) = 1) -> (z e. CH -> (0 <_ (S` z) /\ (S` z) <_ 1)))
43	42	r19.21aiv 1259	. . . 4 |- ((u e. H~ /\ (norm` u) = 1) -> A.z e. CH (0 <_ (S` z) /\ (S` z) <_ 1))
44	11, 43	jca 236	. . 3 |- ((u e. H~ /\ (norm` u) = 1) -> (S:CH-->RR /\ A.z e. CH (0 <_ (S` z) /\ (S` z) <_ 1)))
45		pjch1t 5560	. . . . . . . 8 |- (u e. H~ -> ((Proj` H~)` u) = u)
46	45	fveq2d 2836	. . . . . . 7 |- (u e. H~ -> (norm` ((Proj` H~)` u)) = (norm` u))
47	46	opreq1d 3012	. . . . . 6 |- (u e. H~ -> ((norm` ((Proj` H~)` u))^2) = ((norm` u)^2))
48		opreq1 3006	. . . . . . 7 |- ((norm` u) = 1 -> ((norm` u)^2) = (1^2))
49	48, 37	syl6eq 1140	. . . . . 6 |- ((norm` u) = 1 -> ((norm` u)^2) = 1)
50	47, 49	sylan9eq 1144	. . . . 5 |- ((u e. H~ /\ (norm` u) = 1) -> ((norm` ((Proj` H~)` u))^2) = 1)
51		helch 5151	. . . . . 6 |- H~ e. CH
52	9	strlem2 5692	. . . . . 6 |- (H~ e. CH -> (S` H~) = ((norm` ((Proj` H~)` u))^2))
53	51, 52	ax-mp 6	. . . . 5 |- (S` H~) = ((norm` ((Proj` H~)` u))^2)
54	50, 53	syl5eq 1136	. . . 4 |- ((u e. H~ /\ (norm` u) = 1) -> (S` H~) = 1)
55		pjcjt2 5580	. . . . . . . . . . . . . . 15 |- ((z e. CH /\ w e. CH /\ u e. H~) -> (z (_ (_|_` w) -> ((Proj` (z vH w))` u) = (((Proj` z)` u) +v ((Proj` w)` u))))
56	55	imp 277	. . . . . . . . . . . . . 14 |- (((z e. CH /\ w e. CH /\ u e. H~) /\ z (_ (_|_` w)) -> ((Proj` (z vH w))` u) = (((Proj` z)` u) +v ((Proj` w)` u)))
57	56	fveq2d 2836	. . . . . . . . . . . . 13 |- (((z e. CH /\ w e. CH /\ u e. H~) /\ z (_ (_|_` w)) -> (norm` ((Proj` (z vH w))` u)) = (norm` (((Proj` z)` u) +v ((Proj` w)` u))))
58	57	opreq1d 3012	. . . . . . . . . . . 12 |- (((z e. CH /\ w e. CH /\ u e. H~) /\ z (_ (_|_` w)) -> ((norm` ((Proj` (z vH w))` u))^2) = ((norm` (((<