Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs 		 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100
Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 20-Sep-2025 at 6:50 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
16-Sep-2025opabfi 6992 Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐵 ∈ Fin)    &   (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 DECID 𝜓)    ⇒   (𝜑 → 𝑆 ∈ Fin)
 
13-Sep-2025uchoice 6190 Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7267 (with the key difference being the change of ∃ to ∃!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑))
 
11-Sep-2025expghmap 14095 Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.)
𝑀 = (mulGrp‘ℂfld)    &   𝑈 = (𝑀 ↾s {𝑧 ∈ ℂ ∣ 𝑧 # 0})    ⇒   ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈))
 
11-Sep-2025cnfldui 14077 The invertible complex numbers are exactly those apart from zero. This is recapb 8690 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
{𝑧 ∈ ℂ ∣ 𝑧 # 0} = (Unit‘ℂfld)
 
9-Sep-2025gsumfzfsumlemm 14075 Lemma for gsumfzfsum 14076. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.)
(𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐵 ∈ ℂ)    ⇒   (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
 
9-Sep-2025gsumfzfsumlem0 14074 Lemma for gsumfzfsum 14076. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝑁 < 𝑀)    ⇒   (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
 
9-Sep-2025gsumfzmhm2 13414 Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐻 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ (𝐺 MndHom 𝐻))    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑋 ∈ 𝐵)    &   (𝑥 = 𝑋 → 𝐶 = 𝐷)    &   (𝑥 = (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝑋)) → 𝐶 = 𝐸)    ⇒   (𝜑 → (𝐻 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐷)) = 𝐸)
 
8-Sep-2025gsumfzmhm 13413 Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐻 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻))    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐻 Σg (𝐾 ∘ 𝐹)) = (𝐾‘(𝐺 Σg 𝐹)))
 
6-Sep-2025gsumfzconst 13411 Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
𝐵 = (Base‘𝐺)    &    · = (.g‘𝐺)    ⇒   ((𝐺 ∈ Mnd ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝑋)) = (((𝑁 − 𝑀) + 1) · 𝑋))
 
31-Aug-2025gsumfzmptfidmadd 13409 The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) (Revised by Jim Kingdon, 31-Aug-2025.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐶 ∈ 𝐵)    &   ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐷 ∈ 𝐵)    &   𝐹 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐶)    &   𝐻 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐷)    ⇒   (𝜑 → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
 
30-Aug-2025gsumfzsubmcl 13408 Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.)
(𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝑆)    ⇒   (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆)
 
30-Aug-2025seqm1g 10545 Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 30-Aug-2025.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   (𝜑 → + ∈ 𝑉)    &   (𝜑 → 𝐹 ∈ 𝑊)    ⇒   (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁)))
 
29-Aug-2025seqf1og 10592 Rearrange a sum via an arbitrary bijection on (𝑀...𝑁). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 29-Aug-2025.)
((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   (𝜑 → 𝐶 ⊆ 𝑆)    &   (𝜑 → + ∈ 𝑉)    &   (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))    &   ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝐶)    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐺‘(𝐹‘𝑘)))    &   (𝜑 → 𝐺 ∈ 𝑊)    &   (𝜑 → 𝐻 ∈ 𝑋)    ⇒   (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
 
25-Aug-2025irrmulap 9713 The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 9712. (Contributed by Jim Kingdon, 25-Aug-2025.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → ∀𝑞 ∈ ℚ 𝐴 # 𝑞)    &   (𝜑 → 𝐵 ∈ ℚ)    &   (𝜑 → 𝐵 ≠ 0)    &   (𝜑 → 𝑄 ∈ ℚ)    ⇒   (𝜑 → (𝐴 · 𝐵) # 𝑄)
 
19-Aug-2025seqp1g 10537 Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐹 ∈ 𝑉 ∧ + ∈ 𝑊) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
 
19-Aug-2025seq1g 10534 Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ∧ + ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
 
18-Aug-2025iswrdiz 10921 A zero-based sequence is a word. In iswrdinn0 10919 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)
((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℤ) → 𝑊 ∈ Word 𝑆)
 
16-Aug-2025gsumfzcl 13071 Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
 
16-Aug-2025iswrdinn0 10919 A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)
((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℕ0) → 𝑊 ∈ Word 𝑆)
 
15-Aug-2025gsumfzz 13067 Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.)
0 = (0g‘𝐺)    ⇒   ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = 0 )
 
14-Aug-2025gsumfzval 12974 An expression for Σg when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ 𝑉)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)))
 
13-Aug-2025znidom 14145 The ℤ/nℤ structure is an integral domain when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
𝑌 = (ℤ/nℤ‘𝑁)    ⇒   (𝑁 ∈ ℙ → 𝑌 ∈ IDomn)
 
12-Aug-2025rrgmex 13757 A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
𝐸 = (RLReg‘𝑅)    ⇒   (𝐴 ∈ 𝐸 → 𝑅 ∈ V)
 
10-Aug-2025gausslemma2dlem1cl 15175 Lemma for gausslemma2dlem1 15177. Closure of the body of the definition of 𝑅. (Contributed by Jim Kingdon, 10-Aug-2025.)
(𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   (𝜑 → 𝐴 ∈ (1...𝐻))    ⇒   (𝜑 → if((𝐴 · 2) < (𝑃 / 2), (𝐴 · 2), (𝑃 − (𝐴 · 2))) ∈ ℤ)
 
9-Aug-2025gausslemma2dlem1f1o 15176 Lemma for gausslemma2dlem1 15177. (Contributed by Jim Kingdon, 9-Aug-2025.)
(𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   (𝜑 → 𝑅:(1...𝐻)–1-1-onto→(1...𝐻))
 
7-Aug-2025qdclt 10315 Rational < is decidable. (Contributed by Jim Kingdon, 7-Aug-2025.)
((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → DECID 𝐴 < 𝐵)
 
22-Jul-2025ivthdich 14807 The intermediate value theorem implies real number dichotomy. Because real number dichotomy (also known as analytic LLPO) is a constructive taboo, this means we will be unable to prove the intermediate value theorem as stated here (although versions with additional conditions, such as ivthinc 14797 for strictly monotonic functions, can be proved).

The proof is via a function which we call the hover function and which is also described in Section 5.1 of [Bauer], p. 493. Consider any real number 𝑧. We want to show that 𝑧 ≤ 0 ∨ 0 ≤ 𝑧. Because of hovercncf 14800, hovera 14801, and hoverb 14802, we are able to apply the intermediate value theorem to get a value 𝑐 such that the hover function at 𝑐 equals 𝑧. By axltwlin 8087, 𝑐 < 1 or 0 < 𝑐, and that leads to 𝑧 ≤ 0 by hoverlt1 14803 or 0 ≤ 𝑧 by hovergt0 14804. (Contributed by Jim Kingdon and Mario Carneiro, 22-Jul-2025.)

(∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))) → ∀𝑟 ∈ ℝ ∀𝑠 ∈ ℝ (𝑟 ≤ 𝑠 ∨ 𝑠 ≤ 𝑟))
 
22-Jul-2025dich0 14806 Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
(∀𝑧 ∈ ℝ (𝑧 ≤ 0 ∨ 0 ≤ 𝑧) ↔ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
 
22-Jul-2025ivthdichlem 14805 Lemma for ivthdich 14807. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    &   (𝜑 → 𝑍 ∈ ℝ)    &   (𝜑 → ∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))))    ⇒   (𝜑 → (𝑍 ≤ 0 ∨ 0 ≤ 𝑍))
 
22-Jul-2025hovergt0 14804 The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ((𝐶 ∈ ℝ ∧ 0 < 𝐶) → 0 ≤ (𝐹‘𝐶))
 
22-Jul-2025hoverlt1 14803 The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ((𝐶 ∈ ℝ ∧ 𝐶 < 1) → (𝐹‘𝐶) ≤ 0)
 
21-Jul-2025hoverb 14802 A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   (𝑍 ∈ ℝ → 𝑍 < (𝐹‘(𝑍 + 2)))
 
21-Jul-2025hovera 14801 A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   (𝑍 ∈ ℝ → (𝐹‘(𝑍 − 1)) < 𝑍)
 
21-Jul-2025rexeqtrrdv 2701 Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐵 = 𝐴)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
 
21-Jul-2025raleqtrrdv 2700 Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐵 = 𝐴)    ⇒   (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
 
21-Jul-2025rexeqtrdv 2699 Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐴 = 𝐵)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
 
21-Jul-2025raleqtrdv 2698 Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐴 = 𝐵)    ⇒   (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
 
20-Jul-2025hovercncf 14800 The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   𝐹 ∈ (ℝ–cn→ℝ)
 
19-Jul-2025mincncf 14770 The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
(𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   (𝜑 → (𝑥 ∈ 𝑋 ↦ inf({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
 
18-Jul-2025maxcncf 14769 The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)
(𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   (𝜑 → (𝑥 ∈ 𝑋 ↦ sup({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
 
14-Jul-2025xnn0nnen 10508 The set of extended nonnegative integers is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 14-Jul-2025.)
ℕ0* ≈ ℕ
 
12-Jul-2025nninfninc 7182 All values beyond a zero in an ℕ∞ sequence are zero. This is another way of stating that elements of ℕ∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.)
(𝜑 → 𝐴 ∈ ℕ∞)    &   (𝜑 → 𝑋 ∈ ω)    &   (𝜑 → 𝑌 ∈ ω)    &   (𝜑 → 𝑋 ⊆ 𝑌)    &   (𝜑 → (𝐴‘𝑋) = ∅)    ⇒   (𝜑 → (𝐴‘𝑌) = ∅)
 
10-Jul-2025nninfctlemfo 12177 Lemma for nninfct 12178. (Contributed by Jim Kingdon, 10-Jul-2025.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))    &   𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {⟨+∞, (ω × {1o})⟩})    ⇒   (ω ∈ Omni → 𝐼:ℕ0*–onto→ℕ∞)
 
8-Jul-2025nnnninfen 15511 Equinumerosity of the natural numbers and ℕ∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
(ω ≈ ℕ∞ ↔ ω ∈ Omni)
 
8-Jul-2025nninfct 12178 The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.)
(ω ∈ Omni → ∃𝑓 𝑓:ω–onto→(ℕ∞ ⊔ 1o))
 
8-Jul-2025nninfinf 10514 ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.)
ω ≼ ℕ∞
 
7-Jul-2025ivthreinc 14799 Restating the intermediate value theorem. Given a hypothesis stating the intermediate value theorem (in a strong form which is not provable given our axioms alone), provide a conclusion similar to the theorem as stated in the Metamath Proof Explorer (which is also similar to how we state the theorem for a strictly monotonic function at ivthinc 14797). Being able to have a hypothesis stating the intermediate value theorem will be helpful when it comes time to show that it implies a constructive taboo. This version of the theorem requires that the function 𝐹 is continuous on the entire real line, not just (𝐴[,]𝐵) which may be an unnecessary condition but which is sufficient for the way we want to use it. (Contributed by Jim Kingdon, 7-Jul-2025.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → 𝐹 ∈ (ℝ–cn→ℝ))    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (𝜑 → ∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))))    ⇒   (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
 
28-Jun-2025fngsum 12971 Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
Σg Fn (V × V)
 
28-Jun-2025iotaexel 5878 Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) → (℩𝑥𝜑) ∈ V)
 
27-Jun-2025df-igsum 12870 Define a finite group sum (also called "iterated sum") of a structure.

Given 𝐺 Σg 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set 𝐴 and each demanding different properties of 𝐺.

1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity.

2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ((𝐹‘1) + (𝐹‘2)) + (𝐹‘3), etc.

3. This definition does not handle other cases.

(Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)

Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))
 
20-Jun-2025opprnzrbg 13681 The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 13682. (Contributed by SN, 20-Jun-2025.)
𝑂 = (oppr‘𝑅)    ⇒   (𝑅 ∈ 𝑉 → (𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing))
 
16-Jun-2025fnpsr 14153 The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
mPwSer Fn (V × V)
 
14-Jun-2025basm 12679 A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
𝐵 = (Base‘𝐺)    ⇒   (𝐴 ∈ 𝐵 → ∃𝑗 𝑗 ∈ 𝐺)
 
14-Jun-2025elfvm 5587 If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
(𝐴 ∈ (𝐹‘𝐵) → ∃𝑗 𝑗 ∈ 𝐹)
 
6-Jun-2025pcxqcl 12450 The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.)
((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → ((𝑃 pCnt 𝑁) ∈ ℤ ∨ (𝑃 pCnt 𝑁) = +∞))
 
5-Jun-2025xqltnle 10336 "Less than" expressed in terms of "less than or equal to", for extended numbers which are rational or +∞. We have not yet had enough usage of such numbers to warrant fully developing the concept, as in ℕ0* or ℝ*, so for now we just have a handful of theorems for what we need. (Contributed by Jim Kingdon, 5-Jun-2025.)
(((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
 
30-May-20254sqexercise2 12537 Exercise which may help in understanding the proof of 4sqlemsdc 12538. (Contributed by Jim Kingdon, 30-May-2025.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑛 = ((𝑥↑2) + (𝑦↑2))}    ⇒   (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
 
27-May-2025iotaexab 5233 Existence of the ℩ class when all the possible values are contained in a set. (Contributed by Jim Kingdon, 27-May-2025.)
({𝑥 ∣ 𝜑} ∈ 𝑉 → (℩𝑥𝜑) ∈ V)
 
25-May-20254sqlemsdc 12538 Lemma for 4sq 12548. The property of being the sum of four squares is decidable.

The proof involves showing that (for a particular 𝐴) there are only a finite number of possible ways that it could be the sum of four squares, so checking each of those possibilities in turn decides whether the number is the sum of four squares. If this proof is hard to follow, especially because of its length, the simplified versions at 4sqexercise1 12536 and 4sqexercise2 12537 may help clarify, as they are using very much the same techniques on simplified versions of this lemma. (Contributed by Jim Kingdon, 25-May-2025.)

𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
 
25-May-20254sqexercise1 12536 Exercise which may help in understanding the proof of 4sqlemsdc 12538. (Contributed by Jim Kingdon, 25-May-2025.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ 𝑛 = (𝑥↑2)}    ⇒   (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
 
24-May-20254sqleminfi 12535 Lemma for 4sq 12548. 𝐴 ∩ ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝑃 ∈ ℕ)    &   𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   (𝜑 → (𝐴 ∩ ran 𝐹) ∈ Fin)
 
24-May-20254sqlemffi 12534 Lemma for 4sq 12548. ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝑃 ∈ ℕ)    &   𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   (𝜑 → ran 𝐹 ∈ Fin)
 
24-May-20254sqlemafi 12533 Lemma for 4sq 12548. 𝐴 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝑃 ∈ ℕ)    &   𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    ⇒   (𝜑 → 𝐴 ∈ Fin)
 
24-May-2025infidc 6993 The intersection of two sets is finite if one of them is and the other is decidable. (Contributed by Jim Kingdon, 24-May-2025.)
((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵) → (𝐴 ∩ 𝐵) ∈ Fin)
 
19-May-2025zrhex 14109 Set existence for ℤRHom. (Contributed by Jim Kingdon, 19-May-2025.)
𝐿 = (ℤRHom‘𝑅)    ⇒   (𝑅 ∈ 𝑉 → 𝐿 ∈ V)
 
16-May-2025rhmex 13653 Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.)
((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 RingHom 𝑆) ∈ V)
 
15-May-2025ghmex 13325 The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) ∈ V)
 
15-May-2025mhmex 13034 The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) ∈ V)
 
14-May-2025idomcringd 13774 An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) (Proof shortened by SN, 14-May-2025.)
(𝜑 → 𝑅 ∈ IDomn)    ⇒   (𝜑 → 𝑅 ∈ CRing)
 
6-May-2025rrgnz 13764 In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025.)
𝐸 = (RLReg‘𝑅)    &    0 = (0g‘𝑅)    ⇒   (𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸)
 
5-May-2025rngressid 13450 A non-unital ring restricted to its base set is a non-unital ring. It will usually be the original non-unital ring exactly, of course, but to show that needs additional conditions such as those in strressid 12689. (Contributed by Jim Kingdon, 5-May-2025.)
𝐵 = (Base‘𝐺)    ⇒   (𝐺 ∈ Rng → (𝐺 ↾s 𝐵) ∈ Rng)
 
5-May-2025ablressid 13405 A commutative group restricted to its base set is a commutative group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 12689. (Contributed by Jim Kingdon, 5-May-2025.)
𝐵 = (Base‘𝐺)    ⇒   (𝐺 ∈ Abel → (𝐺 ↾s 𝐵) ∈ Abel)
 
29-Apr-2025rlmscabas 13956 Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
(𝑅 ∈ 𝑋 → (Base‘𝑅) = (Base‘(Scalar‘(ringLMod‘𝑅))))
 
29-Apr-2025ressbasid 12688 The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.)
𝐵 = (Base‘𝑊)    ⇒   (𝑊 ∈ 𝑉 → (Base‘(𝑊 ↾s 𝐵)) = 𝐵)
 
28-Apr-2025lssmex 13851 If a linear subspace is inhabited, the class it is built from is a set. (Contributed by Jim Kingdon, 28-Apr-2025.)
𝑆 = (LSubSp‘𝑊)    ⇒   (𝑈 ∈ 𝑆 → 𝑊 ∈ V)
 
27-Apr-2025lidlex 13969 Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
(𝑊 ∈ 𝑉 → (LIdeal‘𝑊) ∈ V)
 
27-Apr-2025lssex 13850 Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.)
(𝑊 ∈ 𝑉 → (LSubSp‘𝑊) ∈ V)
 
25-Apr-2025rspex 13970 Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
(𝑊 ∈ 𝑉 → (RSpan‘𝑊) ∈ V)
 
25-Apr-2025lspex 13891 Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.)
(𝑊 ∈ 𝑋 → (LSpan‘𝑊) ∈ V)
 
25-Apr-2025eqgex 13291 The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.)
((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐺 ~QG 𝑆) ∈ V)
 
25-Apr-2025qusex 12908 Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
((𝑅 ∈ 𝑉 ∧ ∼ ∈ 𝑊) → (𝑅 /s ∼ ) ∈ V)
 
23-Apr-20251dom1el 15483 If a set is dominated by one, then any two of its elements are equal. (Contributed by Jim Kingdon, 23-Apr-2025.)
((𝐴 ≼ 1o ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → 𝐵 = 𝐶)
 
22-Apr-2025mulgex 13193 Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.)
(𝐺 ∈ 𝑉 → (.g‘𝐺) ∈ V)
 
20-Apr-2025elovmpod 6116 Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6117 in deduction form. (Revised by AV, 20-Apr-2025.)
𝑂 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)    &   (𝜑 → 𝑋 ∈ 𝐴)    &   (𝜑 → 𝑌 ∈ 𝐵)    &   (𝜑 → 𝐷 ∈ 𝑉)    &   ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → 𝐶 = 𝐷)    ⇒   (𝜑 → (𝐸 ∈ (𝑋𝑂𝑌) ↔ 𝐸 ∈ 𝐷))
 
18-Apr-2025df2idl2 14005 Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
𝑈 = (2Ideal‘𝑅)    &   𝐵 = (Base‘𝑅)    &    · = (.r‘𝑅)    ⇒   (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 ((𝑥 · 𝑦) ∈ 𝐼 ∧ (𝑦 · 𝑥) ∈ 𝐼))))
 
18-Apr-20252idlmex 13997 Existence of the set a two-sided ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
𝑇 = (2Ideal‘𝑊)    ⇒   (𝑈 ∈ 𝑇 → 𝑊 ∈ V)
 
18-Apr-2025dflidl2 13984 Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
𝑈 = (LIdeal‘𝑅)    &   𝐵 = (Base‘𝑅)    &    · = (.r‘𝑅)    ⇒   (𝑅 ∈ Ring → (𝐼 ∈ 𝑈 ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐼 (𝑥 · 𝑦) ∈ 𝐼)))
 
18-Apr-2025lidlmex 13971 Existence of the set a left ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
𝐼 = (LIdeal‘𝑊)    ⇒   (𝑈 ∈ 𝐼 → 𝑊 ∈ V)
 
18-Apr-2025lsslsp 13925 Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.)
𝑋 = (𝑊 ↾s 𝑈)    &   𝑀 = (LSpan‘𝑊)    &   𝑁 = (LSpan‘𝑋)    &   𝐿 = (LSubSp‘𝑊)    ⇒   ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈) → (𝑁‘𝐺) = (𝑀‘𝐺))
 
16-Apr-2025sraex 13942 Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
(𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑 → 𝑆 ⊆ (Base‘𝑊))    &   (𝜑 → 𝑊 ∈ 𝑋)    ⇒   (𝜑 → 𝐴 ∈ V)
 
14-Apr-2025grpmgmd 13098 A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.)
(𝜑 → 𝐺 ∈ Grp)    ⇒   (𝜑 → 𝐺 ∈ Mgm)
 
12-Apr-2025psraddcl 14164 Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝐵 = (Base‘𝑆)    &    + = (+g‘𝑆)    &   (𝜑 → 𝑅 ∈ Mgm)    &   (𝜑 → 𝑋 ∈ 𝐵)    &   (𝜑 → 𝑌 ∈ 𝐵)    ⇒   (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
 
10-Apr-2025cndcap 15549 Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ ℂ DECID 𝑧 # 𝑤)
 
4-Apr-2025ghmf1 13343 Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 4-Apr-2025.)
𝐴 = (Base‘𝑅)    &   𝐵 = (Base‘𝑆)    &   𝑁 = (0g‘𝑅)    &    0 = (0g‘𝑆)    ⇒   (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹:𝐴–1-1→𝐵 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) = 0 → 𝑥 = 𝑁)))
 
3-Apr-2025quscrng 14029 The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
𝑈 = (𝑅 /s (𝑅 ~QG 𝑆))    &   𝐼 = (LIdeal‘𝑅)    ⇒   ((𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼) → 𝑈 ∈ CRing)
 
31-Mar-2025mpocnfldmul 14055 The multiplication operation of the field of complex numbers. Version of cnfldmul 14054 using maps-to notation. (Contributed by GG, 31-Mar-2025.)
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld)
 
31-Mar-2025mpocnfldadd 14053 The addition operation of the field of complex numbers. Version of cnfldadd 14052 using maps-to notation. (Contributed by GG, 31-Mar-2025.)
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld)
 
31-Mar-20252idlcpbl 14020 The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
𝑋 = (Base‘𝑅)    &   𝐸 = (𝑅 ~QG 𝑆)    &   𝐼 = (2Ideal‘𝑅)    &    · = (.r‘𝑅)    ⇒   ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
 
22-Mar-2025idomringd 13775 An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
(𝜑 → 𝑅 ∈ IDomn)    ⇒   (𝜑 → 𝑅 ∈ Ring)
 
22-Mar-2025idomdomd 13773 An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
(𝜑 → 𝑅 ∈ IDomn)    ⇒   (𝜑 → 𝑅 ∈ Domn)
  Copyright terms: Public domain W3C HTML validation [external]