![]() |
Metamath
Proof Explorer Theorem List (p. 412 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hdmapglem7a 41101* | Lemma for hdmapg 41104. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’)) | ||
Theorem | hdmapglem7b 41102 | Lemma for hdmapg 41104. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ β = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β π₯ β (πβ{πΈ})) & β’ (π β π¦ β (πβ{πΈ})) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβ((π Β· πΈ) + π₯))β((π Β· πΈ) + π¦)) = ((π Γ (πΊβπ)) β ((πβπ₯)βπ¦))) | ||
Theorem | hdmapglem7 41103 | Lemma for hdmapg 41104. Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). In the proof, our πΈ, (πβ{πΈ}), π, π, π, π’, π, and π£ correspond respectively to Baer's w, H, x, y, x', x'', y', and y'', and our ((πβπ)βπ) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ β = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β π β π) β β’ (π β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) | ||
Theorem | hdmapg 41104 | Apply the scalar sigma function (involution) πΊ to an inner product reverses the arguments. The inner product of π and π is represented by ((πβπ)βπ). Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) | ||
Theorem | hdmapoc 41105* | Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in [Holland95] p. 14. (Contributed by NM, 17-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = {π¦ β π β£ βπ§ β π ((πβπ§)βπ¦) = 0 }) | ||
Syntax | chlh 41106 | Extend class notation with the final constructed Hilbert space. |
class HLHil | ||
Definition | df-hlhil 41107* | Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ HLHil = (π β V β¦ (π€ β (LHypβπ) β¦ β¦((DVecHβπ)βπ€) / π’β¦β¦(Baseβπ’) / π£β¦({β¨(Baseβndx), π£β©, β¨(+gβndx), (+gβπ’)β©, β¨(Scalarβndx), (((EDRingβπ)βπ€) sSet β¨(*πβndx), ((HGMapβπ)βπ€)β©)β©} βͺ {β¨( Β·π βndx), ( Β·π βπ’)β©, β¨(Β·πβndx), (π₯ β π£, π¦ β π£ β¦ ((((HDMapβπ)βπ€)βπ¦)βπ₯))β©}))) | ||
Theorem | hlhilset 41108* | The final Hilbert space constructed from a Hilbert lattice πΎ and an arbitrary hyperplane π in πΎ. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((HLHilβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ π = (πΈ sSet β¨(*πβndx), πΊβ©) & β’ Β· = ( Β·π βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ , = (π₯ β π, π¦ β π β¦ ((πβπ¦)βπ₯)) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΏ = ({β¨(Baseβndx), πβ©, β¨(+gβndx), + β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©})) | ||
Theorem | hlhilsca 41109 | The scalar of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ π = (πΈ sSet β¨(*πβndx), πΊβ©) β β’ (π β π = (Scalarβπ)) | ||
Theorem | hlhilbase 41110 | The base set of the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) β β’ (π β π = (Baseβπ)) | ||
Theorem | hlhilplus 41111 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ + = (+gβπΏ) β β’ (π β + = (+gβπ)) | ||
Theorem | hlhilslem 41112 | Lemma for hlhilsbase 41114 etc. (Contributed by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot (πΉβndx) & β’ (πΉβndx) β (*πβndx) & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilslemOLD 41113 | Obsolete version of hlhilslem 41112 as of 6-Nov-2024. Lemma for hlhilsbase 41114. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot π & β’ π β β & β’ π < 4 & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilsbase 41114 | The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΆ = (BaseβπΈ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsbaseOLD 41115 | Obsolete version of hlhilsbase 41114 as of 6-Nov-2024. The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΆ = (BaseβπΈ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsplus 41116 | Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ + = (+gβπΈ) β β’ (π β + = (+gβπ )) | ||
Theorem | hlhilsplusOLD 41117 | Obsolete version of hlhilsplus 41116 as of 6-Nov-2024. The scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ + = (+gβπΈ) β β’ (π β + = (+gβπ )) | ||
Theorem | hlhilsmul 41118 | Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ Β· = (.rβπΈ) β β’ (π β Β· = (.rβπ )) | ||
Theorem | hlhilsmulOLD 41119 | Obsolete version of hlhilsmul 41118 as of 6-Nov-2024. The scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ Β· = (.rβπΈ) β β’ (π β Β· = (.rβπ )) | ||
Theorem | hlhilsbase2 41120 | The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΆ = (Baseβπ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsplus2 41121 | Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ + = (+gβπ) β β’ (π β + = (+gβπ )) | ||
Theorem | hlhilsmul2 41122 | Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ Β· = (.rβπ) β β’ (π β Β· = (.rβπ )) | ||
Theorem | hlhils0 41123 | The scalar ring zero for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ 0 = (0gβπ) β β’ (π β 0 = (0gβπ )) | ||
Theorem | hlhils1N 41124 | The scalar ring unity for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ 1 = (1rβπ) β β’ (π β 1 = (1rβπ )) | ||
Theorem | hlhilvsca 41125 | The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β Β· = ( Β·π βπ)) | ||
Theorem | hlhilip 41126* | Inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) & β’ π = ((HDMapβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ , = (π₯ β π, π¦ β π β¦ ((πβπ¦)βπ₯)) β β’ (π β , = (Β·πβπ)) | ||
Theorem | hlhilipval 41127 | Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) & β’ π = ((HDMapβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ , = (Β·πβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π , π) = ((πβπ)βπ)) | ||
Theorem | hlhilnvl 41128 | The involution operation of the star division ring for the final constructed Hilbert space. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ β = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β β = (*πβπ )) | ||
Theorem | hlhillvec 41129 | The final constructed Hilbert space is a vector space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π β LVec) | ||
Theorem | hlhildrng 41130 | The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ π = (Scalarβπ) β β’ (π β π β DivRing) | ||
Theorem | hlhilsrnglem 41131 | Lemma for hlhilsrng 41132. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ π = (Scalarβπ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ πΊ = ((HGMapβπΎ)βπ) β β’ (π β π β *-Ring) | ||
Theorem | hlhilsrng 41132 | The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 21-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ π = (Scalarβπ) β β’ (π β π β *-Ring) | ||
Theorem | hlhil0 41133 | The zero vector for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ 0 = (0gβπΏ) β β’ (π β 0 = (0gβπ)) | ||
Theorem | hlhillsm 41134 | The vector sum operation for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ β = (LSSumβπΏ) β β’ (π β β = (LSSumβπ)) | ||
Theorem | hlhilocv 41135 | The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ π = (BaseβπΏ) & β’ π = ((ocHβπΎ)βπ) & β’ π = (ocvβπ) & β’ (π β π β π) β β’ (π β (πβπ) = (πβπ)) | ||
Theorem | hlhillcs 41136 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 41110 is applied over and over to conclusion rather than applied once to antecedent - would compressed proof be shorter if applied once to antecedent? (Contributed by NM, 23-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ πΆ = (ClSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΆ = ran πΌ) | ||
Theorem | hlhilphllem 41137* | Lemma for hlhil 25191. (Contributed by NM, 23-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = (Scalarβπ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) & β’ + = (+gβπΏ) & β’ Β· = ( Β·π βπΏ) & β’ π = (ScalarβπΏ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ Γ = (.rβπ ) & β’ π = (0gβπ ) & β’ 0 = (0gβπΏ) & β’ , = (Β·πβπ) & β’ π½ = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ πΈ = (π₯ β π, π¦ β π β¦ ((π½βπ¦)βπ₯)) β β’ (π β π β PreHil) | ||
Theorem | hlhilhillem 41138* | Lemma for hlhil 25191. (Contributed by NM, 23-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = (Scalarβπ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) & β’ + = (+gβπΏ) & β’ Β· = ( Β·π βπΏ) & β’ π = (ScalarβπΏ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ Γ = (.rβπ ) & β’ π = (0gβπ ) & β’ 0 = (0gβπΏ) & β’ , = (Β·πβπ) & β’ π½ = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ πΈ = (π₯ β π, π¦ β π β¦ ((π½βπ¦)βπ₯)) & β’ π = (ocvβπ) & β’ πΆ = (ClSubSpβπ) β β’ (π β π β Hil) | ||
Theorem | hlathil 41139 |
Construction of a Hilbert space (df-hil 21478) π from a Hilbert
lattice (df-hlat 38524) πΎ, where π is a fixed but arbitrary
hyperplane (co-atom) in πΎ.
The Hilbert space π is identical to the vector space ((DVecHβπΎ)βπ) (see dvhlvec 40283) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in [Holland95] p. 13, whose proof we follow loosely. An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria SolΓ¨r in 1995 and refined by RenΓ© Mayet in 1998 that result in a division ring isomorphic to β. See additional discussion at https://us.metamath.org/qlegif/mmql.html#what 40283. π corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a π always exists since HL has lattice rank of at least 4 by df-hil 21478. It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π β Hil) | ||
Syntax | ccsrg 41140 | Extend class notation with the class of all commutative semirings. |
class CSRing | ||
Definition | df-csring 41141 | Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.) |
β’ CSRing = {π β SRing β£ (mulGrpβπ) β CMnd} | ||
Theorem | iscsrg 41142 | A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.) |
β’ πΊ = (mulGrpβπ ) β β’ (π β CSRing β (π β SRing β§ πΊ β CMnd)) | ||
Theorem | leexp1ad 41143 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β0) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ π΅) β β’ (π β (π΄βπ) β€ (π΅βπ)) | ||
Theorem | relogbcld 41144 | Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β) & β’ (π β 0 < π΅) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π΅ β 1) β β’ (π β (π΅ logb π) β β) | ||
Theorem | relogbexpd 41145 | Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β+) & β’ (π β π΅ β 1) & β’ (π β π β β€) β β’ (π β (π΅ logb (π΅βπ)) = π) | ||
Theorem | relogbzexpd 41146 | Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β+) & β’ (π β π΅ β 1) & β’ (π β πΆ β β+) & β’ (π β π β β€) β β’ (π β (π΅ logb (πΆβπ)) = (π Β· (π΅ logb πΆ))) | ||
Theorem | logblebd 41147 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β€) & β’ (π β 2 β€ π΅) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β€ π) β β’ (π β (π΅ logb π) β€ (π΅ logb π)) | ||
Theorem | uzindd 41148* | Induction on the upper integers that start at π. The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024.) |
β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = (π + 1) β (π β π)) & β’ (π = π β (π β π)) & β’ (π β π) & β’ ((π β§ π β§ (π β β€ β§ π β€ π)) β π) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β€ π) β β’ (π β π) | ||
Theorem | fzadd2d 41149 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π½ β (π...π)) & β’ (π β πΎ β (π...π)) & β’ (π β π = (π + π)) & β’ (π β π = (π + π)) β β’ (π β (π½ + πΎ) β (π...π )) | ||
Theorem | zltlem1d 41150 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β π β€ (π β 1))) | ||
Theorem | zltp1led 41151 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β (π + 1) β€ π)) | ||
Theorem | fzne2d 41152 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
β’ (π β πΎ β (π...π)) & β’ (π β πΎ β π) β β’ (π β πΎ < π) | ||
Theorem | eqfnfv2d2 41153* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΅) & β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = (πΊβπ₯)) β β’ (π β πΉ = πΊ) | ||
Theorem | fzsplitnd 41154 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΎ β (π...π)) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | fzsplitnr 41155 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β π β€ πΎ) & β’ (π β πΎ β€ π) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | addassnni 41156 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ)) | ||
Theorem | addcomnni 41157 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) = (π΅ + π΄) | ||
Theorem | mulassnni 41158 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ)) | ||
Theorem | mulcomnni 41159 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) = (π΅ Β· π΄) | ||
Theorem | gcdcomnni 41160 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) = (π gcd π) | ||
Theorem | gcdnegnni 41161 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd -π) = (π gcd π) | ||
Theorem | neggcdnni 41162 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (-π gcd π) = (π gcd π) | ||
Theorem | bccl2d 41163 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β πΎ β β0) & β’ (π β πΎ β€ π) β β’ (π β (πCπΎ) β β) | ||
Theorem | recbothd 41164 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π· β β) & β’ (π β π· β 0) β β’ (π β ((π΄ / π΅) = (πΆ / π·) β (π΅ / π΄) = (π· / πΆ))) | ||
Theorem | gcdmultiplei 41165 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd (π Β· π)) = π | ||
Theorem | gcdaddmzz2nni 41166 | Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β & β’ πΎ β β€ β β’ (π gcd π) = (π gcd (π + (πΎ Β· π))) | ||
Theorem | gcdaddmzz2nncomi 41167 | Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β & β’ πΎ β β€ β β’ (π gcd π) = (π gcd ((πΎ Β· π) + π)) | ||
Theorem | gcdnncli 41168 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) β β | ||
Theorem | muldvds1d 41169 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β πΎ β₯ π) | ||
Theorem | muldvds2d 41170 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β π β₯ π) | ||
Theorem | nndivdvdsd 41171 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16210. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) β β’ (π β (π β₯ π β (π / π) β β)) | ||
Theorem | nnproddivdvdsd 41172 | A product of natural numbers divides a natural number if and only if a factor divides the quotient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β) & β’ (π β π β β) & β’ (π β π β β) β β’ (π β ((πΎ Β· π) β₯ π β πΎ β₯ (π / π))) | ||
Theorem | coprmdvds2d 41173 | If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ gcd π) = 1) & β’ (π β πΎ β₯ π) & β’ (π β π β₯ π) β β’ (π β (πΎ Β· π) β₯ π) | ||
Theorem | 12gcd5e1 41174 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 gcd 5) = 1 | ||
Theorem | 60gcd6e6 41175 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 6) = 6 | ||
Theorem | 60gcd7e1 41176 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 7) = 1 | ||
Theorem | 420gcd8e4 41177 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 gcd 8) = 4 | ||
Theorem | lcmeprodgcdi 41178 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β & β’ πΊ β β & β’ π» β β & β’ (π gcd π) = πΊ & β’ (πΊ Β· π») = π΄ & β’ (π Β· π) = π΄ β β’ (π lcm π) = π» | ||
Theorem | 12lcm5e60 41179 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 lcm 5) = ;60 | ||
Theorem | 60lcm6e60 41180 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 6) = ;60 | ||
Theorem | 60lcm7e420 41181 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 7) = ;;420 | ||
Theorem | 420lcm8e840 41182 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 lcm 8) = ;;840 | ||
Theorem | lcmfunnnd 41183 | Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024.) |
β’ (π β π β β) β β’ (π β (lcmβ(1...π)) = ((lcmβ(1...(π β 1))) lcm π)) | ||
Theorem | lcm1un 41184 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...1)) = 1 | ||
Theorem | lcm2un 41185 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...2)) = 2 | ||
Theorem | lcm3un 41186 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...3)) = 6 | ||
Theorem | lcm4un 41187 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...4)) = ;12 | ||
Theorem | lcm5un 41188 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...5)) = ;60 | ||
Theorem | lcm6un 41189 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...6)) = ;60 | ||
Theorem | lcm7un 41190 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...7)) = ;;420 | ||
Theorem | lcm8un 41191 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...8)) = ;;840 | ||
Theorem | 3factsumint1 41192* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ π΄ = (πΏ[,]π) & β’ (π β π΅ β Fin) & β’ (π β πΏ β β) & β’ (π β π β β) & β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ (π β (π₯ β π΄ β¦ πΉ) β (π΄βcnββ)) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ π») β (π΄βcnββ)) β β’ (π β β«π΄Ξ£π β π΅ (πΉ Β· (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ β«π΄(πΉ Β· (πΊ Β· π»)) dπ₯) | ||
Theorem | 3factsumint2 41193* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β Ξ£π β π΅ β«π΄(πΉ Β· (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ β«π΄(πΊ Β· (πΉ Β· π»)) dπ₯) | ||
Theorem | 3factsumint3 41194* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ π΄ = (πΏ[,]π) & β’ (π β πΏ β β) & β’ (π β π β β) & β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ (π β (π₯ β π΄ β¦ πΉ) β (π΄βcnββ)) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ π») β (π΄βcnββ)) β β’ (π β Ξ£π β π΅ β«π΄(πΊ Β· (πΉ Β· π»)) dπ₯ = Ξ£π β π΅ (πΊ Β· β«π΄(πΉ Β· π») dπ₯)) | ||
Theorem | 3factsumint4 41195* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β β«π΄Ξ£π β π΅ (πΉ Β· (πΊ Β· π»)) dπ₯ = β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯) | ||
Theorem | 3factsumint 41196* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
β’ π΄ = (πΏ[,]π) & β’ (π β π΅ β Fin) & β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ πΉ) β (π΄βcnββ)) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ π») β (π΄βcnββ)) β β’ (π β β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ (πΊ Β· β«π΄(πΉ Β· π») dπ₯)) | ||
Theorem | resopunitintvd 41197 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0(,)1) β¦ π΄) β ((0(,)1)βcnββ)) | ||
Theorem | resclunitintvd 41198 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0[,]1) β¦ π΄) β ((0[,]1)βcnββ)) | ||
Theorem | resdvopclptsd 41199* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) & β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β β) β β’ (π β (β D (π₯ β (0[,]1) β¦ π΄)) = (π₯ β (0(,)1) β¦ π΅)) | ||
Theorem | lcmineqlem1 41200* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.) |
β’ πΉ = β«(0[,]1)((π₯β(π β 1)) Β· ((1 β π₯)β(π β π))) dπ₯ & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β πΉ = β«(0[,]1)((π₯β(π β 1)) Β· Ξ£π β (0...(π β π))(((-1βπ) Β· ((π β π)Cπ)) Β· (π₯βπ))) dπ₯) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |