P. 286 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28501-28600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	osumi 28501	If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. Note that the (countable) Axiom of Choice is used for this proof via pjhth 28252, although "the hard part" of this proof, chscl 28500, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_ ( _|_ ` B ) -> ( A +H B ) = ( A vH B ) )
Theorem	osumcori 28502	Corollary of osumi 28501. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( ( A i^i B ) +H ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) )
Theorem	osumcor2i 28503	Corollary of osumi 28501, showing it holds under the weaker hypothesis that A and B commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   =>    |- ( A C_H B -> ( A +H B ) = ( A vH B ) )
Theorem	osum 28504	If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH /\ A C_ ( _|_ ` B ) ) -> ( A +H B ) = ( A vH B ) )
Theorem	spansnji 28505	The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. ~H   =>    |- ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) )
Theorem	spansnj 28506	The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. ~H ) -> ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) ) )
Theorem	spansnscl 28507	The subspace sum of a closed subspace and a one-dimensional subspace is closed. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. ~H ) -> ( A +H ( span ` { B } ) ) e. CH )
Theorem	sumspansn 28508	The sum of two vectors belong to the span of one of them iff the other vector also belongs. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) )
Theorem	spansnm0i 28509	The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( -. A e. ( span ` { B } ) -> ( ( span ` { A } ) i^i ( span ` { B } ) ) = 0H )
Theorem	nonbooli 28510	A Hilbert lattice with two or more dimensions fails the distributive law and therefore cannot be a Boolean algebra. This counterexample demonstrates a condition where ( ( H i^i F ) vH ( H i^i G ) ) = 0H but ( H i^i ( F vH G ) ) =/= 0H. The antecedent specifies that the vectors A and B are nonzero and non-colinear. The last three hypotheses assign one-dimensional subspaces to F, G, and H. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- F = ( span ` { A } )   &    |- G = ( span ` { B } )   &    |- H = ( span ` { ( A +h B ) } )   =>    |- ( -. ( A e. G \/ B e. F ) -> ( H i^i ( F vH G ) ) =/= ( ( H i^i F ) vH ( H i^i G ) ) )
Theorem	spansncvi 28511	Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. ~H   =>    |- ( ( A C. B /\ B C_ ( A vH ( span ` { C } ) ) ) -> B = ( A vH ( span ` { C } ) ) )
Theorem	spansncv 28512	Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
|- ( ( A e. CH /\ B e. CH /\ C e. ~H ) -> ( ( A C. B /\ B C_ ( A vH ( span ` { C } ) ) ) -> B = ( A vH ( span ` { C } ) ) ) )
19.5.9  Orthoarguesian laws 5OA and 3OA
Theorem	5oalem1 28513	Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- R e. SH   =>    |- ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> v e. ( B +H ( A i^i ( C +H R ) ) ) )
Theorem	5oalem2 28514	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- D e. SH   =>    |- ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) e. ( ( A +H C ) i^i ( B +H D ) ) )
Theorem	5oalem3 28515	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- D e. SH   &    |- F e. SH   &    |- G e. SH   =>    |- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) )
Theorem	5oalem4 28516	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- D e. SH   &    |- F e. SH   &    |- G e. SH   =>    |- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) ) )
Theorem	5oalem5 28517	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-May-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- D e. SH   &    |- F e. SH   &    |- G e. SH   &    |- R e. SH   &    |- S e. SH   =>    |- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( f e. F /\ g e. G ) /\ ( v e. R /\ u e. S ) ) ) /\ ( ( ( x +h y ) = ( v +h u ) /\ ( z +h w ) = ( v +h u ) ) /\ ( f +h g ) = ( v +h u ) ) ) -> ( x -h z ) e. ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) )
Theorem	5oalem6 28518	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- D e. SH   &    |- F e. SH   &    |- G e. SH   &    |- R e. SH   &    |- S e. SH   =>    |- ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
Theorem	5oalem7 28519	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
|- A e. SH   &    |- B e. SH   &    |- C e. SH   &    |- D e. SH   &    |- F e. SH   &    |- G e. SH   &    |- R e. SH   &    |- S e. SH   =>    |- ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) C_ ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) )
Theorem	5oai 28520	Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). (Contributed by NM, 5-May-2000.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- D e. CH   &    |- F e. CH   &    |- G e. CH   &    |- R e. CH   &    |- S e. CH   &    |- A C_ ( _|_ ` B )   &    |- C C_ ( _|_ ` D )   &    |- F C_ ( _|_ ` G )   &    |- R C_ ( _|_ ` S )   =>    |- ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( ( F vH G ) i^i ( R vH S ) ) ) C_ ( B vH ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) )
Theorem	3oalem1 28521*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- B e. CH   &    |- C e. CH   &    |- R e. CH   &    |- S e. CH   =>    |- ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) )
Theorem	3oalem2 28522*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- B e. CH   &    |- C e. CH   &    |- R e. CH   &    |- S e. CH   =>    |- ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )
Theorem	3oalem3 28523	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- B e. CH   &    |- C e. CH   &    |- R e. CH   &    |- S e. CH   =>    |- ( ( B +H R ) i^i ( C +H S ) ) C_ ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) )
Theorem	3oalem4 28524	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- R = ( ( _|_ ` B ) i^i ( B vH A ) )   =>    |- R C_ ( _|_ ` B )
Theorem	3oalem5 28525	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- R = ( ( _|_ ` B ) i^i ( B vH A ) )   &    |- S = ( ( _|_ ` C ) i^i ( C vH A ) )   =>    |- ( ( B +H R ) i^i ( C +H S ) ) = ( ( B vH R ) i^i ( C vH S ) )
Theorem	3oalem6 28526	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- R = ( ( _|_ ` B ) i^i ( B vH A ) )   &    |- S = ( ( _|_ ` C ) i^i ( C vH A ) )   =>    |- ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) C_ ( B vH ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )
Theorem	3oai 28527	3OA (weak) orthoarguesian law. Equation IV of [GodowskiGreechie] p. 249. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- R = ( ( _|_ ` B ) i^i ( B vH A ) )   &    |- S = ( ( _|_ ` C ) i^i ( C vH A ) )   =>    |- ( ( B vH R ) i^i ( C vH S ) ) C_ ( B vH ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )
19.5.10  Projectors (cont.)
Theorem	pjorthi 28528	Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   =>    |- ( H e. CH -> ( ( ( proj h ` H ) ` A ) .ih ( ( proj h ` ( _|_ ` H ) ) ` B ) ) = 0 )
Theorem	pjch1 28529	Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
|- ( A e. ~H -> ( ( proj h ` ~H ) ` A ) = A )
Theorem	pjo 28530	The orthogonal projection. Lemma 4.4(i) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( ( proj h ` ( _|_ ` H ) ) ` A ) = ( ( ( proj h ` ~H ) ` A ) -h ( ( proj h ` H ) ` A ) ) )
Theorem	pjcompi 28531	Component of a projection. (Contributed by NM, 31-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( proj h ` H ) ` ( A +h B ) ) = A )
Theorem	pjidmi 28532	A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   =>    |- ( ( proj h ` H ) ` ( ( proj h ` H ) ` A ) ) = ( ( proj h ` H ) ` A )
Theorem	pjadjii 28533	A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- B e. ~H   =>    |- ( ( ( proj h ` H ) ` A ) .ih B ) = ( A .ih ( ( proj h ` H ) ` B ) )
Theorem	pjaddii 28534	Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- B e. ~H   =>    |- ( ( proj h ` H ) ` ( A +h B ) ) = ( ( ( proj h ` H ) ` A ) +h ( ( proj h ` H ) ` B ) )
Theorem	pjinormii 28535	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   =>    |- ( ( ( proj h ` H ) ` A ) .ih A ) = ( ( normh ` ( ( proj h ` H ) ` A ) ) ^ 2 )
Theorem	pjmulii 28536	Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- C e. CC   =>    |- ( ( proj h ` H ) ` ( C .h A ) ) = ( C .h ( ( proj h ` H ) ` A ) )
Theorem	pjsubii 28537	Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- B e. ~H   =>    |- ( ( proj h ` H ) ` ( A -h B ) ) = ( ( ( proj h ` H ) ` A ) -h ( ( proj h ` H ) ` B ) )
Theorem	pjsslem 28538	Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- G e. CH   =>    |- ( ( ( proj h ` ( _|_ ` H ) ) ` A ) -h ( ( proj h ` ( _|_ ` G ) ) ` A ) ) = ( ( ( proj h ` G ) ` A ) -h ( ( proj h ` H ) ` A ) )
Theorem	pjss2i 28539	Subset relationship for projections. Theorem 4.5(i)->(ii) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- G e. CH   =>    |- ( H C_ G -> ( ( proj h ` H ) ` ( ( proj h ` G ) ` A ) ) = ( ( proj h ` H ) ` A ) )
Theorem	pjssmii 28540	Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- G e. CH   =>    |- ( H C_ G -> ( ( ( proj h ` G ) ` A ) -h ( ( proj h ` H ) ` A ) ) = ( ( proj h ` ( G i^i ( _|_ ` H ) ) ) ` A ) )
Theorem	pjssge0ii 28541	Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- G e. CH   =>    |- ( ( ( ( proj h ` G ) ` A ) -h ( ( proj h ` H ) ` A ) ) = ( ( proj h ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( proj h ` G ) ` A ) -h ( ( proj h ` H ) ` A ) ) .ih A ) )
Theorem	pjdifnormii 28542	Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- G e. CH   =>    |- ( 0 <_ ( ( ( ( proj h ` G ) ` A ) -h ( ( proj h ` H ) ` A ) ) .ih A ) <-> ( normh ` ( ( proj h ` H ) ` A ) ) <_ ( normh ` ( ( proj h ` G ) ` A ) ) )
Theorem	pjcji 28543	The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   &    |- G e. CH   =>    |- ( H C_ ( _|_ ` G ) -> ( ( proj h ` ( H vH G ) ) ` A ) = ( ( ( proj h ` H ) ` A ) +h ( ( proj h ` G ) ` A ) ) )
Theorem	pjadji 28544	A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( proj h ` H ) ` A ) .ih B ) = ( A .ih ( ( proj h ` H ) ` B ) ) )
Theorem	pjaddi 28545	Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( ( proj h ` H ) ` ( A +h B ) ) = ( ( ( proj h ` H ) ` A ) +h ( ( proj h ` H ) ` B ) ) )
Theorem	pjinormi 28546	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
|- H e. CH   =>    |- ( A e. ~H -> ( ( ( proj h ` H ) ` A ) .ih A ) = ( ( normh ` ( ( proj h ` H ) ` A ) ) ^ 2 ) )
Theorem	pjsubi 28547	Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( ( proj h ` H ) ` ( A -h B ) ) = ( ( ( proj h ` H ) ` A ) -h ( ( proj h ` H ) ` B ) ) )
Theorem	pjmuli 28548	Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( A e. CC /\ B e. ~H ) -> ( ( proj h ` H ) ` ( A .h B ) ) = ( A .h ( ( proj h ` H ) ` B ) ) )
Theorem	pjige0i 28549	The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
|- H e. CH   =>    |- ( A e. ~H -> 0 <_ ( ( ( proj h ` H ) ` A ) .ih A ) )
Theorem	pjige0 28550	The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> 0 <_ ( ( ( proj h ` H ) ` A ) .ih A ) )
Theorem	pjcjt2 28551	The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
|- ( ( H e. CH /\ G e. CH /\ A e. ~H ) -> ( H C_ ( _|_ ` G ) -> ( ( proj h ` ( H vH G ) ) ` A ) = ( ( ( proj h ` H ) ` A ) +h ( ( proj h ` G ) ` A ) ) ) )
Theorem	pj0i 28552	The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( proj h ` H ) ` 0h ) = 0h
Theorem	pjch 28553	Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( A e. H <-> ( ( proj h ` H ) ` A ) = A ) )
Theorem	pjid 28554	The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. H ) -> ( ( proj h ` H ) ` A ) = A )
Theorem	pjvec 28555*	The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
|- ( H e. CH -> H = { x e. ~H | ( ( proj h ` H ) ` x ) = x } )
Theorem	pjocvec 28556*	The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- ( H e. CH -> ( _|_ ` H ) = { x e. ~H | ( ( proj h ` H ) ` x ) = 0h } )
Theorem	pjocini 28557	Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   =>    |- ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( proj h ` G ) ` A ) e. ( _|_ ` ( G i^i H ) ) )
Theorem	pjini 28558	Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   =>    |- ( A e. ( G i^i H ) -> ( ( proj h ` G ) ` A ) e. ( G i^i H ) )
Theorem	pjjsi 28559*	A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004.) (New usage is discouraged.)
|- G e. CH   &    |- H e. SH   =>    |- ( A. x e. ( G vH H ) ( ( proj h ` ( _|_ ` G ) ) ` x ) e. H -> ( G vH H ) = ( G +H H ) )
Theorem	pjfni 28560	Functionality of a projection. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
|- H e. CH   =>    |- ( proj h ` H ) Fn ~H
Theorem	pjrni 28561	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- H e. CH   =>    |- ran ( proj h ` H ) = H
Theorem	pjfoi 28562	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- H e. CH   =>    |- ( proj h ` H ) : ~H -onto-> H
Theorem	pjfi 28563	The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
|- H e. CH   =>    |- ( proj h ` H ) : ~H --> ~H
Theorem	pjvi 28564	The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.)
|- H e. CH   =>    |- ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( proj h ` H ) ` ( A +h B ) ) = A )
Theorem	pjhfo 28565	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- ( H e. CH -> ( proj h ` H ) : ~H -onto-> H )
Theorem	pjrn 28566	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- ( H e. CH -> ran ( proj h ` H ) = H )
Theorem	pjhf 28567	The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- ( H e. CH -> ( proj h ` H ) : ~H --> ~H )
Theorem	pjfn 28568	Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( H e. CH -> ( proj h ` H ) Fn ~H )
Theorem	pjsumi 28569	The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   =>    |- ( A e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( proj h ` ( G +H H ) ) ` A ) = ( ( ( proj h ` G ) ` A ) +h ( ( proj h ` H ) ` A ) ) ) )
Theorem	pj11i 28570	One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   =>    |- ( ( proj h ` G ) = ( proj h ` H ) <-> G = H )
Theorem	pjdsi 28571	Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   =>    |- ( ( A e. ( G vH H ) /\ G C_ ( _|_ ` H ) ) -> A = ( ( ( proj h ` G ) ` A ) +h ( ( proj h ` H ) ` A ) ) )
Theorem	pjds3i 28572	Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
|- F e. CH   &    |- G e. CH   &    |- H e. CH   =>    |- ( ( ( A e. ( ( F vH G ) vH H ) /\ F C_ ( _|_ ` G ) ) /\ ( F C_ ( _|_ ` H ) /\ G C_ ( _|_ ` H ) ) ) -> A = ( ( ( ( proj h ` F ) ` A ) +h ( ( proj h ` G ) ` A ) ) +h ( ( proj h ` H ) ` A ) ) )
Theorem	pj11 28573	One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- ( ( G e. CH /\ H e. CH ) -> ( ( proj h ` G ) = ( proj h ` H ) <-> G = H ) )
Theorem	pjmfn 28574	Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- proj h Fn CH
Theorem	pjmf1 28575	The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
|- proj h : CH -1-1-> ( ~H ^m ~H )
Theorem	pjoi0 28576	The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
|- ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ G C_ ( _|_ ` H ) ) -> ( ( ( proj h ` G ) ` A ) .ih ( ( proj h ` H ) ` A ) ) = 0 )
Theorem	pjoi0i 28577	The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   &    |- A e. ~H   =>    |- ( G C_ ( _|_ ` H ) -> ( ( ( proj h ` G ) ` A ) .ih ( ( proj h ` H ) ` A ) ) = 0 )
Theorem	pjopythi 28578	Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
|- G e. CH   &    |- H e. CH   &    |- A e. ~H   =>    |- ( G C_ ( _|_ ` H ) -> ( ( normh ` ( ( ( proj h ` G ) ` A ) +h ( ( proj h ` H ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( proj h ` G ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( proj h ` H ) ` A ) ) ^ 2 ) ) )
Theorem	pjopyth 28579	Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
|- ( ( H e. CH /\ G e. CH /\ A e. ~H ) -> ( H C_ ( _|_ ` G ) -> ( ( normh ` ( ( ( proj h ` H ) ` A ) +h ( ( proj h ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( proj h ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( proj h ` G ) ` A ) ) ^ 2 ) ) ) )
Theorem	pjnormi 28580	The norm of the projection is less than or equal to the norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   =>    |- ( normh ` ( ( proj h ` H ) ` A ) ) <_ ( normh ` A )
Theorem	pjpythi 28581	Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   =>    |- ( ( normh ` A ) ^ 2 ) = ( ( ( normh ` ( ( proj h ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( proj h ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) )
Theorem	pjneli 28582	If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.)
|- H e. CH   &    |- A e. ~H   =>    |- ( -. A e. H <-> ( normh ` ( ( proj h ` H ) ` A ) ) < ( normh ` A ) )
Theorem	pjnorm 28583	The norm of the projection is less than or equal to the norm. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( normh ` ( ( proj h ` H ) ` A ) ) <_ ( normh ` A ) )
Theorem	pjpyth 28584	Pythagorean theorem for projectors. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( ( normh ` A ) ^ 2 ) = ( ( ( normh ` ( ( proj h ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( proj h ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) ) )
Theorem	pjnel 28585	If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( -. A e. H <-> ( normh ` ( ( proj h ` H ) ` A ) ) < ( normh ` A ) ) )
Theorem	pjnorm2 28586	A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 28553 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( A e. H <-> ( normh ` ( ( proj h ` H ) ` A ) ) = ( normh ` A ) ) )
19.5.11  Mayet's equation E_3
Theorem	mayete3i 28587	Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 1223. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- D e. CH   &    |- F e. CH   &    |- G e. CH   &    |- A C_ ( _|_ ` C )   &    |- A C_ ( _|_ ` F )   &    |- C C_ ( _|_ ` F )   &    |- A C_ ( _|_ ` B )   &    |- C C_ ( _|_ ` D )   &    |- F C_ ( _|_ ` G )   &    |- X = ( ( A vH C ) vH F )   &    |- Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )   &    |- Z = ( ( B vH D ) vH G )   =>    |- ( X i^i Y ) C_ Z
Theorem	mayetes3i 28588	Mayet's equation E^*3, derived from E3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. (Contributed by NM, 10-May-2009.) (New usage is discouraged.)
|- A e. CH   &    |- B e. CH   &    |- C e. CH   &    |- D e. CH   &    |- F e. CH   &    |- G e. CH   &    |- R e. CH   &    |- A C_ ( _|_ ` C )   &    |- A C_ ( _|_ ` F )   &    |- C C_ ( _|_ ` F )   &    |- A C_ ( _|_ ` B )   &    |- C C_ ( _|_ ` D )   &    |- F C_ ( _|_ ` G )   &    |- R C_ ( _|_ ` X )   &    |- X = ( ( A vH C ) vH F )   &    |- Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )   &    |- Z = ( ( B vH D ) vH G )   =>    |- ( ( X vH R ) i^i Y ) C_ ( Z vH R )
19.6  Operators on Hilbert spaces
19.6.1  Operator sum, difference, and scalar multiplication 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 28897.
Definition	df-hosum 28589*	Define the sum of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.)
|- +op = ( f e. ( ~H ^m ~H ) , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) +h ( g ` x ) ) ) )
Definition	df-homul 28590*	Define the scalar product with a Hilbert space operator. Definition of [Beran] p. 111. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- .op = ( f e. CC , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( f .h ( g ` x ) ) ) )
Definition	df-hodif 28591*	Define the difference of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.)
|- -op = ( f e. ( ~H ^m ~H ) , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) -h ( g ` x ) ) ) )
Definition	df-hfsum 28592*	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. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|- +fn = ( f e. ( CC ^m ~H ) , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) + ( g ` x ) ) ) )
Definition	df-hfmul 28593*	Define the scalar product with a Hilbert space functional. Definition of [Beran] p. 111. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|- .fn = ( f e. CC , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( f x. ( g ` x ) ) ) )
Theorem	hosmval 28594*	Value of the sum of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( x e. ~H |-> ( ( S ` x ) +h ( T ` x ) ) ) )
Theorem	hommval 28595*	Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) = ( x e. ~H |-> ( A .h ( T ` x ) ) ) )
Theorem	hodmval 28596*	Value of the difference of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )
Theorem	hfsmval 28597*	Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( ( S : ~H --> CC /\ T : ~H --> CC ) -> ( S +fn T ) = ( x e. ~H |-> ( ( S ` x ) + ( T ` x ) ) ) )
Theorem	hfmmval 28598*	Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> CC ) -> ( A .fn T ) = ( x e. ~H |-> ( A x. ( T ` x ) ) ) )
Theorem	hosval 28599	Value of the sum of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S +op T ) ` A ) = ( ( S ` A ) +h ( T ` A ) ) )
Theorem	homval 28600	Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( ( A .op T ) ` B ) = ( A .h ( T ` B ) ) )