Home | Metamath
Proof Explorer Theorem List (p. 206 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | evl1vsd 20501 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉))) | ||
Theorem | evl1expd 20502 | Polynomial evaluation builder for an exponential. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ ∙ = (.g‘(mulGrp‘𝑃)) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 ↑ 𝑉))) | ||
Theorem | pf1const 20503 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄) | ||
Theorem | pf1id 20504 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄) | ||
Theorem | pf1subrg 20505 | Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑄 ∈ (SubRing‘(𝑅 ↑s 𝐵))) | ||
Theorem | pf1rcl 20506 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) | ||
Theorem | pf1f 20507 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵) | ||
Theorem | mpfpf1 20508* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄) | ||
Theorem | pf1mpf 20509* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦ (𝑥‘∅))) ∈ 𝐸) | ||
Theorem | pf1addcl 20510 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄) | ||
Theorem | pf1mulcl 20511 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄) | ||
Theorem | pf1ind 20512* | Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁) & ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎) & ⊢ (𝑥 = (𝐵 × {𝑓}) → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = ( I ↾ 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) & ⊢ (𝑥 = (𝑓 ∘f + 𝑔) → (𝜓 ↔ 𝜁)) & ⊢ (𝑥 = (𝑓 ∘f · 𝑔) → (𝜓 ↔ 𝜎)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝐴 ∈ 𝑄) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | evl1gsumdlem 20513* | Lemma for evl1gsumd 20514 (induction step). (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) | ||
Theorem | evl1gsumd 20514* | Polynomial evaluation builder for a finite group sum of polynomials. (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝑈) & ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((𝑂‘𝑀)‘𝑌)))) | ||
Theorem | evl1gsumadd 20515* | Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd 20481. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌)))) | ||
Theorem | evl1gsumaddval 20516* | Value of a univariate polynomial evaluation mapping an additive group sum to a group sum of the evaluated variable. (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌)))‘𝐶) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((𝑄‘𝑌)‘𝐶)))) | ||
Theorem | evl1gsummul 20517* | Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ 1 = (1r‘𝑊) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝐻 = (mulGrp‘𝑃) & ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 1 ) ⇒ ⊢ (𝜑 → (𝑄‘(𝐺 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝐻 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌)))) | ||
Theorem | evl1varpw 20518 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 20515, the proof is shorter using evls1varpw 20484 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋))) | ||
Theorem | evl1varpwval 20519 | Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ 𝐻 = (mulGrp‘𝑅) & ⊢ 𝐸 = (.g‘𝐻) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑁 ↑ 𝑋))‘𝐶) = (𝑁𝐸𝐶)) | ||
Theorem | evl1scvarpw 20520 | Univariate polynomial evaluation maps a multiple of an exponentiation of a variable to the multiple of an exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ × = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝑆 = (𝑅 ↑s 𝐵) & ⊢ ∙ = (.r‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ 𝐹 = (.g‘𝑀) ⇒ ⊢ (𝜑 → (𝑄‘(𝐴 × (𝑁 ↑ 𝑋))) = ((𝐵 × {𝐴}) ∙ (𝑁𝐹(𝑄‘𝑋)))) | ||
Theorem | evl1scvarpwval 20521 | Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ × = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ 𝐻 = (mulGrp‘𝑅) & ⊢ 𝐸 = (.g‘𝐻) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑄‘(𝐴 × (𝑁 ↑ 𝑋)))‘𝐶) = (𝐴 · (𝑁𝐸𝐶))) | ||
Theorem | evl1gsummon 20522* | Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐻 = (mulGrp‘𝑅) & ⊢ 𝐸 = (.g‘𝐻) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ ↑ = (.g‘𝐺) & ⊢ × = ( ·𝑠 ‘𝑊) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑀 ⊆ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑄‘(𝑊 Σg (𝑥 ∈ 𝑀 ↦ (𝐴 × (𝑁 ↑ 𝑋)))))‘𝐶) = (𝑅 Σg (𝑥 ∈ 𝑀 ↦ (𝐴 · (𝑁𝐸𝐶))))) | ||
Syntax | cpsmet 20523 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 20524 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cmet 20525 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 20526 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 20527 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 20528 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 20529 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 20530 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 20531* | Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) | ||
Definition | df-xmet 20532* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 20533, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) | ||
Definition | df-met 20533* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22925. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. The 4 properties in Gleason's definition are shown by met0 22947, metgt0 22963, metsym 22954, and mettri 22956. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
Definition | df-bl 20534* | Define the metric space ball function. See blval 22990 for its value. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})) | ||
Definition | df-mopn 20535 | Define a function whose value is the family of open sets of a metric space. See elmopn 23046 for its main property. (Contributed by NM, 1-Sep-2006.) |
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
Definition | df-fbas 20536* | Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.) |
⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)}) | ||
Definition | df-fg 20537* | Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.) |
⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}) | ||
Definition | df-metu 20538* | Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) | ||
Syntax | ccnfld 20539 | Extend class notation with the field of complex numbers. |
class ℂfld | ||
Definition | df-cnfld 20540 |
The field of complex numbers. Other number fields and rings can be
constructed by applying the ↾s
restriction operator, for instance
(ℂfld ↾ 𝔸) is the
field of algebraic numbers.
The contract of this set is defined entirely by cnfldex 20542, cnfldadd 20544, cnfldmul 20545, cnfldcj 20546, cnfldtset 20547, cnfldle 20548, cnfldds 20549, and cnfldbas 20543. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) (New usage is discouraged.) |
⊢ ℂfld = (({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ∪ ({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉})) | ||
Theorem | cnfldstr 20541 | The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℂfld Struct 〈1, ;13〉 | ||
Theorem | cnfldex 20542 | The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℂfld ∈ V | ||
Theorem | cnfldbas 20543 | The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℂ = (Base‘ℂfld) | ||
Theorem | cnfldadd 20544 | The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ + = (+g‘ℂfld) | ||
Theorem | cnfldmul 20545 | The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ · = (.r‘ℂfld) | ||
Theorem | cnfldcj 20546 | The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ∗ = (*𝑟‘ℂfld) | ||
Theorem | cnfldtset 20547 | The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ (MetOpen‘(abs ∘ − )) = (TopSet‘ℂfld) | ||
Theorem | cnfldle 20548 | The ordering of the field of complex numbers. (Note that this is not actually an ordering on ℂ, but we put it in the structure anyway because restricting to ℝ does not affect this component, so that (ℂfld ↾s ℝ) is an ordered field even though ℂfld itself is not.) (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ≤ = (le‘ℂfld) | ||
Theorem | cnfldds 20549 | The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ (abs ∘ − ) = (dist‘ℂfld) | ||
Theorem | cnfldunif 20550 | The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld) | ||
Theorem | cnfldfun 20551 | The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.) |
⊢ Fun ℂfld | ||
Theorem | cnfldfunALT 20552 | Alternate proof of cnfldfun 20551 (much shorter proof, using cnfldstr 20541 and structn0fun 16489: in addition, it must be shown that ∅ ∉ ℂfld). (Contributed by AV, 18-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Fun ℂfld | ||
Theorem | xrsstr 20553 | The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 Struct 〈1, ;12〉 | ||
Theorem | xrsex 20554 | The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 ∈ V | ||
Theorem | xrsbas 20555 | The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ* = (Base‘ℝ*𝑠) | ||
Theorem | xrsadd 20556 | The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ +𝑒 = (+g‘ℝ*𝑠) | ||
Theorem | xrsmul 20557 | The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ·e = (.r‘ℝ*𝑠) | ||
Theorem | xrstset 20558 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠) | ||
Theorem | xrsle 20559 | The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ≤ = (le‘ℝ*𝑠) | ||
Theorem | cncrng 20560 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
⊢ ℂfld ∈ CRing | ||
Theorem | cnring 20561 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ Ring | ||
Theorem | xrsmcmn 20562 | The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 20576.) (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd | ||
Theorem | cnfld0 20563 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 0 = (0g‘ℂfld) | ||
Theorem | cnfld1 20564 | One is the unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘ℂfld) | ||
Theorem | cnfldneg 20565 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
Theorem | cnfldplusf 20566 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ + = (+𝑓‘ℂfld) | ||
Theorem | cnfldsub 20567 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘ℂfld) | ||
Theorem | cndrng 20568 | The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ DivRing | ||
Theorem | cnflddiv 20569 | The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ / = (/r‘ℂfld) | ||
Theorem | cnfldinv 20570 | The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋)) | ||
Theorem | cnfldmulg 20571 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | cnfldexp 20572 | The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐵(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑𝐵)) | ||
Theorem | cnsrng 20573 | The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ℂfld ∈ *-Ring | ||
Theorem | xrsmgm 20574 | The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ Mgm | ||
Theorem | xrsnsgrp 20575 | The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∉ Smgrp | ||
Theorem | xrsmgmdifsgrp 20576 | The "additive group" of the extended reals is a magma but not a semigroup, and therefore also not a monoid nor a group, in contrast to the "multiplicative group", see xrsmcmn 20562. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp) | ||
Theorem | xrs1mnd 20577 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 20576. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | xrs10 20578 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | xrs1cmn 20579 | The extended real numbers restricted to ℝ* ∖ {-∞} form a commutative monoid. They are not a group because 1 + +∞ = 2 + +∞ even though 1 ≠ 2. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | xrge0subm 20580 | The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ (0[,]+∞) ∈ (SubMnd‘𝑅) | ||
Theorem | xrge0cmn 20581 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
Theorem | xrsds 20582* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
Theorem | xrsdsval 20583 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
Theorem | xrsdsreval 20584 | The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
Theorem | xrsdsreclblem 20585 | Lemma for xrsdsreclb 20586. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | xrsdsreclb 20586 | The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) → ((𝐴𝐷𝐵) ∈ ℝ ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | cnsubmlem 20587* | Lemma for nn0subm 20594 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 20588* | Lemma for resubdrg 20746 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 20589* | Lemma for resubdrg 20746 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubdrglem 20590* | Lemma for resubdrg 20746 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
Theorem | qsubdrg 20591 | The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing) | ||
Theorem | zsubrg 20592 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) | ||
Theorem | gzsubrg 20593 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
Theorem | nn0subm 20594 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
Theorem | rege0subm 20595 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
Theorem | absabv 20596 | The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ abs ∈ (AbsVal‘ℂfld) | ||
Theorem | zsssubrg 20597 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
Theorem | qsssubdrg 20598 | The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝑅) ∈ DivRing) → ℚ ⊆ 𝑅) | ||
Theorem | cnsubrg 20599 | There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) | ||
Theorem | cnmgpabl 20600 | The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ 𝑀 ∈ Abel |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |