![]() |
Metamath
Proof Explorer Theorem List (p. 425 of 473) | < 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: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gneispacern2 42401* | 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 42402* | 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 42403* | 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 42404* | 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 42405* | 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 42406* | 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 42407* | 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 42408* | 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 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃)) | ||
See https://kerodon.net/ for a work in progress by Jacob Lurie. | ||
See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension 𝑁. | ||
Theorem | k0004lem1 42409 | Application of ssin 4190 to range of a function. (Contributed by RP, 1-Apr-2021.) |
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷)) | ||
Theorem | k0004lem2 42410 | A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶 ↑m 𝐴))) | ||
Theorem | k0004lem3 42411 | 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 42412* | 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 42413* | 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 42414* | 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 42415* | 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 42416* | 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〉}} | ||
Theorem | inductionexd 42417 | Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5)) | ||
Theorem | wwlemuld 42418 | Natural deduction form of lemul2d 13001. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) & ⊢ (𝜑 → 0 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | leeq1d 42419 | Specialization of breq1d 5115 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐶) | ||
Theorem | leeq2d 42420 | Specialization of breq2d 5117 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐷) | ||
Theorem | absmulrposd 42421 | Specialization of absmuld with absidd 15307. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵))) | ||
Theorem | imadisjld 42422 | Natural dduction form of one side of imadisj 6032. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅) | ||
Theorem | imadisjlnd 42423 | Natural deduction form of one negated side of imadisj 6032. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) ≠ ∅) | ||
Theorem | wnefimgd 42424 | The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅) | ||
Theorem | fco2d 42425 | Natural deduction form of fco2 6695. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
Theorem | wfximgfd 42426 | The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴)) | ||
Theorem | extoimad 42427* | 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 42428* | Lemma for imo72b2 42435. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
Theorem | suprleubrd 42429* | Natural deduction form of specialized suprleub 12121. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵) | ||
Theorem | imo72b2lem2 42430* | Lemma for imo72b2 42435. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶) ⇒ ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶) | ||
Theorem | suprlubrd 42431* | Natural deduction form of specialized suprlub 12119. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧) ⇒ ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < )) | ||
Theorem | imo72b2lem1 42432* | Lemma for imo72b2 42435. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
Theorem | lemuldiv3d 42433 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) | ||
Theorem | lemuldiv4d 42434 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) | ||
Theorem | imo72b2 42435* | IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢 − 𝑣))) = (2 · ((𝐹‘𝑢) · (𝐺‘𝑣)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) ⇒ ⊢ (𝜑 → (abs‘(𝐺‘𝐵)) ≤ 1) | ||
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 11158 1red 11156 readdcld 11184 remulcld 11185 eqcomd 2742. | ||
Theorem | int-addcomd 42436 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴)) | ||
Theorem | int-addassocd 42437 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷)) | ||
Theorem | int-addsimpd 42438 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 = (𝐴 − 𝐵)) | ||
Theorem | int-mulcomd 42439 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴)) | ||
Theorem | int-mulassocd 42440 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷)) | ||
Theorem | int-mulsimpd 42441 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → 1 = (𝐴 / 𝐵)) | ||
Theorem | int-leftdistd 42442 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴))) | ||
Theorem | int-rightdistd 42443 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷))) | ||
Theorem | int-sqdefd 42444 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2)) | ||
Theorem | int-mul11d 42445 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐵) | ||
Theorem | int-mul12d 42446 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐵) | ||
Theorem | int-add01d 42447 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐵) | ||
Theorem | int-add02d 42448 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐵) | ||
Theorem | int-sqgeq0d 42449 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | int-eqprincd 42450 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷)) | ||
Theorem | int-eqtransd 42451 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | int-eqmvtd 42452 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷)) | ||
Theorem | int-eqineqd 42453 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
Theorem | int-ineqmvtd 42454 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶) | ||
Theorem | int-ineq1stprincd 42455 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶)) | ||
Theorem | int-ineq2ndprincd 42456 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶)) | ||
Theorem | int-ineqtransd 42457 | InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≤ 𝐴) | ||
This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12633 addcomli 11347 00id 11330 addid1i 11342 addid2i 11343 eqid 2736 dec0h 12640 decadd 12672 decaddc 12673. | ||
Theorem | unitadd 42458 | Theorem used in conjunction with decaddc 12673 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝐴 + 𝐵) = 𝐹 & ⊢ (𝐶 + 1) = 𝐵 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐶) + 1) = 𝐹 | ||
Theorem | gsumws3 42459 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg 〈“𝑆𝑇𝑈”〉) = (𝑆 + (𝑇 + 𝑈))) | ||
Theorem | gsumws4 42460 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg 〈“𝑆𝑇𝑈𝑉”〉) = (𝑆 + (𝑇 + (𝑈 + 𝑉)))) | ||
Theorem | amgm2d 42461 | Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 26339. (Contributed by Stanislas Polu, 8-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2)) | ||
Theorem | amgm3d 42462 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
Theorem | amgm4d 42463 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
Theorem | spALT 42464 | sp 2176 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2176 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | elnelneqd 42465 | 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 42466 | 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 42467* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | rexlimdvaacbv 42468* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3153. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimddvcbvw 42469* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42468. The equivalent of this theorem without the bound variable change is rexlimddv 3158. Version of rexlimddvcbv 42470 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | rexlimddvcbv 42470* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42468. The equivalent of this theorem without the bound variable change is rexlimddv 3158. Usage of this theorem is discouraged because it depends on ax-13 2370, see rexlimddvcbvw 42469 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | rr-elrnmpt3d 42471* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
Theorem | finnzfsuppd 42472* | If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍)) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | rr-phpd 42473 | Equivalent of php 9154 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ω) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | suceqd 42474 | Deduction associated with suceq 6383. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → suc 𝐴 = suc 𝐵) | ||
Theorem | tfindsd 42475* | Deduction associated with tfinds 7796. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → 𝜂) | ||
Syntax | cmnring 42476 | Extend class notation with the monoid ring function. |
class MndRing | ||
Definition | df-mnring 42477* | 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 42478* | 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 42479 | 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 | mnringnmulrdOLD 42480 | Obsolete version of mnringnmulrd 42479 as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ (.r‘ndx) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐸‘𝑉) = (𝐸‘𝐹)) | ||
Theorem | mnringbased 42481 | 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 | mnringbasedOLD 42482 | Obsolete version of mnringnmulrd 42479 as of 1-Nov-2024. The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐹)) | ||
Theorem | mnringbaserd 42483 | The base set of a monoid ring. Converse of mnringbased 42481. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑉)) | ||
Theorem | mnringelbased 42484 | 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 42485 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝐶 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐴⟶𝐶) | ||
Theorem | mnringbasefsuppd 42486 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 finSupp 0 ) | ||
Theorem | mnringaddgd 42487 | 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 | mnringaddgdOLD 42488 | Obsolete version of mnringaddgd 42487 as of 1-Nov-2024. The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (+g‘𝑉) = (+g‘𝐹)) | ||
Theorem | mnring0gd 42489 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹)) | ||
Theorem | mnring0g2d 42490 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹)) | ||
Theorem | mnringmulrd 42491* | 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 42492 | The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) | ||
Theorem | mnringscadOLD 42493 | Obsolete version of mnringscad 42492 as of 1-Nov-2024. The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) | ||
Theorem | mnringvscad 42494 | 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 | mnringvscadOLD 42495 | Obsolete version of mnringvscad 42494 as of 1-Nov-2024. The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ·𝑠 ‘𝑉) = ( ·𝑠 ‘𝐹)) | ||
Theorem | mnringlmodd 42496 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐹 ∈ LMod) | ||
Theorem | mnringmulrvald 42497* | 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 42498 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ · = (.r‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | gru0eld 42499 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → ∅ ∈ 𝐺) | ||
Theorem | grusucd 42500 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝐺) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |