![]() |
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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hgmapvv 41101 | Value of a double involution. Part 1.2 of [Baer] p. 110 line 37. (Contributed by NM, 13-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΊβ(πΊβπ)) = π) | ||
Theorem | hdmapglem7a 41102* | Lemma for hdmapg 41105. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’)) | ||
Theorem | hdmapglem7b 41103 | Lemma for hdmapg 41105. (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 41104 | Lemma for hdmapg 41105. 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 41105 | 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 41106* | 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 41107 | Extend class notation with the final constructed Hilbert space. |
class HLHil | ||
Definition | df-hlhil 41108* | 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 41109* | 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 41110 | 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 41111 | 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 41112 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ + = (+gβπΏ) β β’ (π β + = (+gβπ)) | ||
Theorem | hlhilslem 41113 | Lemma for hlhilsbase 41115 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 41114 | Obsolete version of hlhilslem 41113 as of 6-Nov-2024. Lemma for hlhilsbase 41115. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot π & β’ π β β & β’ π < 4 & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilsbase 41115 | 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 41116 | Obsolete version of hlhilsbase 41115 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 41117 | 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 41118 | Obsolete version of hlhilsplus 41117 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 41119 | 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 41120 | Obsolete version of hlhilsmul 41119 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 41121 | 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 41122 | 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 41123 | 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 41124 | 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 41125 | 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 41126 | 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 41127* | 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 41128 | 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 41129 | 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 41130 | 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 41131 | 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 41132 | Lemma for hlhilsrng 41133. (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 41133 | 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 41134 | 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 41135 | 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 41136 | 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 41137 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 41111 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 41138* | Lemma for hlhil 25192. (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 41139* | Lemma for hlhil 25192. (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 41140 |
Construction of a Hilbert space (df-hil 21479) π from a Hilbert
lattice (df-hlat 38525) πΎ, where π is a fixed but arbitrary
hyperplane (co-atom) in πΎ.
The Hilbert space π is identical to the vector space ((DVecHβπΎ)βπ) (see dvhlvec 40284) 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 40284. π 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 21479. 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 41141 | Extend class notation with the class of all commutative semirings. |
class CSRing | ||
Definition | df-csring 41142 | Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.) |
β’ CSRing = {π β SRing β£ (mulGrpβπ) β CMnd} | ||
Theorem | iscsrg 41143 | A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.) |
β’ πΊ = (mulGrpβπ ) β β’ (π β CSRing β (π β SRing β§ πΊ β CMnd)) | ||
Theorem | leexp1ad 41144 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β0) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ π΅) β β’ (π β (π΄βπ) β€ (π΅βπ)) | ||
Theorem | relogbcld 41145 | 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 41146 | 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 41147 | 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 41148 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β€) & β’ (π β 2 β€ π΅) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β€ π) β β’ (π β (π΅ logb π) β€ (π΅ logb π)) | ||
Theorem | uzindd 41149* | 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 41150 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π½ β (π...π)) & β’ (π β πΎ β (π...π)) & β’ (π β π = (π + π)) & β’ (π β π = (π + π)) β β’ (π β (π½ + πΎ) β (π...π )) | ||
Theorem | zltlem1d 41151 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β π β€ (π β 1))) | ||
Theorem | zltp1led 41152 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β (π + 1) β€ π)) | ||
Theorem | fzne2d 41153 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
β’ (π β πΎ β (π...π)) & β’ (π β πΎ β π) β β’ (π β πΎ < π) | ||
Theorem | eqfnfv2d2 41154* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΅) & β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = (πΊβπ₯)) β β’ (π β πΉ = πΊ) | ||
Theorem | fzsplitnd 41155 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΎ β (π...π)) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | fzsplitnr 41156 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β π β€ πΎ) & β’ (π β πΎ β€ π) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | addassnni 41157 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ)) | ||
Theorem | addcomnni 41158 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) = (π΅ + π΄) | ||
Theorem | mulassnni 41159 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ)) | ||
Theorem | mulcomnni 41160 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) = (π΅ Β· π΄) | ||
Theorem | gcdcomnni 41161 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) = (π gcd π) | ||
Theorem | gcdnegnni 41162 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd -π) = (π gcd π) | ||
Theorem | neggcdnni 41163 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (-π gcd π) = (π gcd π) | ||
Theorem | bccl2d 41164 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β πΎ β β0) & β’ (π β πΎ β€ π) β β’ (π β (πCπΎ) β β) | ||
Theorem | recbothd 41165 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π· β β) & β’ (π β π· β 0) β β’ (π β ((π΄ / π΅) = (πΆ / π·) β (π΅ / π΄) = (π· / πΆ))) | ||
Theorem | gcdmultiplei 41166 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd (π Β· π)) = π | ||
Theorem | gcdaddmzz2nni 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 | gcdaddmzz2nncomi 41168 | 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 41169 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) β β | ||
Theorem | muldvds1d 41170 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β πΎ β₯ π) | ||
Theorem | muldvds2d 41171 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β π β₯ π) | ||
Theorem | nndivdvdsd 41172 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16211. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) β β’ (π β (π β₯ π β (π / π) β β)) | ||
Theorem | nnproddivdvdsd 41173 | 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 41174 | 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 41175 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 gcd 5) = 1 | ||
Theorem | 60gcd6e6 41176 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 6) = 6 | ||
Theorem | 60gcd7e1 41177 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 7) = 1 | ||
Theorem | 420gcd8e4 41178 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 gcd 8) = 4 | ||
Theorem | lcmeprodgcdi 41179 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β & β’ πΊ β β & β’ π» β β & β’ (π gcd π) = πΊ & β’ (πΊ Β· π») = π΄ & β’ (π Β· π) = π΄ β β’ (π lcm π) = π» | ||
Theorem | 12lcm5e60 41180 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 lcm 5) = ;60 | ||
Theorem | 60lcm6e60 41181 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 6) = ;60 | ||
Theorem | 60lcm7e420 41182 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 7) = ;;420 | ||
Theorem | 420lcm8e840 41183 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 lcm 8) = ;;840 | ||
Theorem | lcmfunnnd 41184 | 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 41185 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...1)) = 1 | ||
Theorem | lcm2un 41186 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...2)) = 2 | ||
Theorem | lcm3un 41187 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...3)) = 6 | ||
Theorem | lcm4un 41188 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...4)) = ;12 | ||
Theorem | lcm5un 41189 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...5)) = ;60 | ||
Theorem | lcm6un 41190 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...6)) = ;60 | ||
Theorem | lcm7un 41191 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...7)) = ;;420 | ||
Theorem | lcm8un 41192 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...8)) = ;;840 | ||
Theorem | 3factsumint1 41193* | 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 41194* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β Ξ£π β π΅ β«π΄(πΉ Β· (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ β«π΄(πΊ Β· (πΉ Β· π»)) dπ₯) | ||
Theorem | 3factsumint3 41195* | 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 41196* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β β«π΄Ξ£π β π΅ (πΉ Β· (πΊ Β· π»)) dπ₯ = β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯) | ||
Theorem | 3factsumint 41197* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
β’ π΄ = (πΏ[,]π) & β’ (π β π΅ β Fin) & β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ πΉ) β (π΄βcnββ)) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ π») β (π΄βcnββ)) β β’ (π β β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ (πΊ Β· β«π΄(πΉ Β· π») dπ₯)) | ||
Theorem | resopunitintvd 41198 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0(,)1) β¦ π΄) β ((0(,)1)βcnββ)) | ||
Theorem | resclunitintvd 41199 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0[,]1) β¦ π΄) β ((0[,]1)βcnββ)) | ||
Theorem | resdvopclptsd 41200* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) & β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β β) β β’ (π β (β D (π₯ β (0[,]1) β¦ π΄)) = (π₯ β (0(,)1) β¦ π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |