Home | Metamath
Proof Explorer Theorem List (p. 206 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | evl1var 20501 | Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐵)) | ||
Theorem | evl1vard 20502 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ ((𝑂‘𝑋)‘𝑌) = 𝑌)) | ||
Theorem | evls1var 20503 | Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑋 = (var1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → (𝑄‘𝑋) = ( I ↾ 𝐵)) | ||
Theorem | evls1scasrng 20504 | The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 13-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑂 = (eval1‘𝑆) & ⊢ 𝑊 = (Poly1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑃 = (Poly1‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐶 = (algSc‘𝑃) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝑂‘(𝐶‘𝑋))) | ||
Theorem | evls1varsrng 20505 | The evaluation of the variable of univariate polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.) |
⊢ 𝑄 = (𝑆 evalSub1 𝑅) & ⊢ 𝑂 = (eval1‘𝑆) & ⊢ 𝑉 = (var1‘𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → (𝑄‘𝑉) = (𝑂‘𝑉)) | ||
Theorem | evl1addd 20506 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊))) | ||
Theorem | evl1subd 20507 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ − = (-g‘𝑃) & ⊢ 𝐷 = (-g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊))) | ||
Theorem | evl1muld 20508 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊))) | ||
Theorem | evl1vsd 20509 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉))) | ||
Theorem | evl1expd 20510 | 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 20511 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄) | ||
Theorem | pf1id 20512 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄) | ||
Theorem | pf1subrg 20513 | 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 20514 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) | ||
Theorem | pf1f 20515 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵) | ||
Theorem | mpfpf1 20516* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄) | ||
Theorem | pf1mpf 20517* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1o eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦ (𝑥‘∅))) ∈ 𝐸) | ||
Theorem | pf1addcl 20518 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄) | ||
Theorem | pf1mulcl 20519 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄) | ||
Theorem | pf1ind 20520* | 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 20521* | Lemma for evl1gsumd 20522 (induction step). (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) | ||
Theorem | evl1gsumd 20522* | 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 20523* | 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 20489. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌)))) | ||
Theorem | evl1gsumaddval 20524* | 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 20525* | 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 20526 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 20523, the proof is shorter using evls1varpw 20492 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋))) | ||
Theorem | evl1varpwval 20527 | 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 20528 | 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 20529 | 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 20530* | 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 20531 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 20532 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cmet 20533 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 20534 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 20535 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 20536 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 20537 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 20538 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 20539* | 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 20540* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 20541, 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 20541* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22933. 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 22955, metgt0 22971, metsym 22962, and mettri 22964. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
Definition | df-bl 20542* | Define the metric space ball function. See blval 22998 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 20543 | Define a function whose value is the family of open sets of a metric space. See elmopn 23054 for its main property. (Contributed by NM, 1-Sep-2006.) |
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
Definition | df-fbas 20544* | 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 20545* | 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 20546* | 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 20547 | Extend class notation with the field of complex numbers. |
class ℂfld | ||
Definition | df-cnfld 20548 |
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 20550, cnfldadd 20552, cnfldmul 20553, cnfldcj 20554, cnfldtset 20555, cnfldle 20556, cnfldds 20557, and cnfldbas 20551. 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 20549 | 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 20550 | 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 20551 | 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 20552 | 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 20553 | 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 20554 | 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 20555 | 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 20556 | 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 20557 | 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 20558 | The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld) | ||
Theorem | cnfldfun 20559 | The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.) |
⊢ Fun ℂfld | ||
Theorem | cnfldfunALT 20560 | Alternate proof of cnfldfun 20559 (much shorter proof, using cnfldstr 20549 and structn0fun 16497: 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 20561 | The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 Struct 〈1, ;12〉 | ||
Theorem | xrsex 20562 | The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 ∈ V | ||
Theorem | xrsbas 20563 | The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ* = (Base‘ℝ*𝑠) | ||
Theorem | xrsadd 20564 | The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ +𝑒 = (+g‘ℝ*𝑠) | ||
Theorem | xrsmul 20565 | The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ·e = (.r‘ℝ*𝑠) | ||
Theorem | xrstset 20566 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠) | ||
Theorem | xrsle 20567 | The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ≤ = (le‘ℝ*𝑠) | ||
Theorem | cncrng 20568 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
⊢ ℂfld ∈ CRing | ||
Theorem | cnring 20569 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ Ring | ||
Theorem | xrsmcmn 20570 | The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 20584.) (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd | ||
Theorem | cnfld0 20571 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 0 = (0g‘ℂfld) | ||
Theorem | cnfld1 20572 | One is the unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘ℂfld) | ||
Theorem | cnfldneg 20573 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
Theorem | cnfldplusf 20574 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ + = (+𝑓‘ℂfld) | ||
Theorem | cnfldsub 20575 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘ℂfld) | ||
Theorem | cndrng 20576 | The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ DivRing | ||
Theorem | cnflddiv 20577 | 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 20578 | The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋)) | ||
Theorem | cnfldmulg 20579 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | cnfldexp 20580 | 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 20581 | The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ℂfld ∈ *-Ring | ||
Theorem | xrsmgm 20582 | The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ Mgm | ||
Theorem | xrsnsgrp 20583 | The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∉ Smgrp | ||
Theorem | xrsmgmdifsgrp 20584 | 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 20570. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ (Mgm ∖ Smgrp) | ||
Theorem | xrs1mnd 20585 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 20584. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | xrs10 20586 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | xrs1cmn 20587 | 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 20588 | 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 20589 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
Theorem | xrsds 20590* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
Theorem | xrsdsval 20591 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
Theorem | xrsdsreval 20592 | 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 20593 | Lemma for xrsdsreclb 20594. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | xrsdsreclb 20594 | 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 20595* | Lemma for nn0subm 20602 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 20596* | Lemma for resubdrg 20754 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 20597* | Lemma for resubdrg 20754 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubdrglem 20598* | Lemma for resubdrg 20754 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
Theorem | qsubdrg 20599 | 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 20600 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |