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

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

Type	Label	Description
Statement
Theorem	pjf 9601	The mapping of a projection.
|- H e. CH   =>   |- (proj` H):H~-->H~
Theorem	pjv 9602	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 9603	A projection maps onto its subspace.
|- (H e. CH -> (proj` H):H~-onto->H)
Theorem	pjrnt 9604	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44.
|- (H e. CH -> ran (proj` H) = H)
Theorem	pjft 9605	The mapping of a projection.
|- (H e. CH -> (proj` H):H~-->H~)
Theorem	pjfnt 9606	Functionality of a projection.
|- (H e. CH -> (proj` H) Fn H~)
Theorem	pjsumt 9607	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 9608	One-to-one correspondence of projection and subspace.
|- G e. CH   &   |- H e. CH   =>   |- ((proj` G) = (proj` H) <-> G = H)
Theorem	pjds 9609	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 9610	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 9611	One-to-one correspondence of projection and subspace.
|- ((G e. CH /\ H e. CH) -> ((proj` G) = (proj` H) <-> G = H))
Theorem	pjmfn 9612	Functionality of the projection function.
|- proj Fn CH
Theorem	pjmf1 9613	The projector function maps one-to-one into the set of Hilbert space operators.
|- proj:CH-1-1->(H~ ^m H~)
Theorem	pjoi0t 9614	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 9615	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 9616	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 9617	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 9618	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 9619	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 9620	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 9621	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 9622	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 9623	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 9624	A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjcht 9591 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 9625	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 9626	Define the Hilbert space zero operator. See df0op2 9630 for alternate definition.
|- 0hop = (proj` 0H)
Definition	df-iop 9627	Define the Hilbert space identity operator. See dfiop2 9631 for alternate definition.
|- Iop = (proj` H~)
Theorem	ho0valt 9628	Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111.
|- (A e. H~ -> (0hop` A) = 0h)
Theorem	ho0f 9629	Functionality of the zero Hilbert space operator.
|- 0hop:H~-->H~
Theorem	df0op2 9630	Alternate definition of Hilbert space zero operator.
|- 0hop = (H~ X. 0H)
Theorem	dfiop2 9631	Alternate definition of Hilbert space identity operator.
|- Iop = (I |` H~)
Theorem	hoif 9632	Functionality of the Hilbert space identity operator.
|- Iop :H~-1-1-onto->H~
Theorem	hoivalt 9633	The value of the Hilbert space identity operator.
|- (A e. H~ -> ( Iop ` A) = A)
Theorem	hoico1t 9634	Composition with the Hilbert space identity operator.
|- (T:H~-->H~ -> (T o. Iop ) = T)
Theorem	hoico2t 9635	Composition with the Hilbert space identity operator.
|- (T:H~-->H~ -> ( Iop o. T) = T)
Operations on Hilbert space operators
Theorem	hoaddclt 9636	The sum of Hilbert space operators is an operator.
|- ((S:H~-->H~ /\ T:H~-->H~) -> (S +op T):H~-->H~)
Theorem	homulclt 9637	The scalar product of a Hilbert space operator is an operator.
|- ((A e. CC /\ T:H~-->H~) -> (A .op T):H~-->H~)
Theorem	hoeqt 9638	Equality of Hilbert space operators.
|- ((T:H~-->H~ /\ U:H~-->H~) -> (A.x e. H~ (T` x) = (U` x) <-> T = U))
Theorem	hoeq 9639	Equality of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A.x e. H~ (S` x) = (T` x) <-> S = T)
Theorem	hoscl 9640	Closure of Hilbert space operator sum.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A e. H~ -> ((S +op T)` A) e. H~)
Theorem	hodcl 9641	Closure of Hilbert space operator difference.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A e. H~ -> ((S -op T)` A) e. H~)
Theorem	hoco 9642	Composition of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A e. H~ -> ((S o. T)` A) = (S` (T` A)))
Theorem	hococl 9643	Closure of composition of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A e. H~ -> ((S o. T)` A) e. H~)
Theorem	hocof 9644	Mapping of composition of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S o. T):H~-->H~
Theorem	hocofn 9645	Functionality of composition of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S o. T) Fn H~
Theorem	hoaddcl 9646	Mapping of sum of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +op T):H~-->H~
Theorem	hosubcl 9647	Mapping of difference of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S -op T):H~-->H~
Theorem	hoaddfn 9648	Functionality of sum of Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +op T) Fn H~
Theorem	hosubfn 9649	Functionality of difference of Hilbert space operators.
|-