P. 448 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44701-44800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	neicvgrcomplex 44701	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	neicvgf1o 44702*	If neighborhood and convergent functions are related by operator 𝐻, it is a one-to-one onto relation. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝐻:(𝒫 𝒫 𝐵 ↑m 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgnvo 44703*	If neighborhood and convergent functions are related by operator 𝐻, it is its own converse function. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → ◡𝐻 = 𝐻)
Theorem	neicvgnvor 44704*	If neighborhood and convergent functions are related by operator 𝐻, the relationship holds with the functions swapped. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝑀𝐻𝑁)
Theorem	neicvgmex 44705*	If the neighborhoods and convergents functions are related, the convergents function exists. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgnex 44706*	If the neighborhoods and convergents functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgel1 44707*	A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋)))
Theorem	neicvgel2 44708*	The complement of a subset being an element of a neighborhood at a point is equivalent to that subset not being a element of the convergent at that point. (Contributed by RP, 12-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋) ↔ ¬ 𝑆 ∈ (𝑀‘𝑋)))
Theorem	neicvgfv 44709*	The value of the neighborhoods (convergents) in terms of the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)})
Theorem	ntrrn 44710	The range of the interior function of a topology a subset of the open sets of the topology. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → ran 𝐼 ⊆ 𝐽)
Theorem	ntrf 44711	The interior function of a topology is a map from the powerset of the base set to the open sets of the topology. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼:𝒫 𝑋⟶𝐽)
Theorem	ntrf2 44712	The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼:𝒫 𝑋⟶𝒫 𝑋)
Theorem	ntrelmap 44713	The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ (𝒫 𝑋 ↑m 𝒫 𝑋))
Theorem	clsf2 44714	The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 23166. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)
Theorem	clselmap 44715	The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾 ∈ (𝒫 𝑋 ↑m 𝒫 𝑋))
Theorem	dssmapntrcls 44716*	The interior and closure operators on a topology are duals of each other. See also kur14lem2 35570. (Contributed by RP, 21-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾))
Theorem	dssmapclsntr 44717*	The closure and interior operators on a topology are duals of each other. See also kur14lem2 35570. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾 = (𝐷‘𝐼))
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 23117 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems.
Theorem	gneispa 44718*	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 44719*	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 44720*	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 44721*	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 44722*	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 44723*	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 44724*	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 44725*	A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹)
Theorem	gneispacern 44726*	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 44727*	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 44728*	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 44729*	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 44730*	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 44731*	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 44732*	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 44733*	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 44734*	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 44735	Application of ssin 4193 to range of a function. (Contributed by RP, 1-Apr-2021.)
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷))
Theorem	k0004lem2 44736	A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶 ↑m 𝐴)))
Theorem	k0004lem3 44737	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 44738*	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 44739*	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 44740*	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 44741*	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 44742*	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 44743	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 44744	Natural deduction form of lemul2d 13095. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	leeq1d 44745	Specialization of breq1d 5115 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐶)
Theorem	leeq2d 44746	Specialization of breq2d 5117 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐷)
Theorem	absmulrposd 44747	Specialization of absmuld with absidd 15464. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵)))
Theorem	imadisjld 44748	Natural dduction form of one side of imadisj 6073. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅)
Theorem	wnefimgd 44749	The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅)
Theorem	fco2d 44750	Natural deduction form of fco2 6722. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	wfximgfd 44751	The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴))
Theorem	extoimad 44752*	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 44753*	Lemma for imo72b2 44760. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵))))    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	suprleubrd 44754*	Natural deduction form of specialized suprleub 12172. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵)
Theorem	imo72b2lem2 44755*	Lemma for imo72b2 44760. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶)    ⇒   ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶)
Theorem	suprlubrd 44756*	Natural deduction form of specialized suprlub 12170. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧)    ⇒   ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < ))
Theorem	imo72b2lem1 44757*	Lemma for imo72b2 44760. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	lemuldiv3d 44758	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴))
Theorem	lemuldiv4d 44759	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴))    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶)
Theorem	imo72b2 44760*	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 11199 1red 11197 readdcld 11226 remulcld 11227 eqcomd 2771.
Theorem	int-addcomd 44761	AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴))
Theorem	int-addassocd 44762	AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷))
Theorem	int-addsimpd 44763	AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 = (𝐴 − 𝐵))
Theorem	int-mulcomd 44764	MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴))
Theorem	int-mulassocd 44765	MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷))
Theorem	int-mulsimpd 44766	MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → 1 = (𝐴 / 𝐵))
Theorem	int-leftdistd 44767	AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴)))
Theorem	int-rightdistd 44768	AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷)))
Theorem	int-sqdefd 44769	SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2))
Theorem	int-mul11d 44770	First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐵)
Theorem	int-mul12d 44771	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐵)
Theorem	int-add01d 44772	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 + 0) = 𝐵)
Theorem	int-add02d 44773	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (0 + 𝐴) = 𝐵)
Theorem	int-sqgeq0d 44774	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	int-eqprincd 44775	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷))
Theorem	int-eqtransd 44776	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	int-eqmvtd 44777	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷))
Theorem	int-eqineqd 44778	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐴)
Theorem	int-ineqmvtd 44779	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶)
Theorem	int-ineq1stprincd 44780	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶))
Theorem	int-ineq2ndprincd 44781	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶))
Theorem	int-ineqtransd 44782	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 12717 addcomli 11390 00id 11373 addridi 11385 addlidi 11386 eqid 2765 dec0h 12729 decadd 12761 decaddc 12762.
Theorem	unitadd 44783	Theorem used in conjunction with decaddc 12762 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 44784	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈)))
Theorem	gsumws4 44785	Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉))))
Theorem	amgm2d 44786	Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 27112. (Contributed by Stanislas Polu, 8-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2))
Theorem	amgm3d 44787	Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3))
Theorem	amgm4d 44788	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 44789	sp 2221 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2221 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	elnelneqd 44790	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 44791	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 44792*	Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	rexlimdvaacbv 44793*	Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3167. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddvcbvw 44794*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44793. The equivalent of this theorem without the bound variable change is rexlimddv 3172. Version of rexlimddvcbv 44795 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by GG, 2-Apr-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rexlimddvcbv 44795*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44793. The equivalent of this theorem without the bound variable change is rexlimddv 3172. Usage of this theorem is discouraged because it depends on ax-13 2406, see rexlimddvcbvw 44794 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rr-elrnmpt3d 44796*	Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ran 𝐹)
Theorem	rr-phpd 44797	Equivalent of php 9179 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ω)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	tfindsd 44798*	Deduction associated with tfinds 7844. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → 𝜂)
21.38.2  Monoid rings
Syntax	cmnring 44799	Extend class notation with the monoid ring function.
class MndRing
Definition	df-mnring 44800*	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‘𝑟))))))⟩))