![]() |
Metamath
Proof Explorer Theorem List (p. 393 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hdmapipcl 39201 | 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 39202 | 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 39203 | Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 + 𝑌)) = (((𝑆‘𝑍)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑌))) | ||
Theorem | hdmaplns1 39204 | Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑁 = (-g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘𝑍)‘(𝑋 − 𝑌)) = (((𝑆‘𝑍)‘𝑋)𝑁((𝑆‘𝑍)‘𝑌))) | ||
Theorem | hdmaplnm1 39205 | Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑆‘𝑌)‘(𝐴 · 𝑋)) = (𝐴 × ((𝑆‘𝑌)‘𝑋))) | ||
Theorem | hdmaplna2 39206 | Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝑅) & ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑆‘(𝑌 + 𝑍))‘𝑋) = (((𝑆‘𝑌)‘𝑋) ⨣ ((𝑆‘𝑍)‘𝑋))) | ||
Theorem | hdmapglnm2 39207 | 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 39208 | 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 39209 | 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 39210 | Membership in the kernel (as shown by hdmaplkr 39209) 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 39211 | 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 39212 | 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 39213 | 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 39214 | Line 27 in [Baer] p. 110. We use 𝐶 for Baer's u. Our unit vector 𝐸 has the required properties for his w by hdmapevec2 39132. 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 39215 | 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 39216 | 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 39217 | 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 39132. 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 39218 | 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 39219 | 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 39220 | Lemma for hgmapvv 39222. 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 39221 | Lemma for hgmapvv 39222. 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 39222 | 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 39223* | Lemma for hdmapg 39226. (Contributed by NM, 14-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ (𝑂‘{𝐸})∃𝑘 ∈ 𝐵 𝑋 = ((𝑘 · 𝐸) + 𝑢)) | ||
Theorem | hdmapglem7b 39224 | Lemma for hdmapg 39226. (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 39225 | Lemma for hdmapg 39226. 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 39226 | 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 39227* | 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 39228 | Extend class notation with the final constructed Hilbert space. |
class HLHil | ||
Definition | df-hlhil 39229* | 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 39230* | 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 39231 | 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 39232 | 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 39233 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐿) ⇒ ⊢ (𝜑 → + = (+g‘𝑈)) | ||
Theorem | hlhilslem 39234 | Lemma for hlhilsbase2 39238. (Contributed by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐹 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 4 & ⊢ 𝐶 = (𝐹‘𝐸) ⇒ ⊢ (𝜑 → 𝐶 = (𝐹‘𝑅)) | ||
Theorem | hlhilsbase 39235 | 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 39236 | 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 39237 | 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 39238 | 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 39239 | 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 39240 | 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 39241 | 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 39242 | 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 39243 | 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 39244* | 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 39245 | 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 39246 | 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 39247 | 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 39248 | 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 39249 | Lemma for hlhilsrng 39250. (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 39250 | 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 39251 | 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 39252 | 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 39253 | 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 39254 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 39232 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 39255* | Lemma for hlhil 24047. (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 39256* | Lemma for hlhil 24047. (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 39257 |
Construction of a Hilbert space (df-hil 20393) 𝑈 from a Hilbert
lattice (df-hlat 36647) 𝐾, where 𝑊 is a fixed but arbitrary
hyperplane (co-atom) in 𝐾.
The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 38405) 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 38405. 𝑊 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 20393. 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 | leexp1ad 39258 | Weak mantissa ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
Theorem | relogbcld 39259 | 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 39260 | 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 39261 | 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 39262 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑌) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)) | ||
Theorem | fzindd 39263* | Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝑥 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁) ∧ 𝜃) → 𝜏) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) → 𝜂) | ||
Theorem | uzindd 39264* | 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 39265 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑂 ∈ ℤ) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃)) & ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂)) & ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃)) ⇒ ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅)) | ||
Theorem | zltlem1d 39266 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
Theorem | zltp1led 39267 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) | ||
Theorem | fzne2d 39268 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ≠ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 < 𝑁) | ||
Theorem | eqfnfv2d2 39269* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | fzsplitnd 39270 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
Theorem | fzsplitnr 39271 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
Theorem | addassnni 39272 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | addcomnni 39273 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
Theorem | mulassnni 39274 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | mulcomnni 39275 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | gcdcomnni 39276 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀) | ||
Theorem | gcdnegnni 39277 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁) | ||
Theorem | neggcdnni 39278 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁) | ||
Theorem | bccl2d 39279 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ) | ||
Theorem | recbothd 39280 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶))) | ||
Theorem | gcdmultiplei 39281 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀 | ||
Theorem | gcdaddmzz2nni 39282 | 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 39283 | 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 39284 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) ∈ ℕ | ||
Theorem | dvdstrd 39285 | The divides relation is transitive, a deduction version of dvdstr 15638. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
Theorem | muldvds1d 39286 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
Theorem | muldvds2d 39287 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝑀 ∥ 𝑁) | ||
Theorem | nndivdvdsd 39288 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 15608. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ)) | ||
Theorem | nnproddivdvdsd 39289 | 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 39290 | 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 39291 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;12 gcd 5) = 1 | ||
Theorem | 60gcd6e6 39292 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 gcd 6) = 6 | ||
Theorem | 60gcd7e1 39293 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 gcd 7) = 1 | ||
Theorem | 420gcd8e4 39294 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;;420 gcd 8) = 4 | ||
Theorem | lcmeprodgcdi 39295 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝐻 ∈ ℕ & ⊢ (𝑀 gcd 𝑁) = 𝐺 & ⊢ (𝐺 · 𝐻) = 𝐴 & ⊢ (𝑀 · 𝑁) = 𝐴 ⇒ ⊢ (𝑀 lcm 𝑁) = 𝐻 | ||
Theorem | 12lcm5e60 39296 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;12 lcm 5) = ;60 | ||
Theorem | 60lcm6e60 39297 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 lcm 6) = ;60 | ||
Theorem | 60lcm7e420 39298 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 lcm 7) = ;;420 | ||
Theorem | 420lcm8e840 39299 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;;420 lcm 8) = ;;840 | ||
Theorem | lcmfunnnd 39300 | Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (lcm‘(1...𝑁)) = ((lcm‘(1...(𝑁 − 1))) lcm 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |