mmtheorems97 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10688

Statement List for Metamath Proof Explorer - 9601-9700 - Page 97 of 107

Type	Label	Description
Statement
Theorem	pjssge0 9601	Theorem 4.5(iv)->(v) of [Beran] p. 112.
|- H e. CH   &   |- A e. H~   &   |- G e. CH   =>   |- ((((proj` G)` A) -h ((proj` H)` A)) = ((proj` (G i^i (_|_` H)))` A) -> 0 <_ ((((proj` G)` A) -h ((proj` H)` A)) .ih A))
Theorem	pjdifnorm 9602	Theorem 4.5(v)<->(vi) of [Beran] p. 112.
|- H e. CH   &   |- A e. H~   &   |- G e. CH   =>   |- (0 <_ ((((proj` G)` A) -h ((proj` H)` A)) .ih A) <-> (normh` ((proj` H)` A)) <_ (normh` ((proj` G)` A)))
Theorem	pjcj 9603	The projection on a subspace join is the sum of the projections.
|- H e. CH   &   |- A e. H~   &   |- G e. CH   =>   |- (H (_ (_|_` G) -> ((proj` (H vH G))` A) = (((proj` H)` A) +h ((proj` G)` A)))
Theorem	pjadjt 9604	A projection is self-adjoint. Property (i) of [Beran] p. 109.
|- H e. CH   =>   |- ((A e. H~ /\ B e. H~) -> (((proj` H)` A) .ih B) = (A .ih ((proj` H)` B)))
Theorem	pjaddt 9605	Projection of vector sum is sum of projections.
|- H e. CH   =>   |- ((A e. H~ /\ B e. H~) -> ((proj` H)` (A +h B)) = (((proj` H)` A) +h ((proj` H)` B)))
Theorem	pjinormt 9606	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44.
|- H e. CH   =>   |- (A e. H~ -> (((proj` H)` A) .ih A) = ((normh` ((proj` H)` A))^2))
Theorem	pjsubt 9607	Projection of vector difference is difference of projections.
|- H e. CH   =>   |- ((A e. H~ /\ B e. H~) -> ((proj` H)` (A -h B)) = (((proj` H)` A) -h ((proj` H)` B)))
Theorem	pjmult 9608	Projection of scalar product is scalar product of projection.
|- H e. CH   =>   |- ((A e. CC /\ B e. H~) -> ((proj` H)` (A .h B)) = (A .h ((proj` H)` B)))
Theorem	pjige0 9609	The inner product of a projection and its argument is nonnegative.
|- H e. CH   =>   |- (A e. H~ -> 0 <_ (((proj` H)` A) .ih A))
Theorem	pjige0t 9610	The inner product of a projection and its argument is nonnegative.
|- ((H e. CH /\ A e. H~) -> 0 <_ (((proj` H)` A) .ih A))
Theorem	pjcjt2 9611	The projection on a subspace join is the sum of the projections.
|- ((H e. CH /\ G e. CH /\ A e. H~) -> (H (_ (_|_` G) -> ((proj` (H vH G))` A) = (((proj` H)` A) +h ((proj` G)` A))))
Theorem	pj0 9612	The projection of the zero vector.
|- H e. CH   =>   |- ((proj` H)` 0h) = 0h
Theorem	pjcht 9613	Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111.
|- ((H e. CH /\ A e. H~) -> (A e. H <-> ((proj` H)` A) = A))
Theorem	pjidt 9614	The projection of a vector in the projection subspace is itself.
|- ((H e. CH /\ A e. H) -> ((proj` H)` A) = A)
Theorem	pjvect 9615	The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of [Halmos] p. 44.
|- (H e. CH -> H = {x e. H~ | ((proj` H)` x) = x})
Theorem	pjocvect 9616	The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of [Halmos] p. 45.
|- (H e. CH -> (_|_` H) = {x e. H~ | ((proj` H)` x) = 0h})
Theorem	pjocin 9617	Membership of projection in orthocomplement of intersection.
|- G e. CH   &   |- H e. CH   =>   |- (A e. (_|_` (G i^i H)) -> ((proj` G)` A) e. (_|_` (G i^i H)))
Theorem	pjin 9618	Membership of projection in an intersection.
|- G e. CH   &   |- H e. CH   =>   |- (A e. (G i^i H) -> ((proj` G)` A) e. (G i^i H))
Theorem	pjjs 9619	A sufficient condition for subspace join to be equal to subspace sum.
|- G e. CH   &   |- H e. SH   =>   |- (A.x e. (G vH H)((proj` (_|_` G))` x) e. H -> (G vH H) = (G +H H))
Theorem	pjfn 9620	Functionality of a projection.
|- H e. CH   =>   |- (proj` H) Fn H~
Theorem	pjrn 9621	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44.
|- H e. CH   =>   |- ran (proj` H) = H
Theorem	pjfo 9622	A projection maps onto its subspace.
|- H e. CH   =>   |- (proj` H):H~-onto->H
Theorem	pjf 9623	The mapping of a projection.
|- H e. CH   =>   |- (proj` H):H~-->H~
Theorem	pjv 9624	The value of a projection in terms of components.
|- H e. CH   =>   |- ((A e. H /\ B e. (_|_` H)) -> ((proj` H)` (A +h B)) = A)
Theorem	pjfot 9625	A projection maps onto its subspace.
|- (H e. CH -> (proj` H):H~-onto->H)
Theorem	pjrnt 9626	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44.
|- (H e. CH -> ran (proj` H) = H)
Theorem	pjft 9627	The mapping of a projection.
|- (H e. CH -> (proj` H):H~-->H~)
Theorem	pjfnt 9628	Functionality of a projection.
|- (H e. CH -> (proj` H) Fn H~)
Theorem	pjsumt 9629	The projection on a subspace sum is the sum of the projections.
|- G e. CH   &   |- H e. CH   =>   |- (A e. H~ -> (G (_ (_|_` H) -> ((proj` (G +H H))` A) = (((proj` G)` A) +h ((proj` H)` A))))
Theorem	pj11 9630	One-to-one correspondence of projection and subspace.
|- G e. CH   &   |- H e. CH   =>   |- ((proj` G) = (proj` H) <-> G = H)
Theorem	pjds 9631	Vector decomposition into sum of projections on orthogonal subspaces.
|- G e. CH   &   |- H e. CH   =>   |- ((A e. (G vH H) /\ G (_ (_|_` H)) -> A = (((proj` G)` A) +h ((proj` H)` A)))
Theorem	pjds3 9632	Vector decomposition into sum of projections on orthogonal subspaces.
|- F e. CH   &   |- G e. CH   &   |- H e. CH   =>   |- (((A e. ((F vH G) vH H) /\ F (_ (_|_` G)) /\ (F (_ (_|_` H) /\ G (_ (_|_` H))) -> A = ((((proj` F)` A) +h ((proj` G)` A)) +h ((proj` H)` A)))
Theorem	pj11t 9633	One-to-one correspondence of projection and subspace.
|- ((G e. CH /\ H e. CH) -> ((proj` G) = (proj` H) <-> G = H))
Theorem	pjmfn 9634	Functionality of the projection function.
|- proj Fn CH
Theorem	pjmf1 9635	The projector function maps one-to-one into the set of Hilbert space operators.
|- proj:CH-1-1->(H~ ^m H~)
Theorem	pjoi0t 9636	The inner product of projections on orthogonal subspaces vanishes.
|- (((G e. CH /\ H e. CH /\ A e. H~) /\ G (_ (_|_` H)) -> (((proj` G)` A) .ih ((proj` H)` A)) = 0)
Theorem	pjoi0 9637	The inner product of projections on orthogonal subspaces vanishes.
|- G e. CH   &   |- H e. CH   &   |- A e. H~   =>   |- (G (_ (_|_` H) -> (((proj` G)` A) .ih ((proj` H)` A)) = 0)
Theorem	pjopyth 9638	Pythagorean theorem for projections on orthogonal subspaces.
|- G e. CH   &   |- H e. CH   &   |- A e. H~   =>   |- (G (_ (_|_` H) -> ((normh` (((proj` G)` A) +h ((proj` H)` A)))^2) = (((normh` ((proj` G)` A))^2) + ((normh` ((proj` H)` A))^2)))
Theorem	pjopytht 9639	Pythagorean theorem for projections on orthogonal subspaces.
|- ((H e. CH /\ G e. CH /\ A e. H~) -> (H (_ (_|_` G) -> ((normh` (((proj` H)` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` G)` A))^2))))
Theorem	pjnorm 9640	The norm of the projection is less than or equal to the norm.
|- H e. CH   &   |- A e. H~   =>   |- (normh` ((proj` H)` A)) <_ (normh` A)
Theorem	pjpyth 9641	Pythagorean theorem for projections.
|- H e. CH   &   |- A e. H~   =>   |- ((normh` A)^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` (_|_` H))` A))^2))
Theorem	pjnel 9642	If a vector does not belong to subspace, the norm of its projection is less than its norm.
|- H e. CH   &   |- A e. H~   =>   |- (-. A e. H <-> (normh` ((proj` H)` A)) < (normh` A))
Theorem	pjnormt 9643	The norm of the projection is less than or equal to the norm.
|- ((H e. CH /\ A e. H~) -> (normh` ((proj` H)` A)) <_