Home | Metamath
Proof Explorer Theorem List (p. 390 of 449) | < 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: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hgmapffval 38901* | Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (HGMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥 ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠 ‘𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚‘𝑣))))})) | ||
Theorem | hgmapfval 38902* | Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣))))) | ||
Theorem | hgmapval 38903* | Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of [Baer] p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 38898. (Contributed by NM, 25-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ 𝑀 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐼 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) = (℩𝑦 ∈ 𝐵 ∀𝑣 ∈ 𝑉 (𝑀‘(𝑋 · 𝑣)) = (𝑦 ∙ (𝑀‘𝑣)))) | ||
Theorem | hgmapfnN 38904 | Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐺 Fn 𝐵) | ||
Theorem | hgmapcl 38905 | Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘𝐹) ∈ 𝐵) | ||
Theorem | hgmapdcl 38906 | Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑄 = (Scalar‘𝐶) & ⊢ 𝐴 = (Base‘𝑄) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘𝐹) ∈ 𝐴) | ||
Theorem | hgmapvs 38907 | Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) = ((𝐺‘𝐹) ∙ (𝑆‘𝑋))) | ||
Theorem | hgmapval0 38908 | Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝐺‘ 0 ) = 0 ) | ||
Theorem | hgmapval1 38909 | Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝐺‘ 1 ) = 1 ) | ||
Theorem | hgmapadd 38910 | Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘(𝑋 + 𝑌)) = ((𝐺‘𝑋) + (𝐺‘𝑌))) | ||
Theorem | hgmapmul 38911 | Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘(𝑋 · 𝑌)) = ((𝐺‘𝑌) · (𝐺‘𝑋))) | ||
Theorem | hgmaprnlem1N 38912 | Lemma for hgmaprnN 38917. (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 | hgmaprnlem2N 38913 | Lemma for hgmaprnN 38917. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero 𝑧 is taken care of automatically. (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 })) & ⊢ (𝜑 → 𝑠 ∈ 𝑉) & ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡))) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LSpan‘𝐶) ⇒ ⊢ (𝜑 → (𝑁‘{𝑠}) ⊆ (𝑁‘{𝑡})) | ||
Theorem | hgmaprnlem3N 38914* | Lemma for hgmaprnN 38917. 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 })) & ⊢ (𝜑 → 𝑠 ∈ 𝑉) & ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡))) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LSpan‘𝐶) ⇒ ⊢ (𝜑 → 𝑧 ∈ ran 𝐺) | ||
Theorem | hgmaprnlem4N 38915* | Lemma for hgmaprnN 38917. 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 38916 | Lemma for hgmaprnN 38917. 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 38917 | 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 38918 | The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐺‘𝑋) = (𝐺‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | hgmapf1oN 38919 | 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 38920 | 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 38921 | 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 38922 | 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 38923 | Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌))) | ||
Theorem | hdmaplns1 38924 | Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑁 = (-g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌))) | ||
Theorem | hdmaplnm1 38925 | Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋))) | ||
Theorem | hdmaplna2 38926 | Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋))) | ||
Theorem | hdmapglnm2 38927 | 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 38928 | 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 38929 | 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 38930 | Membership in the kernel (as shown by hdmaplkr 38929) 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 38931 | 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 38932 | 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 38933 | 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 38934 | Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 38852. 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 38935 | 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 38936 | 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 38937 | 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 38852. 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 38938 | 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 38939 | 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 38940 | Lemma for hgmapvv 38942. 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 38941 | Lemma for hgmapvv 38942. 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 38942 | 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 38943* | Lemma for hdmapg 38946. (Contributed by NM, 14-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢)) | ||
Theorem | hdmapglem7b 38944 | Lemma for hdmapg 38946. (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 38945 | Lemma for hdmapg 38946. Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). In the proof, our 𝐸, (𝑂‘{𝐸}) 𝑋, 𝑌, 𝑘, 𝑢, 𝑙, 𝑣 correspond to Baer's w, H, x, y, x', x'', y' , 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 38946 | 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 38947* | 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 38948 | Extend class notation with the final constructed Hilbert space. |
class HLHil | ||
Definition | df-hlhil 38949* | 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 38950* | 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 38951 | 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 38952 | 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 38953 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐿) ⇒ ⊢ (𝜑 → + = (+g‘𝑈)) | ||
Theorem | hlhilslem 38954 | Lemma for hlhilsbase2 38958. (Contributed by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐹 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 4 & ⊢ 𝐶 = (𝐹‘𝐸) ⇒ ⊢ (𝜑 → 𝐶 = (𝐹‘𝑅)) | ||
Theorem | hlhilsbase 38955 | The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝐶 = (Base‘𝑅)) | ||
Theorem | hlhilsplus 38956 | Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ + = (+g‘𝐸) ⇒ ⊢ (𝜑 → + = (+g‘𝑅)) | ||
Theorem | hlhilsmul 38957 | Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ · = (.r‘𝐸) ⇒ ⊢ (𝜑 → · = (.r‘𝑅)) | ||
Theorem | hlhilsbase2 38958 | 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 38959 | 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 38960 | 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 38961 | 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 38962 | 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 38963 | 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 38964* | 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 38965 | 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 38966 | 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 38967 | 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 38968 | 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 38969 | Lemma for hlhilsrng 38970. (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 38970 | 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 38971 | 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 38972 | 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 38973 | 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 38974 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 38952 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 38975* | Lemma for hlhil 23973. (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 38976* | Lemma for hlhil 23973. (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 38977 |
Construction of a Hilbert space (df-hil 20776) 𝑈 from a Hilbert
lattice (df-hlat 36367) 𝐾, where 𝑊 is a fixed but arbitrary
hyperplane (co-atom) in 𝐾.
The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 38125) 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 38125. 𝑊 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 20776. 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) | ||
Theorem | ioin9i8 38978 | Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜒 → ¬ 𝜃) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | jaodd 38979 | Double deduction form of jaoi 851. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃))) | ||
Theorem | nsb 38980 | Generalization rule for negated wff. (Contributed by Steven Nguyen, 3-May-2023.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ [𝑥 / 𝑦]𝜑 | ||
Theorem | sbn1 38981 | One direction of sbn 2278, using fewer axioms. Compare 19.2 1972. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ ([𝑡 / 𝑥] ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑) | ||
Theorem | sbor2 38982 | One direction of sbor 2307, using fewer axioms. Compare 19.33 1876. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓)) | ||
Theorem | 3rspcedvd 38983* | Triple application of rspcedvd 3623. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓) | ||
Theorem | rabeqcda 38984* | When 𝜓 is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc 3675. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = 𝐴) | ||
Theorem | rabdif 38985* | Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑} | ||
Theorem | sn-axrep5v 38986* | A condensed form of axrep5 5187. (Contributed by SN, 21-Sep-2023.) |
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑)) | ||
Theorem | sn-axprlem3 38987* | axprlem3 5316 using only Tarski's FOL axiom schemes and ax-rep 5181. (Contributed by SN, 22-Sep-2023.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏)) | ||
Theorem | sn-el 38988* | A version of el 5261 with an inner existential quantifier on 𝑥, which avoids ax-7 2006 and ax-8 2107. (Contributed by SN, 18-Sep-2023.) |
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 | ||
Theorem | sn-dtru 38989* | dtru 5262 without ax-8 2107 or ax-12 2167. (Contributed by SN, 21-Sep-2023.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | pssexg 38990 | The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | pssn0 38991 | A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅) | ||
Theorem | psspwb 38992 | Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵) | ||
Theorem | xppss12 38993 | Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷)) | ||
Theorem | elpwbi 38994 | Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | opelxpii 38995 | Ordered pair membership in a Cartesian product (implication). (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ 𝐴 ∈ 𝐶 & ⊢ 𝐵 ∈ 𝐷 ⇒ ⊢ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) | ||
Theorem | iunsn 38996* | Indexed union of a singleton. Compare dfiun2 4949 and rnmpt 5820. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝐵} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | ||
Theorem | imaopab 38997* | The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} | ||
Theorem | fnsnbt 38998 | A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) | ||
Theorem | fnimasnd 38999 | The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 “ {𝑆}) = {(𝐹‘𝑆)}) | ||
Theorem | dfqs2 39000* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |