P. 433 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43201-43300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sn-addgt0d 43201	The sum of positive numbers is positive. Proof of addgt0d 11788 without ax-mulcom 11163. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	sn-nnne0 43202	nnne0 12269 without ax-mulcom 11163. (Contributed by SN, 25-Jan-2025.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	reelznn0nn 43203	elznn0nn 12604 restated using df-resub 43095. (Contributed by SN, 25-Jan-2025.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ)))
Theorem	nn0addcom 43204	Addition is commutative for nonnegative integers. Proven without ax-mulcom 11163. (Contributed by SN, 1-Feb-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcomlem 43205	Lemma for zaddcom 43206. (Contributed by SN, 1-Feb-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcom 43206	Addition is commutative for integers. Proven without ax-mulcom 11163. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	renegmulnnass 43207	Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))
Theorem	nn0mulcom 43208	Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11163. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcomlem 43209	Lemma for zmulcom 43210. (Contributed by SN, 25-Jan-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcom 43210	Multiplication is commutative for integers. Proven without ax-mulcom 11163. From this result and grpcominv1 43250, we can show that rationals commute under multiplication without using ax-mulcom 11163. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	mulgt0con1dlem 43211	Lemma for mulgt0con1d 43212. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0))
Theorem	mulgt0con1d 43212	Counterpart to mulgt0con2d 43213, though not a lemma. This is the first use of ax-pre-mulgt0 11176. One direction of mulgt0b2d 43220. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐴 < 0)
Theorem	mulgt0con2d 43213	Lemma for mulgt0b1d 43214 and contrapositive of mulgt0 11286. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐵 < 0)
Theorem	mulgt0b1d 43214	Biconditional, deductive form of mulgt0 11286. The second factor is positive iff the product is. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-ltmul2d 43215	ltmul2d 13101 without ax-mulcom 11163. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))
Theorem	sn-ltmulgt11d 43216	ltmulgt11d 13094 without ax-mulcom 11163. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴)))
Theorem	sn-0lt1 43217	0lt1 11735 without ax-mulcom 11163. (Contributed by SN, 13-Feb-2024.)
⊢ 0 < 1
Theorem	sn-ltp1 43218	ltp1 12054 without ax-mulcom 11163. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	sn-recgt0d 43219	The reciprocal of a positive real is positive. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 0 < (1 /ℝ 𝐴))
Theorem	mulgt0b2d 43220	Biconditional, deductive form of mulgt0 11286. The first factor is positive iff the product is. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-mulgt1d 43221	mulgt1d 12150 without ax-mulcom 11163. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	reneg1lt0 43222	Negative one is a negative number. (Contributed by SN, 1-Jun-2024.)
⊢ (0 −ℝ 1) < 0
Theorem	sn-reclt0d 43223	The reciprocal of a negative real is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) < 0)
Theorem	mulltgt0d 43224	Negative times positive is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)
Theorem	mullt0b1d 43225	When the first term is negative, the second term is positive iff the product is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ (𝐴 · 𝐵) < 0))
Theorem	mullt0b2d 43226	When the second term is negative, the first term is positive iff the product is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ (𝐴 · 𝐵) < 0))
Theorem	sn-mullt0d 43227	The product of two negative numbers is positive. (Contributed by SN, 1-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴 · 𝐵))
Theorem	sn-msqgt0d 43228	A nonzero square is positive. (Contributed by SN, 1-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴 · 𝐴))
Theorem	sn-inelr 43229	inelr 12207 without ax-mulcom 11163. (Contributed by SN, 1-Jun-2024.)
⊢ ¬ i ∈ ℝ
Theorem	sn-itrere 43230	i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	sn-retire 43231	Commuted version of sn-itrere 43230. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	cnreeu 43232	The reals in the expression given by cnre 11204 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.)
⊢ (𝜑 → 𝑟 ∈ ℝ)    &   ⊢ (𝜑 → 𝑠 ∈ ℝ)    &   ⊢ (𝜑 → 𝑡 ∈ ℝ)    &   ⊢ (𝜑 → 𝑢 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
Theorem	sn-sup2 43233*	sup2 12170 with exactly the same proof except for using sn-ltp1 43218 instead of ltp1 12054, saving ax-mulcom 11163. (Contributed by SN, 26-Jun-2024.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sn-sup3d 43234*	sup3 12171 without ax-mulcom 11163, proven trivially from sn-sup2 43233. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sn-suprcld 43235*	suprcld 12177 without ax-mulcom 11163, proven trivially from sn-sup3d 43234. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	sn-suprubd 43236*	suprubd 12176 without ax-mulcom 11163, proven trivially from sn-suprcld 43235. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
21.31.6  Structures
Theorem	sn-base0 43237	Avoid axioms in base0 17273 by using the discouraged df-base 17269. This kind of axiom save is probably not worth it. (Contributed by SN, 16-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ = (Base‘∅)
Theorem	nelsubginvcld 43238	The inverse of a non-subgroup-member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) ∈ (𝐵 ∖ 𝑆))
Theorem	nelsubgcld 43239	A non-subgroup-member plus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐵 ∖ 𝑆))
Theorem	nelsubgsubcld 43240	A non-subgroup-member minus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐵 ∖ 𝑆))
Theorem	rnasclg 43241	The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) → ran 𝐴 = (𝑁‘{ 1 }))
Theorem	frlmfielbas 43242	The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝑁 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁))
Theorem	frlmfzwrd 43243	A vector of a module with indices from 0 to 𝑁 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆)
Theorem	frlmfzowrd 43244	A vector of a module with indices from 0 to 𝑁 − 1 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆)
Theorem	frlmfzolen 43245	The dimension of a vector of a module with indices from 0 to 𝑁 − 1. (Contributed by SN, 1-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (♯‘𝑋) = 𝑁)
Theorem	frlmfzowrdb 43246	The vectors of a module with indices 0 to 𝑁 − 1 are the length- 𝑁 words over the scalars of the module. (Contributed by SN, 1-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ Word 𝑆 ∧ (♯‘𝑋) = 𝑁)))
Theorem	frlmfzoccat 43247	The concatenation of two vectors of dimension 𝑁 and 𝑀 forms a vector of dimension 𝑁 + 𝑀. (Contributed by SN, 31-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿))    &   ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀))    &   ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ 𝐷 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑈 ++ 𝑉) ∈ 𝐵)
Theorem	frlmvscadiccat 43248	Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿))    &   ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀))    &   ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ 𝐷 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐷)    &   ⊢ 𝑂 = ( ·𝑠 ‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝑋)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉)))
Theorem	grpasscan2d 43249	An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋)
Theorem	grpcominv1 43250	If two elements commute, then they commute with each other's inverses (case of the first element commuting with the inverse of the second element). (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑋 + (𝑁‘𝑌)) = ((𝑁‘𝑌) + 𝑋))
Theorem	grpcominv2 43251	If two elements commute, then they commute with each other's inverses (case of the second element commuting with the inverse of the first element). (Contributed by SN, 1-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑌 + (𝑁‘𝑋)) = ((𝑁‘𝑋) + 𝑌))
Theorem	finsubmsubg 43252	A submonoid of a finite group is a subgroup. This does not extend to infinite groups, as the submonoid ℕ0 of the group (ℤ, + ) shows. Note also that the union of a submonoid and its inverses need not be a submonoid, as the submonoid (ℕ0 ∖ {1}) of the group (ℤ, + ) shows: 3 is in that submonoid, -2 is the inverse of 2, but 1 is not in their union. Or simply, the subgroup generated by (ℕ0 ∖ {1}) is ℤ, not (ℤ ∖ {1, -1}). (Contributed by SN, 31-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	opprmndb 43253	A class is a monoid if and only if its opposite (ring) is a monoid. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd)
Theorem	opprgrpb 43254	A class is a group if and only if its opposite (ring) is a group. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp)
Theorem	opprablb 43255	A class is an Abelian group if and only if its opposite (ring) is an Abelian group. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Abel ↔ 𝑂 ∈ Abel)
Theorem	imacrhmcl 43256	The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.)
⊢ 𝐶 = (𝑁 ↾s (𝐹 “ 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀))    ⇒   ⊢ (𝜑 → 𝐶 ∈ CRing)
Theorem	rimco 43257	The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025.)
⊢ ((𝐹 ∈ (𝑆 RingIso 𝑇) ∧ 𝐺 ∈ (𝑅 RingIso 𝑆)) → (𝐹 ∘ 𝐺) ∈ (𝑅 RingIso 𝑇))
Theorem	rictr 43258	Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑆 ≃𝑟 𝑇) → 𝑅 ≃𝑟 𝑇)
Theorem	riccrng1 43259	Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing) → 𝑆 ∈ CRing)
Theorem	riccrng 43260	A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing))
Theorem	domnexpgn0cl 43261	In a domain, a (nonnegative) power of a nonzero element is nonzero. (Contributed by SN, 6-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐵 ∖ { 0 }))
Theorem	drnginvrn0d 43262	A multiplicative inverse in a division ring is nonzero. (recne0d 11984 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 )
Theorem	drngmullcan 43263	Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11848 analog). (Contributed by SN, 14-Aug-2024.) (Proof shortened by SN, 25-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drngmulrcan 43264	Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11849 analog). (Contributed by SN, 14-Aug-2024.) (Proof shortened by SN, 25-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drnginvmuld 43265	Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋)))
Theorem	ricdrng1 43266	A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing)
Theorem	ricdrng 43267	A ring is a division ring if and only if an isomorphic ring is a division ring. (Contributed by SN, 18-Feb-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ DivRing ↔ 𝑆 ∈ DivRing))
Theorem	ricfld 43268	A ring is a field if and only if an isomorphic ring is a field. (Contributed by SN, 18-Feb-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Field ↔ 𝑆 ∈ Field))
Theorem	asclf1 43269*	Two ways of saying the scalar injection is one-to-one. (Contributed by SN, 3-Jul-2025.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (0g‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ Ring)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝐴:𝐾–1-1→𝐵 ↔ ∀𝑠 ∈ 𝐾 ((𝐴‘𝑠) = 0 → 𝑠 = 𝑁)))
Theorem	abvexp 43270	Move exponentiation in and out of absolute value. (Contributed by SN, 3-Jul-2025.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹‘(𝑁 ↑ 𝑋)) = ((𝐹‘𝑋)↑𝑁))
Theorem	fimgmcyclem 43271*	Lemma for fimgmcyc 43272. (Contributed by SN, 7-Jul-2025.)
⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)))
Theorem	fimgmcyc 43272*	Version of odcl2 19634 for finite magmas: the multiples of an element 𝐴 ∈ 𝐵 are eventually periodic. (Contributed by SN, 3-Jul-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ · = (.g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mgm)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑝 ∈ ℕ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴))
Theorem	fidomncyc 43273*	Version of odcl2 19634 for multiplicative groups of finite domains (that is, a finite monoid where nonzero elements are cancellable): one (1) is a multiple of any nonzero element. (Contributed by SN, 3-Jul-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 }))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑛 ↑ 𝐴) = 1 )
Theorem	fiabv 43274*	In a finite domain (a finite field), the only absolute value is the trivial one (abvtrivg 20915). (Contributed by SN, 3-Jul-2025.)
⊢ 𝐴 = (AbsVal‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑇 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1))    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐴 = {𝑇})
Theorem	lvecgrp 43275	A vector space is a group. (Contributed by SN, 28-May-2023.)
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp)
Theorem	lvecring 43276	The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring)
Theorem	frlm0vald 43277	All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 )
Theorem	frlmsnic 43278*	Given a free module with a singleton as the index set, that is, a free module of one-dimensional vectors, the function that maps each vector to its coordinate is a module isomorphism from that module to its ring of scalars seen as a module. (Contributed by Steven Nguyen, 18-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod {𝐼})    &   ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑊) ↦ (𝑥‘𝐼))    ⇒   ⊢ ((𝐾 ∈ Ring ∧ 𝐼 ∈ V) → 𝐹 ∈ (𝑊 LMIso (ringLMod‘𝐾)))
Theorem	uvccl 43279	A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵)
Theorem	uvcn0 43280	A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 )
Theorem	psrmnd 43281	The ring of power series is a monoid. (Contributed by SN, 25-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Mnd)
Theorem	mhmcopsr 43282	The composition of a monoid homomorphism and a power series is a power series. (Contributed by SN, 18-May-2025.)
⊢ 𝑃 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑄 = (𝐼 mPwSer 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶)
Theorem	mhmcoaddpsr 43283	Show that the ring homomorphism in rhmpsr 43285 preserves addition. (Contributed by SN, 18-May-2025.)
⊢ 𝑃 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑄 = (𝐼 mPwSer 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ✚ = (+g‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺)))
Theorem	rhmcomulpsr 43284	Show that the ring homomorphism in rhmpsr 43285 preserves multiplication. (Contributed by SN, 18-May-2025.)
⊢ 𝑃 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑄 = (𝐼 mPwSer 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ∙ = (.r‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺)))
Theorem	rhmpsr 43285*	Provide a ring homomorphism between two power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑄 = (𝐼 mPwSer 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	rhmpsr1 43286*	Provide a ring homomorphism between two univariate power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (PwSer1‘𝑅)    &   ⊢ 𝑄 = (PwSer1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	evl0 43287	The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂}))
Theorem	evlsbagval 43288*	Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since 0 and 1 using 𝑈 instead of 𝑆 may not be convenient. (Contributed by SN, 29-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑊 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 1 = (1r‘𝑈)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐹 = (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 ))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑊 ∧ ((𝑄‘𝐹)‘𝐴) = (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣))))))
Theorem	evlvvvallem 43289*	Lemma for theorems using evlvvval 22263. Version of evlsvvvallem2 22222 using df-evl 22205. (Contributed by SN, 11-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅))
Theorem	evlselvlem 43290*	Lemma for evlselv 43291. Used to re-index to and from bags of variables in 𝐼 and bags of variables in the subsets 𝐽 and 𝐼 ∖ 𝐽. (Contributed by SN, 10-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐸 = {𝑔 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑔 “ ℕ) ∈ Fin}    &   ⊢ 𝐶 = {𝑓 ∈ (ℕ0 ↑m (𝐼 ∖ 𝐽)) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (𝑐 ∈ 𝐶, 𝑒 ∈ 𝐸 ↦ (𝑐 ∪ 𝑒))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → 𝐻:(𝐶 × 𝐸)–1-1-onto→𝐷)
Theorem	evlselv 43291	Evaluating a selection of variable assignments, then evaluating the rest of the variables, is the same as evaluating with all assignments. (Contributed by SN, 10-Mar-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐿 = (algSc‘𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((((𝐼 ∖ 𝐽) eval 𝑅)‘(((𝐽 eval 𝑈)‘(((𝐼 selectVars 𝑅)‘𝐽)‘𝐹))‘(𝐿 ∘ (𝐴 ↾ 𝐽))))‘(𝐴 ↾ (𝐼 ∖ 𝐽))) = (((𝐼 eval 𝑅)‘𝐹)‘𝐴))
Theorem	fsuppind 43292*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21885 and frlmplusgval 21893). This theorem is structurally general for polynomial proof usage (see mplelbas 22119 and mpladd 22137). Note that hypothesis 0 is redundant when 𝐼 is nonempty. (Contributed by SN, 18-May-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻)    ⇒   ⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻)
Theorem	fsuppssindlem1 43293*	Lemma for fsuppssind 43295. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, ((𝐹 ↾ 𝑆)‘𝑥), 0 )))
Theorem	fsuppssindlem2 43294*	Lemma for fsuppssind 43295. Write a function as a union. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻)))
Theorem	fsuppssind 43295*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support (see fsuppind 43292) whose supports are subsets of 𝑆. (Contributed by SN, 15-Jun-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    &   ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐼 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐻)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋:𝐼⟶𝐵)    &   ⊢ (𝜑 → 𝑋 finSupp 0 )    &   ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐻)
Theorem	mhpind 43296*	The homogeneous polynomials of degree 𝑁 are generated by the terms of degree 𝑁 and addition. (Contributed by SN, 28-Jul-2024.)
⊢ 𝐻 = (𝐼 mHomP 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐺)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐺)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ 𝐺)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐺)
Theorem	evlsmhpvvval 43297*	Give a formula for the evaluation of a homogeneous polynomial given assignments from variables to values. The difference between this and evlsvvval 22223 is that 𝑏 ∈ 𝐷 is restricted to 𝑏 ∈ 𝐺, that is, we can evaluate an 𝑁-th degree homogeneous polynomial over just the terms where the sum of all variable degrees is 𝑁. (Contributed by SN, 5-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐺 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐺 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
Theorem	mhphflem 43298*	Lemma for mhphf 43299. Add several multiples of 𝐿 together, in a case where the total amount of multiplies is 𝑁. (Contributed by SN, 30-Jul-2024.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁}    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (𝑁 · 𝐿))
Theorem	mhphf 43299	A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the (𝑄‘𝑋) which corresponds to 𝑋). (Contributed by SN, 28-Jul-2024.) (Proof shortened by SN, 8-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf2 43300	A homogeneous polynomial defines a homogeneous function; this is mhphf 43299 with simpler notation in the conclusion in exchange for a complex definition of ∙, which is based on frlmvscafval 21895 but without the finite support restriction (frlmpws 21879, frlmbas 21884) on the assignments 𝐴 from variables to values. TODO?: Polynomials (df-mpl 22040) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ ∙ = ( ·𝑠 ‘((ringLMod‘𝑆) ↑s 𝐼))    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))