Home | Metamath
Proof Explorer Theorem List (p. 198 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | evl1vard 19701 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ ((𝑂‘𝑋)‘𝑌) = 𝑌)) | ||
Theorem | evls1var 19702 | 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 19703 | 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 19704 | 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 19705 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊))) | ||
Theorem | evl1subd 19706 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ − = (-g‘𝑃) & ⊢ 𝐷 = (-g‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊))) | ||
Theorem | evl1muld 19707 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊))) | ||
Theorem | evl1vsd 19708 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ ∙ = ( ·𝑠 ‘𝑃) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉))) | ||
Theorem | evl1expd 19709 | 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 19710 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄) | ||
Theorem | pf1id 19711 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄) | ||
Theorem | pf1subrg 19712 | 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 19713 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) ⇒ ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) | ||
Theorem | pf1f 19714 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵) | ||
Theorem | mpfpf1 19715* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1𝑜 eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 × {𝑦}))) ∈ 𝑄) | ||
Theorem | pf1mpf 19716* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = ran (1𝑜 eval 𝑅) ⇒ ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚 1𝑜) ↦ (𝑥‘∅))) ∈ 𝐸) | ||
Theorem | pf1addcl 19717 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘𝑓 + 𝐺) ∈ 𝑄) | ||
Theorem | pf1mulcl 19718 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑄 = ran (eval1‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘𝑓 · 𝐺) ∈ 𝑄) | ||
Theorem | pf1ind 19719* | 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 ↾ 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) & ⊢ (𝑥 = (𝑓 ∘𝑓 + 𝑔) → (𝜓 ↔ 𝜁)) & ⊢ (𝑥 = (𝑓 ∘𝑓 · 𝑔) → (𝜓 ↔ 𝜎)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝐴 ∈ 𝑄) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | evl1gsumdlem 19720* | Lemma for evl1gsumd 19721 (induction step). (Contributed by AV, 17-Sep-2019.) |
⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌)))))) | ||
Theorem | evl1gsumd 19721* | 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 19722* | 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 19689. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝑃 = (𝑅 ↑s 𝐾) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌)))) | ||
Theorem | evl1gsumaddval 19723* | 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 19724* | 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 19725 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 19722, the proof is shorter using evls1varpw 19691 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
⊢ 𝑄 = (eval1‘𝑅) & ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑊) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋))) | ||
Theorem | evl1varpwval 19726 | 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 19727 | 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 19728 | 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 19729* | 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 19730 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmt 19731 | Extend class notation with the class of all extended metric spaces. |
class ∞Met | ||
Syntax | cme 19732 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 19733 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 19734 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 19735 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 19736 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 19737 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 19738* | 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 ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) | ||
Definition | df-xmet 19739* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 19740, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}) | ||
Definition | df-met 19740* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22126. 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 22148, metgt0 22164, metsym 22155, and mettri 22157. (Contributed by NM, 25-Aug-2006.) |
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}) | ||
Definition | df-bl 19741* | Define the metric space ball function. See blval 22191 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 19742 | Define a function whose value is the family of open sets of a metric space. See elmopn 22247 for its main property. (Contributed by NM, 1-Sep-2006.) |
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) | ||
Definition | df-fbas 19743* | 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 19744* | 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 19745* | 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 19746 | Extend class notation with the field of complex numbers. |
class ℂfld | ||
Definition | df-cnfld 19747 |
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 19749, cnfldadd 19751, cnfldmul 19752, cnfldcj 19753, cnfldtset 19754, cnfldle 19755, cnfldds 19756, and cnfldbas 19750. 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 19748 | 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 19749 | 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 19750 | 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 19751 | 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 19752 | 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 19753 | 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 19754 | 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 19755 | 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 19756 | 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 19757 | The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld) | ||
Theorem | cnfldfun 19758 | The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.) |
⊢ Fun ℂfld | ||
Theorem | cnfldfunALT 19759 | Alternate proof of cnfldfun 19758 (much shorter proof, using cnfldstr 19748 and structn0fun 15869: 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 19760 | The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 Struct 〈1, ;12〉 | ||
Theorem | xrsex 19761 | The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 ∈ V | ||
Theorem | xrsbas 19762 | The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ* = (Base‘ℝ*𝑠) | ||
Theorem | xrsadd 19763 | The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ +𝑒 = (+g‘ℝ*𝑠) | ||
Theorem | xrsmul 19764 | The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ·e = (.r‘ℝ*𝑠) | ||
Theorem | xrstset 19765 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠) | ||
Theorem | xrsle 19766 | The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ≤ = (le‘ℝ*𝑠) | ||
Theorem | cncrng 19767 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
⊢ ℂfld ∈ CRing | ||
Theorem | cnring 19768 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ Ring | ||
Theorem | xrsmcmn 19769 | The multiplicative group of the extended reals forms a commutative monoid (even though the additive group is not, see xrsmgmdifsgrp 19783.) (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd | ||
Theorem | cnfld0 19770 | The zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 0 = (0g‘ℂfld) | ||
Theorem | cnfld1 19771 | The unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘ℂfld) | ||
Theorem | cnfldneg 19772 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
Theorem | cnfldplusf 19773 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ + = (+𝑓‘ℂfld) | ||
Theorem | cnfldsub 19774 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘ℂfld) | ||
Theorem | cndrng 19775 | The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ DivRing | ||
Theorem | cnflddiv 19776 | 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 19777 | The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋)) | ||
Theorem | cnfldmulg 19778 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | cnfldexp 19779 | 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 19780 | The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ℂfld ∈ *-Ring | ||
Theorem | xrsmgm 19781 | The (additive group of the) extended reals is a magma. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ Mgm | ||
Theorem | xrsnsgrp 19782 | The (additive group of the) extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∉ SGrp | ||
Theorem | xrsmgmdifsgrp 19783 | The (additive group of the) extended reals is a magma, but not a semigroup, and therefore also no monoid and no group, in contrast to the multiplicative group, see xrsmcmn 19769. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ (Mgm ∖ SGrp) | ||
Theorem | xrs1mnd 19784 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form a monoid - in contrast to the full structure, see xrsmgmdifsgrp 19783. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | xrs10 19785 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | xrs1cmn 19786 | 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 19787 | 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 19788 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
Theorem | xrsds 19789* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
Theorem | xrsdsval 19790 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
Theorem | xrsdsreval 19791 | 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 19792 | Lemma for xrsdsreclb 19793. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | xrsdsreclb 19793 | 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 19794* | Lemma for nn0subm 19801 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 19795* | Lemma for resubdrg 19954 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 19796* | Lemma for resubdrg 19954 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubdrglem 19797* | Lemma for resubdrg 19954 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
Theorem | qsubdrg 19798 | 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 19799 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) | ||
Theorem | gzsubrg 19800 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |