Theorem strlem3a 10179

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 = ((normh` ((proj` x)` u))^2))}

Assertion

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

Distinct variable group:   x,u,y

Proof of Theorem strlem3a

Step	Hyp	Ref	Expression
1		pjhclt 9243	. . . . . . . . 9 |- ((x e. CH /\ u e. H~) -> ((proj` x)` u) e. H~)
2	1	adantrr 395	. . . . . . . 8 |- ((x e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> ((proj` x)` u) e. H~)
3		normclt 8991	. . . . . . . 8 |- (((proj` x)` u) e. H~ -> (normh` ((proj` x)` u)) e. RR)
4		resqclt 6621	. . . . . . . 8 |- ((normh` ((proj` x)` u)) e. RR -> ((normh` ((proj` x)` u))^2) e. RR)
5	2, 3, 4	3syl 20	. . . . . . 7 |- ((x e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> ((normh` ((proj` x)` u))^2) e. RR)
6	5	expcom 374	. . . . . 6 |- ((u e. H~ /\ (normh` u) = 1) -> (x e. CH -> ((normh` ((proj` x)` u))^2) e. RR))
7	6	r19.21aiv 1713	. . . . 5 |- ((u e. H~ /\ (normh` u) = 1) -> A.x e. CH ((normh` ((proj` x)` u))^2) e. RR)
8		strlem3a.1	. . . . . 6 |- S = {<.x, y>. | (x e. CH /\ y = ((normh` ((proj` x)` u))^2))}
9	8	fopab2 3823	. . . . 5 |- (A.x e. CH ((normh` ((proj` x)` u))^2) e. RR <-> S:CH-->RR)
10	7, 9	sylib 198	. . . 4 |- ((u e. H~ /\ (normh` u) = 1) -> S:CH-->RR)
11		pjhclt 9243	. . . . . . . . . 10 |- ((z e. CH /\ u e. H~) -> ((proj` z)` u) e. H~)
12	11	adantrr 395	. . . . . . . . 9 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> ((proj` z)` u) e. H~)
13		normclt 8991	. . . . . . . . 9 |- (((proj` z)` u) e. H~ -> (normh` ((proj` z)` u)) e. RR)
14		sqge0t 6633	. . . . . . . . 9 |- ((normh` ((proj` z)` u)) e. RR -> 0 <_ ((normh` ((proj` z)` u))^2))
15	12, 13, 14	3syl 20	. . . . . . . 8 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> 0 <_ ((normh` ((proj` z)` u))^2))
16	8	strlem2 10178	. . . . . . . . 9 |- (z e. CH -> (S` z) = ((normh` ((proj` z)` u))^2))
17	16	adantr 389	. . . . . . . 8 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (S` z) = ((normh` ((proj` z)` u))^2))
18	15, 17	breqtrrd 2641	. . . . . . 7 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> 0 <_ (S` z))
19		pjnormt 9669	. . . . . . . . . . . 12 |- ((z e. CH /\ u e. H~) -> (normh` ((proj` z)` u)) <_ (normh` u))
20	19	adantrr 395	. . . . . . . . . . 11 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (normh` ((proj` z)` u)) <_ (normh` u))
21		simprr 415	. . . . . . . . . . 11 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (normh` u) = 1)
22	20, 21	breqtrd 2639	. . . . . . . . . 10 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (normh` ((proj` z)` u)) <_ 1)
23		1re 5435	. . . . . . . . . . . . 13 |- 1 e. RR
24		0re 5440	. . . . . . . . . . . . . 14 |- 0 e. RR
25		lt01 5680	. . . . . . . . . . . . . 14 |- 0 < 1
26	24, 23, 25	ltlei 5581	. . . . . . . . . . . . 13 |- 0 <_ 1
27	23, 26	pm3.2i 285	. . . . . . . . . . . 12 |- (1 e. RR /\ 0 <_ 1)
28		le2sqt 6631	. . . . . . . . . . . 12 |- ((((normh` ((proj` z)` u)) e. RR /\ 0 <_ (normh` ((proj` z)` u))) /\ (1 e. RR /\ 0 <_ 1)) -> ((normh` ((proj` z)` u)) <_ 1 <-> ((normh` ((proj` z)` u))^2) <_ (1^2)))
29	27, 28	mpan2 696	. . . . . . . . . . 11 |- (((normh` ((proj` z)` u)) e. RR /\ 0 <_ (normh` ((proj` z)` u))) -> ((normh` ((proj` z)` u)) <_ 1 <-> ((normh` ((proj` z)` u))^2) <_ (1^2)))
30	12, 13	syl 10	. . . . . . . . . . 11 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (normh` ((proj` z)` u)) e. RR)
31		normge0t 8992	. . . . . . . . . . . 12 |- (((proj` z)` u) e. H~ -> 0 <_ (normh` ((proj` z)` u)))
32	12, 31	syl 10	. . . . . . . . . . 11 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> 0 <_ (normh` ((proj` z)` u)))
33	29, 30, 32	sylanc 471	. . . . . . . . . 10 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> ((normh` ((proj` z)` u)) <_ 1 <-> ((normh` ((proj` z)` u))^2) <_ (1^2)))
34	22, 33	mpbid 195	. . . . . . . . 9 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> ((normh` ((proj` z)` u))^2) <_ (1^2))
35		sq1 6637	. . . . . . . . 9 |- (1^2) = 1
36	34, 35	syl6breq 2654	. . . . . . . 8 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> ((normh` ((proj` z)` u))^2) <_ 1)
37	17, 36	eqbrtrd 2635	. . . . . . 7 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (S` z) <_ 1)
38	18, 37	jca 288	. . . . . 6 |- ((z e. CH /\ (u e. H~ /\ (normh` u) = 1)) -> (0 <_ (S` z) /\ (S` z) <_ 1))
39	38	expcom 374	. . . . 5 |- ((u e. H~ /\ (normh` u) = 1) -> (z e. CH -> (0 <_ (S` z) /\ (S` z) <_ 1)))
40	39	r19.21aiv 1713	. . . 4 |- ((u e. H~ /\ (normh` u) = 1) -> A.z e. CH (0 <_ (S` z) /\ (S` z) <_ 1))
41	10, 40	jca 288	. . 3 |- ((u e. H~ /\ (normh` u) = 1) -> (S:CH-->RR /\ A.z e. CH (0 <_ (S` z) /\ (S` z) <_ 1)))
42		pjch1t 9615	. . . . . . . 8 |- (u e. H~ -> ((proj` H~)` u) = u)
43	42	fveq2d 3728	. . . . . . 7 |- (u e. H~ -> (normh` ((proj` H~)` u)) = (normh` u))
44	43	opreq1d 3975	. . . . . 6 |- (u e. H~ -> ((normh` ((proj` H~)` u))^2) = ((normh` u)^2))
45		opreq1 3968	. . . . . . 7 |- ((normh` u) = 1 -> ((normh` u)^2) = (1^2))
46	45, 35	syl6eq 1523	. . . . . 6 |- ((normh` u) = 1 -> ((normh` u)^2) = 1)
47	44, 46	sylan9eq 1527	. . . . 5 |- ((u e. H~ /\ (normh` u) = 1) -> ((normh` ((proj` H~)` u))^2) = 1)
48		helch 9116	. . . . . 6 |- H~ e. CH
49	8	strlem2 10178	. . . . . 6 |- (H~ e. CH -> (S` H~) = ((normh` ((proj` H~)` u))^2))
50	48, 49	ax-mp 7	. . . . 5 |- (S` H~) = ((normh` ((proj` H~)` u))^2)
51	47, 50	syl5eq 1519	. . . 4 |- ((u e. H~ /\ (normh` u) = 1) -> (S` H~) = 1)
52		pjcjt2 9637	. . . . . . . . . . . . . 14 |- ((z e. CH /\ w e. CH /\ u e. H~) -> (z (_ (_|_` w) -> ((proj` (z vH w))` u) = (((proj` z)` u) +h ((proj` w)` u))))
53	52	imp 350	. . . . . . . . . . . . 13 |- (((z e. CH /\ w e. CH /\ u e. H~) /\ z (_ (_|_` w)) -> ((proj` (z vH w))` u) = (((proj` z)` u) +h ((proj` w)` u)))
54	53	fveq2d 3728	. . . . . . . . . . . 12 |- (((z e. CH /\ w e. CH /\ u e. H~) /\ z (_ (_|_` w)) -> (normh` ((proj` (z vH w))` u)) = (normh` (((proj` z)` u) +h ((proj` w)` u))))
55	54	opreq1d 3975	. . . . . . . . . . 11 |- (((z e. CH /\ w e. CH /\ u e. H~) /\ z (_ (_|_` w)) -> ((normh` ((proj` (z vH w))` u))^2) = ((normh` (((proj` z)` u) +h ((proj` w)` u)))^2))
56		pjopytht 9665	. . . . . . . . . . . 12 |- ((z e. CH /\ w e. CH /\ u e. H~) -> (z (_ (_|_` w) -> ((normh` (((proj` z)` u) +h ((proj` w)` u)))^2) = (((normh` ((proj` z)` u))^2) + ((normh` ((proj` w)` u))^