mmtheorems96 - 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-10700 108 10701-10766

Statement List for Metamath Proof Explorer - 9501-9600 - Page 96 of 108

Type	Label	Description
Statement
Theorem	spansneleq 9501	Membership relation that implies equality of spans.
|- ((B e. H~ /\ A =/= 0h) -> (A e. (span` {B}) -> (span` {A}) = (span` {B})))
Theorem	spansnsst 9502	The span of the singleton of an element of a subspace is included in the subspace.
|- ((A e. SH /\ B e. A) -> (span` {B}) (_ A)
Theorem	elspansn3t 9503	A member of the span of the singleton of a vector is a member of a subspace containing the vector.
|- ((A e. SH /\ B e. A /\ C e. (span` {B})) -> C e. A)
Theorem	elspansn4t 9504	A span membership condition implying two vectors belong to the same subspace.
|- (((A e. SH /\ B e. H~) /\ (C e. (span` {B}) /\ C =/= 0h)) -> (B e. A <-> C e. A))
Theorem	elspansn5t 9505	A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero.
|- (A e. SH -> (((B e. H~ /\ -. B e. A) /\ (C e. (span` {B}) /\ C e. A)) -> C = 0h))
Theorem	spansnss2t 9506	The span of the singleton of an element of a subspace is included in the subspace.
|- ((A e. SH /\ B e. H~) -> (B e. A <-> (span` {B}) (_ A))
Theorem	normcant 9507	Cancellation-type law that "extracts" a vector A from its inner product with a proportional vector B.
|- ((B e. H~ /\ B =/= 0h /\ A e. (span` {B})) -> (((A .ih B) / ((normh` B)^2)) .h B) = A)
Theorem	pjspansnt 9508	A projection on the span of a singleton.
|- ((A e. H~ /\ B e. H~ /\ A =/= 0h) -> ((proj` (span` {A}))` B) = (((B .ih A) / ((normh` A)^2)) .h A))
Theorem	spansnpj 9509	A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement.
|- A (_ H~   &   |- B e. H~   =>   |- A (_ (_|_` (span` {((proj` (_|_` A))` B)}))
Theorem	spanunsn 9510	The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton.
|- A e. CH   &   |- B e. H~   =>   |- (span` (A u. {B})) = (span` (A u. {((proj` (_|_` A))` B)}))
Theorem	spanpr 9511	The span of a pair of vectors.
|- ((A e. H~ /\ B e. H~) -> (span` {(A +h B)}) (_ (span` {A, B}))
Theorem	h1datom 9512	A 1-dimensional subspace is an atom.
|- A e. CH   &   |- B e. H~   =>   |- (A (_ (_|_` (_|_` {B})) -> (A = (_|_` (_|_` {B})) \/ A = 0H))
Theorem	h1datomt 9513	A 1-dimensional subspace is an atom.
|- ((A e. CH /\ B e. H~) -> (A (_ (_|_` (_|_` {B})) -> (A = (_|_` (_|_` {B})) \/ A = 0H)))
Operator sum, difference, and scalar multiplication
Definition	df-hosum 9514	Define the sum of two Hilbert space operators. Definition of [Beran] p. 111. Note on operators. Unlike some authors, we use the term "operator" to mean any function from H~ to H~. This is the definition of operator in [Hughes] p. 14, the definition of operator in [AkhiezerGlazman] p. 30, and the definition of operator in [Goldberg] p. 10. For Reed and Simon, an operator is linear (definition of operator in [ReedSimon] p. 2). For Halmos, an operator is bounded and linear (definition of operator in [Halmos] p. 35). For Kalmbach and Beran, an operator is continuous and linear (definition of operator in [Kalmbach] p. 353; definition of operator in [Beran] p. 99). Note that "bounded and linear" and "continuous and linear" are equivalent by lncnbd 9975.
|- +op = {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) +h (g` x)))})}
Definition	df-homul 9515	Define the scalar product with a Hilbert space operator. Definition of [Beran] p. 111.
|- .op = {<.<.f, g>., h>. | ((f e. CC /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = (f .h (g` x)))})}
Definition	df-hodif 9516	Define the difference of two Hilbert space operators. Definition of [Beran] p. 111.
|- -op = {<.<.f, g>., h>. | ((f:H~-->H~ /\ g:H~-->H~) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) -h (g` x)))})}
Definition	df-hfsum 9517	Define the sum of two Hilbert space functionals. Definition of [Beran] p. 111. Note that unlike some authors, we define a functional as any function from H~ to CC, not just linear (or bounded linear) ones.
|- +fn = {<.<.f, g>., h>. | ((f:H~-->CC /\ g:H~-->CC) /\ h = {<.x, y>. | (x e. H~ /\ y = ((f` x) + (g` x)))})}
Definition	df-hfmul 9518	Define the scalar product with a Hilbert space functional. Definition of [Beran] p. 111.
|- .fn = {<.<.f, g>., h>. | ((f e. CC /\ g:H~-->CC) /\ h = {<.x, y>. | (x e. H~ /\ y = (f x. (g` x)))})}
Theorem	hosmvalt 9519	Value of the sum of two Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~) -> (S +op T) = {<.x, y>. | (x e. H~ /\ y = ((S` x) +h (T` x)))})
Theorem	hommvalt 9520	Value of the scalar product with a Hilbert space operator.
|- ((A e. CC /\ T:H~-->H~) -> (A .op T) = {<.x, y>. | (x e. H~ /\ y = (A .h (T` x)))})
Theorem	hodmvalt 9521	Value of the difference of two Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~) -> (S -op T) = {<.x, y>. | (x e. H~ /\ y = ((S` x) -h (T` x)))})
Theorem	hfsmvalt 9522	Value of the sum of two Hilbert space functionals.
|- ((S:H~-->CC /\ T:H~-->CC) -> (S +fn T) = {<.x, y>. | (x e. H~ /\ y = ((S` x) + (T` x)))})
Theorem	hfmmvalt 9523	Value of the scalar product with a Hilbert space functional.
|- ((A e. CC /\ T:H~-->CC) -> (A .fn T) = {<.x, y>. | (x e. H~ /\ y = (A x. (T` x)))})
Theorem	hosvalt 9524	Value of the sum of two Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ A e. H~) -> ((S +op T)` A) = ((S` A) +h (T` A)))
Theorem	hosvaltOLD 9525	Value of the sum of two Hilbert space operators.
|- (((S:H~-->H~ /\ T:H~-->H~) /\ A e. H~) -> ((S +op T)` A) = ((S` A) +h (T` A)))
Theorem	homvalt 9526	Value of the scalar product with a Hilbert space operator.
|- ((A e. CC /\ T:H~-->H~ /\ B e. H~) -> ((A .op T)` B) = (A .h (T` B)))
Theorem	hodvalt 9527	Value of the difference of two Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ A e. H~) -> ((S -op T)` A) = ((S` A) -h (T` A)))
Theorem	hodvaltOLD 9528	Value of the difference of two Hilbert space operators.
|- (((S:H~-->H~ /\ T:H~-->H~) /\ A e. H~) -> ((S -op T)` A) = ((S` A) -h (T` A)))
Theorem	hfsvalt 9529	Value of the sum of two Hilbert space functionals.
|- (((S:H~-->CC /\ T:H~-->CC) /\ A e. H~) -> ((S +fn T)` A) = ((S` A) + (T` A)))
Theorem	hfmvalt 9530	Value of the scalar product with a Hilbert space functional.
|- ((A e. CC /\ T:H~-->CC /\ B e. H~) -> ((A .fn T)` B) = (A x. (T` B)))
Theorem	hosclt 9531	Closure of the sum of two Hilbert space operators.
|- (((S:H~-->H~ /\ T:H~-->H~) /\ A e. H~) -> ((S +op T)` A) e. H~)
Theorem	homclt 9532	Closure of the scalar product of a Hilbert space operator.
|- ((A e. CC /\ T:H~-->H~ /\ B e. H~) -> ((A .op T)` B) e. H~)
Theorem	hodclt 9533	Closure of the difference of two Hilbert space operators.
|- (((S:H~-->H~ /\ T:H~-->H~) /\ A e. H~) -> ((S -op T)` A) e. H~)
Commutes relation for Hilbert lattice elements
Definition	df-cm 9534	Define the commutes relation (on the Hilbert lattice). Definition of commutes in [Kalmbach] p. 20, who uses the notation xCy for "x commutes with y." See cmbr 9541 for membership relation.
|- C_H = {<.x, y>. | ((x e. CH /\ y e. CH) /\ x = ((x i^i y) vH (x i^i (_|_` y))))}
Theorem	cmbrt 9535	Binary relation expressing A commutes with B. Definition of commutes in [Kalmbach] p. 20.
|- ((A e. CH /\ B e. CH) -> (A C_H B <-> A = ((A i^i B) vH (A i^i (_|_` B)))))
Theorem	pjoml2 9536	Variation of orthomodular law. Definition in [Kalmbach] p. 22.
|- A e. CH   &   |- B e. CH   =>   |- (A (_ B -> (A vH ((_|_` A) i^i B)) = B)
Theorem	pjoml3 9537	Variation of orthomodular law.
|- A e. CH   &   |- B e. CH   =>   |- (B (_ A -> (A i^i ((_|_` A) vH B)) = B)
Theorem	pjoml4 9538	Variation of orthomodular law.
|- A e. CH   &   |- B e. CH   =>   |- (A vH (B i^i ((_|_` A) vH (_|_` B)))) = (A