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-10697

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

Type	Label	Description
Statement
Theorem	pjige0 9601	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 9602	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 9603	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 9604	The projection of the zero vector.
|- H e. CH   =>   |- ((proj` H)` 0h) = 0h
Theorem	pjcht 9605	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 9606	The projection of a vector in the projection subspace is itself.
|- ((H e. CH /\ A e. H) -> ((proj` H)` A) = A)
Theorem	pjvect 9607	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 9608	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 9609	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 9610	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 9611	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 9612	Functionality of a projection.
|- H e. CH   =>   |- (proj` H) Fn H~
Theorem	pjrn 9613	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44.
|- H e. CH   =>   |- ran (proj` H) = H
Theorem	pjfo 9614	A projection maps onto its subspace.
|- H e. CH   =>   |- (proj` H):H~-onto->H
Theorem	pjf 9615	The mapping of a projection.
|- H e. CH   =>   |- (proj` H):H~-->H~
Theorem	pjv 9616	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 9617	A projection maps onto its subspace.
|- (H e. CH -> (proj` H):H~-onto->H)
Theorem	pjrnt 9618	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44.
|- (H e. CH -> ran (proj` H) = H)
Theorem	pjft 9619	The mapping of a projection.
|- (H e. CH -> (proj` H):H~-->H~)
Theorem	pjfnt 9620	Functionality of a projection.
|- (H e. CH -> (proj` H) Fn H~)
Theorem	pjsumt 9621	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 9622	One-to-one correspondence of projection and subspace.
|- G e. CH   &   |- H e. CH   =>   |- ((proj` G) = (proj` H) <-> G = H)
Theorem	pjds 9623	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 9624	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 9625	One-to-one correspondence of projection and subspace.
|- ((G e. CH /\ H e. CH) -> ((proj` G) = (proj` H) <-> G = H))
Theorem	pjmfn 9626	Functionality of the projection function.
|- proj Fn CH
Theorem	pjmf1 9627	The projector function maps one-to-one into the set of Hilbert space operators.
|- proj:CH-1-1->(H~ ^m H~)
Theorem	pjoi0t 9628	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 9629	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 9630	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 9631	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 9632	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 9633	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 9634	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 9635	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	pjpytht 9636	Pythagorean theorem for projectors.
|- ((H e. CH /\ A e. H~) -> ((normh` A)^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` (_|_` H))` A))^2)))
Theorem	pjnelt 9637	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	pjnorm2t 9638	A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjcht 9605 yield Theorem 26.3 of [Halmos] p. 44.
|- ((H e. CH /\ A e. H~) -> (A e. H <-> (normh` ((proj` H)` A)) = (normh` A)))
Mayet's equation E_3
Theorem	mayete3 9639	Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 7.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   &   |- F e. CH   &   |- G e. CH   &   |- A (_ (_|_` B)   &   |- A (_ (_|_` C)   &   |- B (_ (_|_` C)   &   |- A (_ (_|_` D)   &   |- B (_ (_|_` F)   &   |- C (_ (_|_` G)   &   |- R = ((A vH B) vH C)   &   |- S = (((A vH D) i^i (B vH F)) i^i (C vH G))   &   |- T = ((D vH F) vH G)   =>   |- (R i^i S) (_ T
Zero and identity operators
Definition	df-h0op 9640	Define the Hilbert space zero operator. See df0op2 9644 for alternate definition.
|- 0hop = (proj` 0H)
Definition	df-iop 9641	Define the Hilbert space identity operator. See dfiop2 9645 for alternate definition.
|- Iop = (proj` H~)
Theorem	ho0valt 9642	Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111.
|- (A e. H~ -> (0hop` A) = 0h)
Theorem	ho0f 9643	Functionality of the zero Hilbert space operator.
|- 0hop:H~-->H~
Theorem	df0op2 9644	Alternate definition of Hilbert space zero operator.
|- 0hop = (H~ X. 0H)
Theorem	dfiop2 9645	Alternate definition of Hilbert space identity operator.
|- Iop = (I |` H~)
Theorem	hoif 9646	Functionality of the Hilbert space identity operator.
|- Iop :H~-1-1-onto->H~
Theorem	hoivalt 9647	The value of the Hilbert space identity operator.
|- (A e. H~ -> ( Iop ` A) = A)
Theorem	hoico1t 9648	Composition with the Hilbert space identity operator.
|- (T:H~-->H~ -> (T o. Iop ) = T)
Theorem	hoico2t 9649	Composition with the Hilbert space identity operator.
|- (T:H~-->