| Metamath
Proof Explorer Theorem List (p. 420 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hgmaprnlem4N 41901* | Lemma for hgmaprnN 41903. Eliminate 𝑠. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑃 = (Scalar‘𝐶) & ⊢ 𝐴 = (Base‘𝑃) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑧 ∈ 𝐴) & ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝑧 ∈ ran 𝐺) | ||
| Theorem | hgmaprnlem5N 41902 | Lemma for hgmaprnN 41903. Eliminate 𝑡. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝑃 = (Scalar‘𝐶) & ⊢ 𝐴 = (Base‘𝑃) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ 𝑄 = (0g‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑧 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑧 ∈ ran 𝐺) | ||
| Theorem | hgmaprnN 41903 | Part of proof of part 16 in [Baer] p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ran 𝐺 = 𝐵) | ||
| Theorem | hgmap11 41904 | The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌)) | ||
| Theorem | hgmapf1oN 41905 | The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐵) | ||
| Theorem | hgmapeq0 41906 | The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐺‘𝑋) = 0 ↔ 𝑋 = 0 )) | ||
| Theorem | hdmapipcl 41907 | The inner product (Hermitian form) (𝑋, 𝑌) will be defined as ((𝑆‘𝑌)‘𝑋). Show closure. (Contributed by NM, 7-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑌)‘𝑋) ∈ 𝐵) | ||
| Theorem | hdmapln1 41908 | Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘((𝐴 · 𝑋) + 𝑌)) = ((𝐴 × ((𝑆‘𝑍)‘𝑋)) ⨣ ((𝑆‘𝑍)‘𝑌))) | ||
| Theorem | hdmaplna1 41909 | Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌))) | ||
| Theorem | hdmaplns1 41910 | Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑁 = (-g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌))) | ||
| Theorem | hdmaplnm1 41911 | Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋))) | ||
| Theorem | hdmaplna2 41912 | Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋))) | ||
| Theorem | hdmapglnm2 41913 | g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑆‘(𝐴 · 𝑌))‘𝑋) = (((𝑆‘𝑌)‘𝑋) × (𝐺‘𝐴))) | ||
| Theorem | hdmapgln2 41914 | g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑆‘((𝐴 · 𝑌) + 𝑍))‘𝑋) = ((((𝑆‘𝑌)‘𝑋) × (𝐺‘𝐴)) ⨣ ((𝑆‘𝑍)‘𝑋))) | ||
| Theorem | hdmaplkr 41915 | Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate 𝐹 hypothesis. (Contributed by NM, 9-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝑌 = (LKer‘𝑈) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑌‘(𝑆‘𝑋)) = (𝑂‘{𝑋})) | ||
| Theorem | hdmapellkr 41916 | Membership in the kernel (as shown by hdmaplkr 41915) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑌) = 0 ↔ 𝑌 ∈ (𝑂‘{𝑋}))) | ||
| Theorem | hdmapip0 41917 | Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑍 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 ↔ 𝑋 = 0 )) | ||
| Theorem | hdmapip1 41918 | Construct a proportional vector 𝑌 whose inner product with the original 𝑋 equals one. (Contributed by NM, 13-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invr‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ 𝑌 = ((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 1 ) | ||
| Theorem | hdmapip0com 41919 | Commutation property of Baer's sigma map (Holland's A map). Line 20 of [Holland95] p. 14. Also part of Lemma 1 of [Baer] p. 110 line 7. (Contributed by NM, 9-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑌) = 0 ↔ ((𝑆‘𝑌)‘𝑋) = 0 )) | ||
| Theorem | hdmapinvlem1 41920 | Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 41838. Our ((𝑆‘𝐸)‘𝐶) means the inner product 〈𝐶, 𝐸〉 i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) ⇒ ⊢ (𝜑 → ((𝑆‘𝐸)‘𝐶) = 0 ) | ||
| Theorem | hdmapinvlem2 41921 | Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) ⇒ ⊢ (𝜑 → ((𝑆‘𝐶)‘𝐸) = 0 ) | ||
| Theorem | hdmapinvlem3 41922 | Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) & ⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶)) ⇒ ⊢ (𝜑 → ((𝑆‘((𝐽 · 𝐸) − 𝐷))‘((𝐼 · 𝐸) + 𝐶)) = 0 ) | ||
| Theorem | hdmapinvlem4 41923 | Part 1.1 of Proposition 1 of [Baer] p. 110. We use 𝐶, 𝐷, 𝐼, and 𝐽 for Baer's u, v, s, and t. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 41838. Our ((𝑆‘𝐷)‘𝐶) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) & ⊢ (𝜑 → (𝐼 × (𝐺‘𝐽)) = ((𝑆‘𝐷)‘𝐶)) ⇒ ⊢ (𝜑 → (𝐽 × (𝐺‘𝐼)) = ((𝑆‘𝐶)‘𝐷)) | ||
| Theorem | hdmapglem5 41924 | Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘((𝑆‘𝐷)‘𝐶)) = ((𝑆‘𝐶)‘𝐷)) | ||
| Theorem | hgmapvvlem1 41925 | Involution property of scalar sigma map. Line 10 in [Baer] p. 111, t sigma squared = t. Our 𝐸, 𝐶, 𝐷, 𝑌, 𝑋 correspond to Baer's w, h, k, s, t. (Contributed by NM, 13-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invr‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 ) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → (𝑌 × (𝐺‘𝑋)) = 1 ) ⇒ ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) | ||
| Theorem | hgmapvvlem2 41926 | Lemma for hgmapvv 41928. Eliminate 𝑌 (Baer's s). (Contributed by NM, 13-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invr‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) & ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 ) ⇒ ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) | ||
| Theorem | hgmapvvlem3 41927 | Lemma for hgmapvv 41928. Eliminate ((𝑆‘𝐷)‘𝐶) = 1 (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invr‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) | ||
| Theorem | hgmapvv 41928 | 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 41929* | Lemma for hdmapg 41932. (Contributed by NM, 14-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢)) | ||
| Theorem | hdmapglem7b 41930 | Lemma for hdmapg 41932. (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 41931 | Lemma for hdmapg 41932. 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 41932 | 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 41933* | 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 41934 | Extend class notation with the final constructed Hilbert space. |
| class HLHil | ||
| Definition | df-hlhil 41935* | 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 41936* | 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 41937 | 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 41938 | 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 41939 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐿) ⇒ ⊢ (𝜑 → + = (+g‘𝑈)) | ||
| Theorem | hlhilslem 41940 | Lemma for hlhilsbase 41942 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 41941 | Obsolete version of hlhilslem 41940 as of 6-Nov-2024. Lemma for hlhilsbase 41942. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐹 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 4 & ⊢ 𝐶 = (𝐹‘𝐸) ⇒ ⊢ (𝜑 → 𝐶 = (𝐹‘𝑅)) | ||
| Theorem | hlhilsbase 41942 | 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 41943 | Obsolete version of hlhilsbase 41942 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 41944 | 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 41945 | Obsolete version of hlhilsplus 41944 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 41946 | 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 41947 | Obsolete version of hlhilsmul 41946 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 41948 | 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 41949 | 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 41950 | 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 41951 | 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 41952 | 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 41953 | 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 41954* | 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 41955 | 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 41956 | 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 41957 | 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 41958 | 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 41959 | Lemma for hlhilsrng 41960. (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 41960 | 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 41961 | 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 41962 | 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 41963 | 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 41964 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 41938 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 41965* | Lemma for hlhil 25477. (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 41966* | Lemma for hlhil 25477. (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 41967 |
Construction of a Hilbert space (df-hil 21724) 𝑈 from a Hilbert
lattice (df-hlat 39352) 𝐾, where 𝑊 is a fixed but arbitrary
hyperplane (co-atom) in 𝐾.
The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 41111) 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 41111. 𝑊 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 21724. 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 41968 | Extend class notation with the class of all commutative semirings. |
| class CSRing | ||
| Definition | df-csring 41969 | Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.) |
| ⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd} | ||
| Theorem | iscsrg 41970 | A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ CSRing ↔ (𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd)) | ||
| Theorem | rhmzrhval 41971 | Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ ℤ) & ⊢ 𝑀 = (ℤRHom‘𝑅) & ⊢ 𝑁 = (ℤRHom‘𝑆) ⇒ ⊢ (𝜑 → (𝐹‘(𝑀‘𝑋)) = (𝑁‘𝑋)) | ||
| Theorem | zndvdchrrhm 41972* | Construction of a ring homomorphism from ℤ/nℤ to 𝑅 when the characteristic of 𝑅 divides 𝑁. (Contributed by metakunt, 4-Jun-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (chr‘𝑅) ∈ ℤ) & ⊢ (𝜑 → (chr‘𝑅) ∥ 𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑍) ↦ ∪ ((ℤRHom‘𝑅) “ 𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑍 RingHom 𝑅)) | ||
| Theorem | leexp1ad 41973 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
| Theorem | relogbcld 41974 | 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 41975 | 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 41976 | 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 41977 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑌) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)) | ||
| Theorem | uzindd 41978* | 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 41979 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑂 ∈ ℤ) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃)) & ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂)) & ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃)) ⇒ ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅)) | ||
| Theorem | zltp1led 41980 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) | ||
| Theorem | fzne2d 41981 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ≠ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 < 𝑁) | ||
| Theorem | eqfnfv2d2 41982* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | fzsplitnd 41983 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
| Theorem | fzsplitnr 41984 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
| Theorem | addassnni 41985 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
| Theorem | addcomnni 41986 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
| Theorem | mulassnni 41987 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
| Theorem | mulcomnni 41988 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
| Theorem | gcdcomnni 41989 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀) | ||
| Theorem | gcdnegnni 41990 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁) | ||
| Theorem | neggcdnni 41991 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁) | ||
| Theorem | bccl2d 41992 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ) | ||
| Theorem | recbothd 41993 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶))) | ||
| Theorem | gcdmultiplei 41994 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀 | ||
| Theorem | gcdaddmzz2nni 41995 | 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 41996 | 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 41997 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) ∈ ℕ | ||
| Theorem | muldvds1d 41998 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
| Theorem | muldvds2d 41999 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝑀 ∥ 𝑁) | ||
| Theorem | nndivdvdsd 42000 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16299. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |