P. 202 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20101-20200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	evl1addd 20101	Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊)))
Theorem	evl1subd 20102	Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐷 = (-g‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊)))
Theorem	evl1muld 20103	Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊)))
Theorem	evl1vsd 20104	Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ ∙ = ( ·𝑠 ‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉)))
Theorem	evl1expd 20105	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 20106	Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄)
Theorem	pf1id 20107	The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄)
Theorem	pf1subrg 20108	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 20109	Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing)
Theorem	pf1f 20110	Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵)
Theorem	mpfpf1 20111*	Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = ran (1o eval 𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄)
Theorem	pf1mpf 20112*	Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = ran (1o eval 𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑𝑚 1o) ↦ (𝑥‘∅))) ∈ 𝐸)
Theorem	pf1addcl 20113	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘𝑓 + 𝐺) ∈ 𝑄)
Theorem	pf1mulcl 20114	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘𝑓 · 𝐺) ∈ 𝑄)
Theorem	pf1ind 20115*	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 20116*	Lemma for evl1gsumd 20117 (induction step). (Contributed by AV, 17-Sep-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))))
Theorem	evl1gsumd 20117*	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 20118*	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 20085. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝑃 = (𝑅 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evl1gsumaddval 20119*	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 20120*	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 20121	Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 20118, the proof is shorter using evls1varpw 20087 instead of proving it directly. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋)))
Theorem	evl1varpwval 20122	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 20123	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 20124	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 20125*	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 (𝑥 ∈ 𝑀 ↦ (𝐴 · (𝑁𝐸𝐶)))))
10.11  The complex numbers as an algebraic extensible structure
10.11.1  Definition and basic properties
Syntax	cpsmet 20126	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 20127	Extend class notation with the class of all extended metric spaces.
class ∞Met
Syntax	cmet 20128	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 20129	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 20130	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 20131	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 20132	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 20133	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 20134*	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 20135*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 20136, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Definition	df-met 20136*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22534. 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 22556, metgt0 22572, metsym 22563, and mettri 22565. (Contributed by NM, 25-Aug-2006.)
⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
Definition	df-bl 20137*	Define the metric space ball function. See blval 22599 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 20138	Define a function whose value is the family of open sets of a metric space. See elmopn 22655 for its main property. (Contributed by NM, 1-Sep-2006.)
⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
Definition	df-fbas 20139*	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 20140*	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 20141*	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 20142	Extend class notation with the field of complex numbers.
class ℂfld
Definition	df-cnfld 20143	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 20145, cnfldadd 20147, cnfldmul 20148, cnfldcj 20149, cnfldtset 20150, cnfldle 20151, cnfldds 20152, and cnfldbas 20146. 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 20144	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 20145	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 20146	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 20147	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 20148	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 20149	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 20150	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 20151	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 20152	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 20153	The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ (metUnif‘(abs ∘ − )) = (UnifSet‘ℂfld)
Theorem	cnfldfun 20154	The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021.)
⊢ Fun ℂfld
Theorem	cnfldfunALT 20155	Alternate proof of cnfldfun 20154 (much shorter proof, using cnfldstr 20144 and structn0fun 16267: 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 20156	The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 Struct ⟨1, ;12⟩
Theorem	xrsex 20157	The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ V
Theorem	xrsbas 20158	The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ* = (Base‘ℝ*𝑠)
Theorem	xrsadd 20159	The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 = (+g‘ℝ*𝑠)
Theorem	xrsmul 20160	The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e = (.r‘ℝ*𝑠)
Theorem	xrstset 20161	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
Theorem	xrsle 20162	The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ≤ = (le‘ℝ*𝑠)
Theorem	cncrng 20163	The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.)
⊢ ℂfld ∈ CRing
Theorem	cnring 20164	The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ Ring
Theorem	xrsmcmn 20165	The "multiplicative group" of the extended reals is a commutative monoid (even though the "additive group" is not a semigroup, see xrsmgmdifsgrp 20179.) (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (mulGrp‘ℝ*𝑠) ∈ CMnd
Theorem	cnfld0 20166	Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 0 = (0g‘ℂfld)
Theorem	cnfld1 20167	One is the unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 1 = (1r‘ℂfld)
Theorem	cnfldneg 20168	The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋)
Theorem	cnfldplusf 20169	The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ + = (+𝑓‘ℂfld)
Theorem	cnfldsub 20170	The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘ℂfld)
Theorem	cndrng 20171	The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ ℂfld ∈ DivRing
Theorem	cnflddiv 20172	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 20173	The multiplicative inverse in the field of complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → ((invr‘ℂfld)‘𝑋) = (1 / 𝑋))
Theorem	cnfldmulg 20174	The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵))
Theorem	cnfldexp 20175	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 20176	The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ ℂfld ∈ *-Ring
Theorem	xrsmgm 20177	The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ Mgm
Theorem	xrsnsgrp 20178	The "additive group" of the extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∉ SGrp
Theorem	xrsmgmdifsgrp 20179	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 20165. (Contributed by AV, 30-Jan-2020.)
⊢ ℝ*𝑠 ∈ (Mgm ∖ SGrp)
Theorem	xrs1mnd 20180	The extended real numbers, restricted to ℝ* ∖ {-∞}, form an additive monoid - in contrast to the full structure, see xrsmgmdifsgrp 20179. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 𝑅 ∈ Mnd
Theorem	xrs10 20181	The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    ⇒   ⊢ 0 = (0g‘𝑅)
Theorem	xrs1cmn 20182	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 20183	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 20184	The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
Theorem	xrsds 20185*	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
Theorem	xrsdsval 20186	The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵)))
Theorem	xrsdsreval 20187	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 20188	Lemma for xrsdsreclb 20189. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐷 = (dist‘ℝ*𝑠)    ⇒   ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
Theorem	xrsdsreclb 20189	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 20190*	Lemma for nn0subm 20197 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ 0 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubMnd‘ℂfld)
Theorem	cnsubglem 20191*	Lemma for resubdrg 20351 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 𝐵 ∈ 𝐴    ⇒   ⊢ 𝐴 ∈ (SubGrp‘ℂfld)
Theorem	cnsubrglem 20192*	Lemma for resubdrg 20351 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    ⇒   ⊢ 𝐴 ∈ (SubRing‘ℂfld)
Theorem	cnsubdrglem 20193*	Lemma for resubdrg 20351 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴)    &   ⊢ 1 ∈ 𝐴    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴)    ⇒   ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing)
Theorem	qsubdrg 20194	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 20195	The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ ∈ (SubRing‘ℂfld)
Theorem	gzsubrg 20196	The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.)
⊢ ℤ[i] ∈ (SubRing‘ℂfld)
Theorem	nn0subm 20197	The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ ℕ0 ∈ (SubMnd‘ℂfld)
Theorem	rege0subm 20198	The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
Theorem	absabv 20199	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 20200	The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅)