HomeTheorem List (p. 446 of 502)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 446 of 502) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50158) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | k0004ss1 44501* | 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 44502* | 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 44503* | 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 44504* | 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 44505 | Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5)) | ||
| Theorem | wwlemuld 44506 | Natural deduction form of lemul2d 13005. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) & ⊢ (𝜑 → 0 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | leeq1d 44507 | Specialization of breq1d 5110 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐶) | ||
| Theorem | leeq2d 44508 | Specialization of breq2d 5112 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐷) | ||
| Theorem | absmulrposd 44509 | Specialization of absmuld with absidd 15358. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵))) | ||
| Theorem | imadisjld 44510 | Natural dduction form of one side of imadisj 6047. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅) | ||
| Theorem | wnefimgd 44511 | The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅) | ||
| Theorem | fco2d 44512 | Natural deduction form of fco2 6696. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
| Theorem | wfximgfd 44513 | The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴)) | ||
| Theorem | extoimad 44514* | 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 44515* | Lemma for imo72b2 44522. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
| Theorem | suprleubrd 44516* | Natural deduction form of specialized suprleub 12120. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵) | ||
| Theorem | imo72b2lem2 44517* | Lemma for imo72b2 44522. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶) ⇒ ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶) | ||
| Theorem | suprlubrd 44518* | Natural deduction form of specialized suprlub 12118. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧) ⇒ ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < )) | ||
| Theorem | imo72b2lem1 44519* | Lemma for imo72b2 44522. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
| Theorem | lemuldiv3d 44520 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) | ||
| Theorem | lemuldiv4d 44521 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) | ||
| Theorem | imo72b2 44522* | 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 11147 1red 11145 readdcld 11173 remulcld 11174 eqcomd 2743. | ||
| Theorem | int-addcomd 44523 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴)) | ||
| Theorem | int-addassocd 44524 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷)) | ||
| Theorem | int-addsimpd 44525 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 = (𝐴 − 𝐵)) | ||
| Theorem | int-mulcomd 44526 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴)) | ||
| Theorem | int-mulassocd 44527 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷)) | ||
| Theorem | int-mulsimpd 44528 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → 1 = (𝐴 / 𝐵)) | ||
| Theorem | int-leftdistd 44529 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴))) | ||
| Theorem | int-rightdistd 44530 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷))) | ||
| Theorem | int-sqdefd 44531 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2)) | ||
| Theorem | int-mul11d 44532 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐵) | ||
| Theorem | int-mul12d 44533 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐵) | ||
| Theorem | int-add01d 44534 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐵) | ||
| Theorem | int-add02d 44535 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐵) | ||
| Theorem | int-sqgeq0d 44536 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) | ||
| Theorem | int-eqprincd 44537 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷)) | ||
| Theorem | int-eqtransd 44538 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
| Theorem | int-eqmvtd 44539 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷)) | ||
| Theorem | int-eqineqd 44540 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
| Theorem | int-ineqmvtd 44541 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶) | ||
| Theorem | int-ineq1stprincd 44542 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶)) | ||
| Theorem | int-ineq2ndprincd 44543 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶)) | ||
| Theorem | int-ineqtransd 44544 | 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 12634 addcomli 11337 00id 11320 addridi 11332 addlidi 11333 eqid 2737 dec0h 12641 decadd 12673 decaddc 12674. | ||
| Theorem | unitadd 44545 | Theorem used in conjunction with decaddc 12674 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝐴 + 𝐵) = 𝐹 & ⊢ (𝐶 + 1) = 𝐵 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐶) + 1) = 𝐹 | ||
| Theorem | gsumws3 44546 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈))) | ||
| Theorem | gsumws4 44547 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉)))) | ||
| Theorem | amgm2d 44548 | Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 26968. (Contributed by Stanislas Polu, 8-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2)) | ||
| Theorem | amgm3d 44549 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
| Theorem | amgm4d 44550 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
| Theorem | spALT 44551 | sp 2191 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2191 instead. (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | elnelneqd 44552 | 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 44553 | 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 44554* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
| Theorem | rexlimdvaacbv 44555* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3140. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
| Theorem | rexlimddvcbvw 44556* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44555. The equivalent of this theorem without the bound variable change is rexlimddv 3145. Version of rexlimddvcbv 44557 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by GG, 2-Apr-2024.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | rexlimddvcbv 44557* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44555. The equivalent of this theorem without the bound variable change is rexlimddv 3145. Usage of this theorem is discouraged because it depends on ax-13 2377, see rexlimddvcbvw 44556 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | rr-elrnmpt3d 44558* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
| Theorem | rr-phpd 44559 | Equivalent of php 9143 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ω) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | tfindsd 44560* | Deduction associated with tfinds 7812. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → 𝜂) | ||
| Syntax | cmnring 44561 | Extend class notation with the monoid ring function. |
| class MndRing | ||
| Definition | df-mnring 44562* | 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 44563* | 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 44564 | 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 44565 | 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 44566 | The base set of a monoid ring. Converse of mnringbased 44565. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑉)) | ||
| Theorem | mnringelbased 44567 | 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 44568 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝐶 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐴⟶𝐶) | ||
| Theorem | mnringbasefsuppd 44569 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 finSupp 0 ) | ||
| Theorem | mnringaddgd 44570 | 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 44571 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹)) | ||
| Theorem | mnring0g2d 44572 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹)) | ||
| Theorem | mnringmulrd 44573* | 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 44574 | 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 44575 | 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 44576 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐹 ∈ LMod) | ||
| Theorem | mnringmulrvald 44577* | 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 44578 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ · = (.r‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
| Theorem | gru0eld 44579 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → ∅ ∈ 𝐺) | ||
| Theorem | grusucd 44580 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝐺) | ||
| Theorem | r1rankcld 44581 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅)) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅)) | ||
| Theorem | grur1cld 44582 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺) | ||
| Theorem | grurankcld 44583 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) | ||
| Theorem | grurankrcld 44584 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐺) | ||
| Syntax | cscott 44585 | Extend class notation with the Scott's trick operation. |
| class Scott 𝐴 | ||
| Definition | df-scott 44586* | Define the Scott operation. This operation constructs a subset of the input class which is nonempty whenever its input is using Scott's trick. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} | ||
| Theorem | scotteqd 44587 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵) | ||
| Theorem | scotteq 44588 | Closed form of scotteqd 44587. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵) | ||
| Theorem | nfscott 44589 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Scott 𝐴 | ||
| Theorem | scottabf 44590* | Value of the Scott operation at a class abstraction. Variant of scottab 44591 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottab 44591* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottabes 44592* | Value of the Scott operation at a class abstraction. Variant of scottab 44591 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottss 44593 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Scott 𝐴 ⊆ 𝐴 | ||
| Theorem | elscottab 44594* | An element of the output of the Scott operation applied to a class abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 ∈ Scott {𝑥 ∣ 𝜑} → 𝜓) | ||
| Theorem | scottex2 44595 | scottex 9809 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ Scott 𝐴 ∈ V | ||
| Theorem | scotteld 44596* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴) | ||
| Theorem | scottelrankd 44597 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) & ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶)) | ||
| Theorem | scottrankd 44598 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵)) | ||
| Theorem | gruscottcld 44599 | If a Grothendieck universe contains an element of a Scott's trick set, it contains the Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐵 ∈ 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → Scott 𝐴 ∈ 𝐺) | ||
| Syntax | ccoll 44600 | Extend class notation with the collection operation. |
| class (𝐹 Coll 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |