Metamath Proof Explorer - mmtheorems57

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 5601-5700 - Page 57 of 58

Type	Label	Description
Statement
Theorem	hocofn 5601	Functionality of composition of Hilbert space operators.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S ∘ T) Fn ℋ
Theorem	hosf 5602	Mapping of sum of Hilbert space operators.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S +P T): ℋ –→ ℋ
Theorem	hodf 5603	Mapping of difference of Hilbert space operators.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S −P T): ℋ –→ ℋ
Theorem	hosfn 5604	Functionality of sum of Hilbert space operators.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S +P T) Fn ℋ
Theorem	hoscom 5605	Commutativity of sum of Hilbert space operators.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S +P T) = (T +P S)
Theorem	hods 5606	Relationship between Hilbert space operator difference and sum.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R −P S) = T ↔ (S +P T) = R)
Theorem	hosass 5607	Associativity of sum of Hilbert space operators.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R +P S) +P T) = (R +P (S +P T))
Theorem	hos12 5608	Commutative/associative law for Hilbert space operator sum that swaps the first two terms.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (R +P (S +P T)) = (S +P (R +P T))
Theorem	hosdir 5609	Distributive law for Hilbert space operator sum.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R +P S) ∘ T) = ((R ∘ T) +P (S ∘ T))
Theorem	hoddir 5610	Distributive law for Hilbert space operator difference.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R −P S) ∘ T) = ((R ∘ T) −P (S ∘ T))
Theorem	ho2co 5611	Double composition of Hilbert space operators.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (A ∈ ℋ → (((R ∘ S) ∘ T) ‘A) = (R ‘(S ‘(T ‘A))))
Theorem	ho0 5612	Zero identity element for Hilbert space operators.
⊢ (Proj ‘0ℋ) = ( ℋ × 0ℋ)
Theorem	ho1 5613	Unit identity element for Hilbert space operators.
⊢ (Proj ‘ ℋ ) = (I ↾ ℋ )
Theorem	hoid0 5614	Sum of Hilbert space operator with zero identity.
⊢ T: ℋ –→ ℋ    ⇒   ⊢ (T +P (Proj ‘0ℋ)) = T
Theorem	hoid0r 5615	Sum of Hilbert space operator with zero identity.
⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((Proj ‘0ℋ) +P T) = T
Theorem	hodid 5616	Difference of a Hilbert space operator from itself.
⊢ T: ℋ –→ ℋ    ⇒   ⊢ (T −P T) = (Proj ‘0ℋ)
Theorem	hoid1 5617	Composition of Hilbert space operator with unit identity.
⊢ T: ℋ –→ ℋ    ⇒   ⊢ (T ∘ (Proj ‘ ℋ )) = T
Theorem	hoid1r 5618	Composition of Hilbert space operator with unit identity.
⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((Proj ‘ ℋ ) ∘ T) = T
Theorem	hodseq 5619	Subtraction and addition of equal Hilbert space operators.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S +P (T −P S)) = T
Theorem	hods0 5620	Subtraction of Hilbert space operators expressed in terms of difference from zero.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S −P T) = (S +P ((Proj ‘0ℋ) −P T))
Theorem	hosdass 5621	Associativity of sum and difference of Hilbert space operators.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R +P S) −P T) = (R +P (S −P T))
Theorem	hosd 5622	Law for sum and difference of Hilbert space operators.
⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R +P S) −P T) = ((R −P T) +P S)
Theorem	hosd1 5623	Hilbert space operator sum expressed in terms of difference.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S +P T) = (S −P ((Proj ‘0ℋ) −P T))
Theorem	hosd2 5624	Hilbert space operator sum expressed in terms of difference.
⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (S +P T) = (S −P ((T −P T) −P T))
Theorem	pjsdi 5625	Distributive law for Hilbert space operator sum.
⊢ H ∈ Cℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((Proj ‘H) ∘ (S +P T)) = (((Proj ‘H) ∘ S) +P ((Proj ‘H) ∘ T))
Theorem	pjddi 5626	Distributive law for Hilbert space operator difference.
⊢ H ∈ Cℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((Proj ‘H) ∘ (S −P T)) = (((Proj ‘H) ∘ S) −P ((Proj ‘H) ∘ T))
Theorem	pjsdi2 5627	Chained distributive law for Hilbert space operator difference.
⊢ H ∈ Cℋ    &   ⊢ R: ℋ –→ ℋ    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ ((R ∘ (S +P T)) = ((R ∘ S) +P (R ∘ T)) → (((Proj ‘H) ∘ R) ∘ (S +P T)) = ((((Proj ‘H) ∘ R) ∘ S) +P (((Proj ‘H) ∘ R) ∘ T)))
Theorem	pjco 5628	Composition of projections.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘A) = ((Proj ‘G) ‘((Proj ‘H) ‘A)))
Theorem	pjcocl 5629	Closure of composition of projections.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘A) ∈ G)
Theorem	pjcohcl 5630	Closure of composition of projections.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘A) ∈ ℋ )
Theorem	pjadjco 5631	Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘A) ·i B) = (A ·i (((Proj ‘H) ∘ (Proj ‘G)) ‘B)))
Theorem	pjcofn 5632	Functionality of composition of projections.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ ((Proj ‘G) ∘ (Proj ‘H)) Fn ℋ
Theorem	pjss1co 5633	Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G ⊆ H ↔ ((Proj ‘H) ∘ (Proj ‘G)) = (Proj ‘G))
Theorem	pjss2co 5634	Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G ⊆ H ↔ ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘G))
Theorem	pjssmt 5635	Projection meet property. Remark of [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → (H ⊆ G → (((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) = ((Proj ‘(G ∩ (⊥ ‘H))) ‘A)))
Theorem	pjssge0t 5636	Theorem 4.5(iv)->(v) of [Beran] p. 112.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → ((((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) = ((Proj ‘(G ∩ (⊥ ‘H))) ‘A) → 0 ≤ ((((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) ·i A)))
Theorem	pjdifnormt 5637	Theorem 4.5(v)<->(vi) of [Beran] p. 112.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → (0 ≤ ((((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) ·i A) ↔ (norm ‘((Proj ‘H) ‘A)) ≤ (norm ‘((Proj ‘G) ‘A))))
Theorem	pjnormss 5638	Theorem 4.5(i)<->(vi) of [Beran] p. 112.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G ⊆ H ↔ ∀x ∈ ℋ (norm ‘((Proj ‘G) ‘x)) ≤ (norm ‘((Proj ‘H) ‘x)))
Theorem	pjorthco 5639	Composition of projections of orthogonal subspaces.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G ⊆ (⊥ ‘H) → ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘0ℋ))
Theorem	pjscj 5640	The projection of orthogonal subspaces is the sum of the projections.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G ⊆ (⊥ ‘H) → (Proj ‘(G ∨ℋ H)) = ((Proj ‘G) +P (Proj ‘H)))
Theorem	pjssum 5641	The projection on a subspace sum is the sum of the projections.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G ⊆ (⊥ ‘H) → (Proj ‘(G +ℋ H)) = ((Proj ‘G) +P (Proj ‘H)))
Theorem	pjidmco 5642	A projection is idempotent. Property (ii) of [Beran] p. 109.
⊢ H ∈ Cℋ    ⇒   ⊢ ((Proj ‘H) ∘ (Proj ‘H)) = (Proj ‘H)
Theorem	pjocco 5643	Composition of projections of a subspace and its orthocomplement.
⊢ H ∈ Cℋ    ⇒   ⊢ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘H))) = (Proj ‘0ℋ)
Theorem	pjtot 5644	Subspace sum of projection and projection of orthocomplement.
⊢ H ∈ Cℋ    ⇒   ⊢ ((Proj ‘H) +P (Proj ‘(⊥ ‘H))) = (Proj ‘ ℋ )
Theorem	pjoc 5645	Projection of orthocomplement.
⊢ H ∈ Cℋ    ⇒   ⊢ ((Proj ‘ ℋ ) −P (Proj ‘H)) = (Proj ‘(⊥ ‘H))
Theorem	pjin1 5646	Lemma for Theorem 1.22 of Mittelstaedt, p. 20.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (Proj ‘(G ∩ H)) = ((Proj ‘G) ∘ (Proj ‘(G ∩ H)))
Theorem	pjin2 5647	Lemma for Theorem 1.22 of Mittelstaedt, p. 20.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((Proj ‘G) = ((Proj ‘G) ∘ (Proj ‘H)) ∧ (Proj ‘H) = ((Proj ‘H) ∘ (Proj ‘G))) ↔ (Proj ‘G) = (Proj ‘H))
Theorem	pjin3 5648	Lemma for Theorem 1.22 of Mittelstaedt, p. 20.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((Proj ‘F) = ((Proj ‘F) ∘ (Proj ‘G)) ∧ (Proj ‘F) = ((Proj ‘F) ∘ (Proj ‘H))) ↔ (Proj ‘F) = ((Proj ‘F) ∘ (Proj ‘(G ∩ H))))
Theorem	pjclem1 5649	Lemma for projection commutation theorem.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G Com H → ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘(G ∩ H)))
Theorem	pjclem2 5650	Lemma for projection commutation theorem.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G Com H → ((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)))
Theorem	pjclem3 5651	Lemma for projection commutation theorem.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ((Proj ‘G) ∘ (Proj ‘(⊥ ‘H))) = ((Proj ‘(⊥ ‘H)) ∘ (Proj ‘G)))
Theorem	pjclem4a 5652	Lemma for projection commutation theorem.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ (G ∩ H) → (((Proj ‘G) ∘ (Proj ‘H)) ‘A) = A)
Theorem	pjclem4 5653	Lemma for projection commutation theorem.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘(G ∩ H)))
Theorem	pjc 5654	Two subspaces commute iff their projections commute. Lemma 4 of [Kalmbach] p. 67.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (G Com H ↔ ((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)))
Theorem	pjcohocl 5655	Closure of composition of projection and Hilbert space operator.
⊢ H ∈ Cℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (A ∈ ℋ → (((Proj ‘H) ∘ T) ‘A) ∈ H)
Theorem	pjadj2co 5656	Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of [Beran] p. 106.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (((((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) ‘A) ·i B) = (A ·i ((((Proj ‘H) ∘ (Proj ‘G)) ∘ (Proj ‘F)) ‘B)))
Theorem	pj2cocl 5657	Closure of double composition of projections.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → ((((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) ‘A) ∈ F)
Theorem	pj3lem1 5658	Lemma for projection triplet theorem.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ((F ∩ G) ∩ H) → ((((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) ‘A) = A)
Theorem	pj3s 5659	Stronger projection triplet theorem.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (((Proj ‘H) ∘ (Proj ‘G)) ∘ (Proj ‘F)) ∧ ran (((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) ⊆ G) → (((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (Proj ‘((F ∩ G) ∩ H)))
Theorem	pj3 5660	Projection triplet theorem.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (((Proj ‘H) ∘ (Proj ‘G)) ∘ (Proj ‘F)) ∧ (((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (((Proj ‘G) ∘ (Proj ‘F)) ∘ (Proj ‘H))) → (((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (Proj ‘((F ∩ G) ∩ H)))
Theorem	pj3cor1 5661	Projection triplet corollary.
⊢ F ∈ Cℋ    &   ⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (((((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (((Proj ‘H) ∘ (Proj ‘G)) ∘ (Proj ‘F)) ∧ (((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (((Proj ‘G) ∘ (Proj ‘F)) ∘ (Proj ‘H))) → (((Proj ‘F) ∘ (Proj ‘G)) ∘ (Proj ‘H)) = (((Proj ‘H) ∘ (Proj ‘F)) ∘ (Proj ‘G)))
Theorem	pjopytht 5662	Pythagorean theorem for projections on orthogonal subspaces.
⊢ ((H ∈ Cℋ ∧ G ∈ Cℋ ∧ A ∈ ℋ ) → (H ⊆ (⊥ ‘G) → ((norm ‘(((Proj ‘H) ‘A) +v ((Proj ‘G) ‘A)))↑2) = (((norm ‘((Proj ‘H) ‘A))↑2) + ((norm ‘((Proj ‘G) ‘A))↑2))))
Theorem	pjnorm 5663	The norm of the projection is less than or equal to the norm.
⊢ H ∈ Cℋ    &   ⊢ A ∈ ℋ    ⇒   ⊢ (norm ‘((Proj ‘H) ‘A)) ≤ (norm ‘A)
Theorem	pjpyth 5664	Pythagorean theorem for projections.
⊢ H ∈ Cℋ    &   ⊢ A ∈ ℋ    ⇒   ⊢ ((norm ‘A)↑2) = (((norm ‘((Proj ‘H) ‘A))↑2) + ((norm ‘((Proj ‘(⊥ ‘H)) ‘A))↑2))
Theorem	pjnel 5665	If a vector does not belong to subspace, the norm of its projection is less than its norm.
⊢ H ∈ Cℋ    &   ⊢ A ∈ ℋ    ⇒   ⊢ (¬ A ∈ H ↔ (norm ‘((Proj ‘H) ‘A)) < (norm ‘A))
Theorem	pjnormt 5666	The norm of the projection is less than or equal to the norm.
⊢ ((H ∈ Cℋ ∧ A ∈ ℋ ) → (norm ‘((Proj ‘H) ‘A)) ≤ (norm ‘A))
Theorem	pjnelt 5667	If a vector does not belong to subspace, the norm of its projection is less than its norm.
⊢ ((H ∈ Cℋ ∧ A ∈ ℋ ) → (¬ A ∈ H ↔ (norm ‘((Proj ‘H) ‘A)) < (norm ‘A)))
Theorem	pjelt 5668	If a vector belongs to a subspace, the norm of its projection equals its norm.
⊢ ((H ∈ Cℋ ∧ A ∈ ℋ ) → (A ∈ H ↔ (norm ‘((Proj ‘H) ‘A)) = (norm ‘A)))
Theorem	pjs14 5669	Theorem S-14 of Watanabe, p. 486.
⊢ G ∈ Cℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ ℋ → (norm ‘(((Proj ‘H) ∘ (Proj ‘G)) ‘A)) ≤ (norm ‘((Proj ‘G) ‘A)))
Definition	df-st 5670	Define the set of states on a Hilbert lattice. Definition of [Kalmbach] p. 266.
⊢ States = {f∣((f: Cℋ –→ℝ ∧ ∀x ∈ Cℋ (0 ≤ (f ‘x) ∧ (f ‘x) ≤ 1)) ∧ ((f ‘ ℋ ) = 1 ∧ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))))}
Theorem	stelt 5671	Property of a state.
⊢ (S ∈ States ↔ ((S: Cℋ –→ℝ ∧ ∀x ∈ Cℋ (0 ≤ (S ‘x) ∧ (S ‘x) ≤ 1)) ∧ ((S ‘ ℋ ) = 1 ∧ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (S ‘(x ∨ℋ y)) = ((S ‘x) + (S ‘y))))))
Theorem	stclt 5672	Real closure of the value of a state.
⊢ (S ∈ States → (A ∈ Cℋ → (S ‘A) ∈ ℝ))
Theorem	stge0t 5673	The value of a state is nonnegative.
⊢ (S ∈ States → (A ∈ Cℋ → 0 ≤ (S ‘A)))
Theorem	stle1t 5674	The value of a state is less than or equal to one.
⊢ (S ∈ States → (A ∈ Cℋ → (S ‘A) ≤ 1))
Theorem	sthil 5675	The value of a state at the full Hilbert space.
⊢ (S ∈ States → (S ‘ ℋ ) = 1)
Theorem	stjt 5676	The value of a state on a join.
⊢ (S ∈ States → (((A ∈ Cℋ ∧ B ∈ Cℋ ) ∧ A ⊆ (⊥ ‘B)) → (S ‘(A ∨ℋ B)) = ((S ‘A) + (S ‘B))))
Theorem	sto1 5677	The state of a subspace plus the state of its orthocomplement.
⊢ A ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((S ‘A) + (S ‘(⊥ ‘A))) = 1)
Theorem	sto2 5678	The state of the orthocomplement.
⊢ A ∈ Cℋ    ⇒   ⊢ (S ∈ States → (S ‘(⊥ ‘A)) = (1 − (S ‘A)))
Theorem	stge1 5679	If a state is greater than or equal to 1, it is 1.
⊢ A ∈ Cℋ    ⇒   ⊢ (S ∈ States → (1 ≤ (S ‘A) ↔ (S ‘A) = 1))
Theorem	stle0 5680	If a state is less than or equal to 0, it is 0.
⊢ A ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((S ‘A) ≤ 0 ↔ (S ‘A) = 0))
Theorem	stle 5681	Ordering law for states.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → (A ⊆ B → (S ‘A) ≤ (S ‘B)))
Theorem	stles 5682	Ordering law for states.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → (A ⊆ B → ((S ‘A) = 1 → (S ‘B) = 1)))
Theorem	stji1 5683	Join of components of Sasaki arrow ->1.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → (S ‘((⊥ ‘A) ∨ℋ (A ∩ B))) = ((S ‘(⊥ ‘A)) + (S ‘(A ∩ B))))
Theorem	stm1 5684	State of component of unit meet.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((S ‘(A ∩ B)) = 1 → (S ‘A) = 1))
Theorem	stm1r 5685	State of component of unit meet.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((S ‘(A ∩ B)) = 1 → (S ‘B) = 1))
Theorem	stm1add 5686	Sum of states whose meet is 1.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((S ‘(A ∩ B)) = 1 → ((S ‘A) + (S ‘B)) = 2))
Theorem	stadd 5687	If the sum of 2 states is 2, then each state is 1.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (S ∈ States → (((S ‘A) + (S ‘B)) = 2 → (S ‘A) = 1))
Theorem	stm1add3 5688	Sum of states whose meet is 1.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((S ‘((A ∩ B) ∩ C)) = 1 → (((S ‘A) + (S ‘B)) + (S ‘C)) = 3))
Theorem	stadd3 5689	If the sum of 3 states is 3, then each state is 1.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ (S ∈ States → ((((S ‘A) + (S ‘B)) + (S ‘C)) = 3 → (S ‘A) = 1))
Theorem	st0 5690	The state of the zero subspace.
⊢ (S ∈ States → (S ‘0ℋ) = 0)
Theorem	strlem1 5691	Lemma for strong state theorem: if closed subspace A is not contained in B, there is a unit vector u in their difference.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (¬ A ⊆ B → ∃u ∈ (A ∖ B)(norm ‘u) = 1)
Theorem	strlem2 5692	Lemma for strong state theorem.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    ⇒   ⊢ (C ∈ Cℋ → (S ‘C) = ((norm ‘((Proj ‘C) ‘u))↑2))
Theorem	strlem3a 5693	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.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    ⇒   ⊢ ((u ∈ ℋ ∧ (norm ‘u) = 1) → S ∈ States)
Theorem	strlem3 5694	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. This lemma restates the hypotheses in a more convenient form to work with.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    &   ⊢ (φ ↔ (u ∈ (A ∖ B) ∧ (norm ‘u) = 1))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → S ∈ States)
Theorem	strlem4 5695	Lemma for strong state theorem.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    &   ⊢ (φ ↔ (u ∈ (A ∖ B) ∧ (norm ‘u) = 1))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → (S ‘A) = 1)
Theorem	strlem5 5696	Lemma for strong state theorem.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    &   ⊢ (φ ↔ (u ∈ (A ∖ B) ∧ (norm ‘u) = 1))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → (S ‘B) < 1)
Theorem	strlem6 5697	Lemma for strong state theorem.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    &   ⊢ (φ ↔ (u ∈ (A ∖ B) ∧ (norm ‘u) = 1))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → ¬ ((S ‘A) = 1 → (S ‘B) = 1))
Theorem	str 5698	Strong state theorem. The states on a Hilbert lattice define an ordering. Remark of [Mayet] p. 370.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (∀f ∈ States ((f ‘A) = 1 → (f ‘B) = 1) → A ⊆ B)
Theorem	strb 5699	Strong state theorem (bidirectional version).
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (∀f ∈ States ((f ‘A) = 1 → (f ‘B) = 1) ↔ A ⊆ B)
Theorem	large 5700	A Hilbert lattice admits a large set of states. Remark of [Mayet] p. 370.
⊢ A ∈ Cℋ    ⇒   ⊢ (¬ A = 0ℋ ↔ ∃f ∈ States (f ‘A) = 1)