P. 442 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44101-44200   *Has distinct variable group(s)

Type	Label	Description
Statement
21.36.7.3  Generic Neighborhood Spaces Any neighborhood space is an open set topology and any open set topology is a neighborhood space. Seifert and Threlfall define a generic neighborhood space which is a superset of what is now generally used and related concepts and the following will show that those definitions apply to elements of Top. Seifert and Threlfall do not allow neighborhood spaces on the empty set while sn0top 22935 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems.
Theorem	gneispa 44101*	Each point 𝑝 of the neighborhood space has at least one neighborhood; each neighborhood of 𝑝 contains 𝑝. Axiom A of Seifert and Threlfall. (Contributed by RP, 5-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ∀𝑝 ∈ 𝑋 (((nei‘𝐽)‘{𝑝}) ≠ ∅ ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑝})𝑝 ∈ 𝑛))
Theorem	gneispb 44102*	Given a neighborhood 𝑁 of 𝑃, each subset of the neighborhood space containing this neighborhood is also a neighborhood of 𝑃. Axiom B of Seifert and Threlfall. (Contributed by RP, 5-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∀𝑠 ∈ 𝒫 𝑋(𝑁 ⊆ 𝑠 → 𝑠 ∈ ((nei‘𝐽)‘{𝑃})))
Theorem	gneispace2 44103*	The predicate that 𝐹 is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
Theorem	gneispace3 44104*	The predicate that 𝐹 is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
Theorem	gneispace 44105*	The predicate that 𝐹 is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))))
Theorem	gneispacef 44106*	A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
Theorem	gneispacef2 44107*	A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:dom 𝐹⟶𝒫 𝒫 dom 𝐹)
Theorem	gneispacefun 44108*	A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹)
Theorem	gneispacern 44109*	A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
Theorem	gneispacern2 44110*	A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
Theorem	gneispace0nelrn 44111*	A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)
Theorem	gneispace0nelrn2 44112*	A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹) → (𝐹‘𝑃) ≠ ∅)
Theorem	gneispace0nelrn3 44113*	A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ¬ ∅ ∈ ran 𝐹)
Theorem	gneispaceel 44114*	Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)𝑝 ∈ 𝑛)
Theorem	gneispaceel2 44115*	Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹 ∧ 𝑁 ∈ (𝐹‘𝑃)) → 𝑃 ∈ 𝑁)
Theorem	gneispacess 44116*	All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))
Theorem	gneispacess2 44117*	All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹) ∧ (𝑁 ∈ (𝐹‘𝑃) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃))
21.36.8  Exploring Higher Homotopy via Kerodon See https://kerodon.net/ for a work in progress by Jacob Lurie.
21.36.8.1  Simplicial Sets See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension 𝑁.
Theorem	k0004lem1 44118	Application of ssin 4214 to range of a function. (Contributed by RP, 1-Apr-2021.)
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷))
Theorem	k0004lem2 44119	A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶 ↑m 𝐴)))
Theorem	k0004lem3 44120	When the value of a mapping on a singleton is known, the mapping is a completely known singleton. (Contributed by RP, 2-Apr-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ 𝐹 = {⟨𝐴, 𝐶⟩}))
Theorem	k0004val 44121*	The topological simplex of dimension 𝑁 is the set of real vectors where the components are nonnegative and sum to 1. (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) = {𝑡 ∈ ((0[,]1) ↑m (1...(𝑁 + 1))) ∣ Σ𝑘 ∈ (1...(𝑁 + 1))(𝑡‘𝑘) = 1})
Theorem	k0004ss1 44122*	The topological simplex of dimension 𝑁 is a subset of the real vectors of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (ℝ ↑m (1...(𝑁 + 1))))
Theorem	k0004ss2 44123*	The topological simplex of dimension 𝑁 is a subset of the base set of a real vector space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(ℝ^‘(1...(𝑁 + 1)))))
Theorem	k0004ss3 44124*	The topological simplex of dimension 𝑁 is a subset of the base set of Euclidean space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(𝔼hil‘(𝑁 + 1))))
Theorem	k0004val0 44125*	The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝐴‘0) = {{⟨1, 1⟩}}
21.37  Mathbox for Stanislas Polu
Theorem	inductionexd 44126	Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5))
21.37.1  IMO Problems
21.37.1.1  IMO 1972 B2
Theorem	wwlemuld 44127	Natural deduction form of lemul2d 13093. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	leeq1d 44128	Specialization of breq1d 5129 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐶)
Theorem	leeq2d 44129	Specialization of breq2d 5131 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐷)
Theorem	absmulrposd 44130	Specialization of absmuld with absidd 15439. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵)))
Theorem	imadisjld 44131	Natural dduction form of one side of imadisj 6067. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅)
Theorem	wnefimgd 44132	The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅)
Theorem	fco2d 44133	Natural deduction form of fco2 6731. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	wfximgfd 44134	The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴))
Theorem	extoimad 44135*	If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 𝐶)
Theorem	imo72b2lem0 44136*	Lemma for imo72b2 44143. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵))))    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	suprleubrd 44137*	Natural deduction form of specialized suprleub 12206. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵)
Theorem	imo72b2lem2 44138*	Lemma for imo72b2 44143. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶)    ⇒   ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶)
Theorem	suprlubrd 44139*	Natural deduction form of specialized suprlub 12204. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧)    ⇒   ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < ))
Theorem	imo72b2lem1 44140*	Lemma for imo72b2 44143. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	lemuldiv3d 44141	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴))
Theorem	lemuldiv4d 44142	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴))    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)
Theorem	imo72b2 44143*	IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢 − 𝑣))) = (2 · ((𝐹‘𝑢) · (𝐺‘𝑣))))    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0)    ⇒   ⊢ (𝜑 → (abs‘(𝐺‘𝐵)) ≤ 1)
21.37.2  INT Inequalities Proof Generator This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 11236 1red 11234 readdcld 11262 remulcld 11263 eqcomd 2741.
Theorem	int-addcomd 44144	AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴))
Theorem	int-addassocd 44145	AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷))
Theorem	int-addsimpd 44146	AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 = (𝐴 − 𝐵))
Theorem	int-mulcomd 44147	MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴))
Theorem	int-mulassocd 44148	MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷))
Theorem	int-mulsimpd 44149	MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → 1 = (𝐴 / 𝐵))
Theorem	int-leftdistd 44150	AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴)))
Theorem	int-rightdistd 44151	AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷)))
Theorem	int-sqdefd 44152	SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2))
Theorem	int-mul11d 44153	First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐵)
Theorem	int-mul12d 44154	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐵)
Theorem	int-add01d 44155	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 + 0) = 𝐵)
Theorem	int-add02d 44156	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (0 + 𝐴) = 𝐵)
Theorem	int-sqgeq0d 44157	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	int-eqprincd 44158	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷))
Theorem	int-eqtransd 44159	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	int-eqmvtd 44160	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷))
Theorem	int-eqineqd 44161	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐴)
Theorem	int-ineqmvtd 44162	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶)
Theorem	int-ineq1stprincd 44163	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶))
Theorem	int-ineq2ndprincd 44164	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶))
Theorem	int-ineqtransd 44165	InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐴)
21.37.3  N-Digit Addition Proof Generator This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12721 addcomli 11425 00id 11408 addridi 11420 addlidi 11421 eqid 2735 dec0h 12728 decadd 12760 decaddc 12761.
Theorem	unitadd 44166	Theorem used in conjunction with decaddc 12761 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝐴 + 𝐵) = 𝐹    &   ⊢ (𝐶 + 1) = 𝐵    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ ((𝐴 + 𝐶) + 1) = 𝐹
21.37.4  AM-GM (for k = 2,3,4)
Theorem	gsumws3 44167	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈)))
Theorem	gsumws4 44168	Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉))))
Theorem	amgm2d 44169	Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 26950. (Contributed by Stanislas Polu, 8-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2))
Theorem	amgm3d 44170	Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3))
Theorem	amgm4d 44171	Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4))
21.38  Mathbox for Rohan Ridenour
21.38.1  Misc
Theorem	spALT 44172	sp 2183 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2183 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	elnelneqd 44173	Two classes are not equal if there is an element of one which is not an element of the other. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	elnelneq2d 44174	Two classes are not equal if one but not the other is an element of a given class. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	rr-spce 44175*	Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	rexlimdvaacbv 44176*	Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3142. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddvcbvw 44177*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44176. The equivalent of this theorem without the bound variable change is rexlimddv 3147. Version of rexlimddvcbv 44178 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by GG, 2-Apr-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rexlimddvcbv 44178*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44176. The equivalent of this theorem without the bound variable change is rexlimddv 3147. Usage of this theorem is discouraged because it depends on ax-13 2376, see rexlimddvcbvw 44177 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rr-elrnmpt3d 44179*	Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ran 𝐹)
Theorem	rr-phpd 44180	Equivalent of php 9219 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ω)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	suceqd 44181	Deduction associated with suceq 6419. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → suc 𝐴 = suc 𝐵)
Theorem	tfindsd 44182*	Deduction associated with tfinds 7853. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → 𝜂)
21.38.2  Monoid rings
Syntax	cmnring 44183	Extend class notation with the monoid ring function.
class MndRing
Definition	df-mnring 44184*	Define the monoid ring function. This takes a monoid 𝑀 and a ring 𝑅 and produces a free left module over 𝑅 with a product extending the monoid function on 𝑀. (Contributed by Rohan Ridenour, 13-May-2024.)
⊢ MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩))
Theorem	mnringvald 44185*	Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑉 sSet ⟨(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))⟩))
Theorem	mnringnmulrd 44186	Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (Revised by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (.r‘ndx)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐸‘𝑉) = (𝐸‘𝐹))
Theorem	mnringbased 44187	The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
Theorem	mnringbaserd 44188	The base set of a monoid ring. Converse of mnringbased 44187. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑉))
Theorem	mnringelbased 44189	Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (𝐶 ↑m 𝐴) ∧ 𝑋 finSupp 0 )))
Theorem	mnringbasefd 44190	Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐴⟶𝐶)
Theorem	mnringbasefsuppd 44191	Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 finSupp 0 )
Theorem	mnringaddgd 44192	The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (+g‘𝑉) = (+g‘𝐹))
Theorem	mnring0gd 44193	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹))
Theorem	mnring0g2d 44194	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹))
Theorem	mnringmulrd 44195*	The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) = (.r‘𝐹))
Theorem	mnringscad 44196	The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹))
Theorem	mnringvscad 44197	The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ·𝑠 ‘𝑉) = ( ·𝑠 ‘𝐹))
Theorem	mnringlmodd 44198	Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LMod)
Theorem	mnringmulrvald 44199*	Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ ∙ = (.r‘𝑅)    &   ⊢ 𝟎 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ · = (.r‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑋‘𝑎) ∙ (𝑌‘𝑏)), 𝟎 )))))
Theorem	mnringmulrcld 44200	Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ · = (.r‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)