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:H~-->H~   &   |- T:H~-->H~   =>   |- (S o. T) Fn H~
Theorem	hosf 5602	Mapping of sum of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +P T):H~-->H~
Theorem	hodf 5603	Mapping of difference of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S -P T):H~-->H~
Theorem	hosfn 5604	Functionality of sum of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +P T) Fn H~
Theorem	hoscom 5605	Commutativity of sum of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +P T) = (T +P S)
Theorem	hods 5606	Relationship between Hilbert space operator difference and sum.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R -P S) = T <-> (S +P T) = R)
Theorem	hosass 5607	Associativity of sum of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((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:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- (R +P (S +P T)) = (S +P (R +P T))
Theorem	hosdir 5609	Distributive law for Hilbert space operator sum.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R +P S) o. T) = ((R o. T) +P (S o. T))
Theorem	hoddir 5610	Distributive law for Hilbert space operator difference.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R -P S) o. T) = ((R o. T) -P (S o. T))
Theorem	ho2co 5611	Double composition of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A e. H~ -> (((R o. S) o. T)` A) = (R` (S` (T` A))))
Theorem	ho0 5612	Zero identity element for Hilbert space operators.
|- (Proj` 0H) = (H~ X. 0H)
Theorem	ho1 5613	Unit identity element for Hilbert space operators.
|- (Proj` H~) = (I |` H~)
Theorem	hoid0 5614	Sum of Hilbert space operator with zero identity.
|- T:H~-->H~   =>   |- (T +P (Proj` 0H)) = T
Theorem	hoid0r 5615	Sum of Hilbert space operator with zero identity.
|- T:H~-->H~   =>   |- ((Proj` 0H) +P T) = T
Theorem	hodid 5616	Difference of a Hilbert space operator from itself.
|- T:H~-->H~   =>   |- (T -P T) = (Proj` 0H)
Theorem	hoid1 5617	Composition of Hilbert space operator with unit identity.
|- T:H~-->H~   =>   |- (T o. (Proj` H~)) = T
Theorem	hoid1r 5618	Composition of Hilbert space operator with unit identity.
|- T:H~-->H~   =>   |- ((Proj` H~) o. T) = T
Theorem	hodseq 5619	Subtraction and addition of equal Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +P (T -P S)) = T
Theorem	hods0 5620	Subtraction of Hilbert space operators expressed in terms of difference from zero.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S -P T) = (S +P ((Proj` 0H) -P T))
Theorem	hosdass 5621	Associativity of sum and difference of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R +P S) -P T) = (R +P (S -P T))
Theorem	hosd 5622	Law for sum and difference of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R +P S) -P T) = ((R -P T) +P S)
Theorem	hosd1 5623	Hilbert space operator sum expressed in terms of difference.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +P T) = (S -P ((Proj` 0H) -P T))
Theorem	hosd2 5624	Hilbert space operator sum expressed in terms of difference.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +P T) = (S -P ((T -P T) -P T))
Theorem	pjsdi 5625	Distributive law for Hilbert space operator sum.
|- H e. CH   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((Proj` H) o. (S +P T)) = (((Proj` H) o. S) +P ((Proj` H) o. T))
Theorem	pjddi 5626	Distributive law for Hilbert space operator difference.
|- H e. CH   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((Proj` H) o. (S -P T)) = (((Proj` H) o. S) -P ((Proj` H) o. T))
Theorem	pjsdi2 5627	Chained distributive law for Hilbert space operator difference.
|- H e. CH   &   |- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R o. (S +P T)) = ((R o. S) +P (R o. T)) -> (((Proj` H) o. R) o. (S +P T)) = ((((Proj` H) o. R) o. S) +P (((Proj` H) o. R) o. T)))
Theorem	pjco 5628	Composition of projections.
|- G e. CH   &   |- H e. CH   =>   |- (A e. H~ -> (((Proj` G) o. (Proj` H))` A) = ((Proj` G)` ((Proj` H)` A)))
Theorem	pjcocl 5629	Closure of composition of projections.
|- G e. CH   &   |- H e. CH   =>   |- (A e. H~ -> (((Proj` G) o. (Proj` H))` A) e. G)
Theorem	pjcohcl 5630	Closure of composition of projections.
|- G e. CH   &   |- H e. CH   =>   |- (A e. H~ -> (((Proj` G) o. (Proj` H))` A) e. H~)
Theorem	pjadjco 5631	Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106.
|- G e. CH   &   |- H e. CH   =>   |- ((A e. H~ /\ B e. H~) -> ((((Proj` G) o. (Proj` H))` A) .i B) = (A .i (((Proj` H) o. (Proj` G))` B)))
Theorem	pjcofn 5632	Functionality of composition of projections.
|- G e. CH   &   |- H e. CH   =>   |- ((Proj` G) o. (Proj` H)) Fn H~
Theorem	pjss1co 5633	Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112.
|- G e. CH   &   |- H e. CH   =>   |- (G (_ H <-> ((Proj` H) o. (Proj` G)) = (Proj` G))
Theorem	pjss2co 5634	Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112.
|- G e. CH   &   |- H e. CH   =>   |- (G (_ H <-> ((Proj` G) o. (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 e. CH   &   |- H e. CH   =>   |- (A e. H~ -> (H (_ G -> (((Proj` G)` A) -v ((Proj` H)` A)) = ((Proj` (G i^i (_|_` H)))` A)))
Theorem	pjssge0t 5636	Theorem 4.5(iv)->(v) of [Beran] p. 112.
|- G e. CH   &   |- H e. CH   =>   |- (A e. H~ -> ((((Proj` G)` A) -v ((Proj` H)` A)) = ((Proj` (G i^i (_|_` 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 e. CH   &   |- H e. CH   =>   |- (A e. H~ -> (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 e. CH   &   |- H e. CH   =>   |- (G (_ H <-> A.x e. H~ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)))
Theorem	pjorthco 5639	Composition of projections of orthogonal subspaces.
|- G e. CH   &   |- H e. CH   =>   |- (G (_ (_|_` H) -> ((Proj` G) o. (Proj` H)) = (Proj` 0H))
Theorem	pjscj 5640	The projection of orthogonal subspaces is the sum of the projections.
|- G e. CH   &   |- H e. CH   =>   |- (G (_ (_|_` H) -> (Proj` (G vH H)) = ((Proj` G) +P (Proj` H)))
Theorem	pjssum 5641	The projection on a subspace sum is the sum of the projections.
|- G e. CH   &   |- H e. CH   =>   |- (G (_ (_|_` H) -> (Proj` (G +H H)) = ((Proj` G) +P (Proj` H)))
Theorem	pjidmco 5642	A projection is idempotent. Property (ii) of [Beran] p. 109.
|- H e. CH   =>   |- ((Proj` H) o. (Proj` H)) = (Proj` H)
Theorem	pjocco 5643	Composition of projections of a subspace and its orthocomplement.
|- H e. CH   =>   |- ((Proj` H) o. (Proj` (_|_` H))) = (Proj` 0H)
Theorem	pjtot 5644	Subspace sum of projection and projection of orthocomplement.
|- H e. CH   =>   |- ((Proj` H) +P (Proj` (_|_` H))) = (Proj` H~)
Theorem	pjoc 5645	Projection of orthocomplement.
|- H e.