P. 411 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41001-41100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fnimasnd 41001	The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 “ {𝑆}) = {(𝐹‘𝑆)})
Theorem	fvmptd4 41002*	Deduction version of fvmpt 6994 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	eqresfnbd 41003	Property of being the restriction of a function. Note that this is closer to funssres 6589 than fnssres 6670. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹)))
Theorem	f1o2d2 41004*	Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐼 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐽 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐷)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶))    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)
Theorem	fmpocos 41005*	Composition of two functions. Variation of fmpoco 8076 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇))
Theorem	ovmpogad 41006*	Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7557. (Contributed by SN, 14-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ofun 41007	A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024.)
⊢ (𝜑 → 𝐴 Fn 𝑀)    &   ⊢ (𝜑 → 𝐵 Fn 𝑀)    &   ⊢ (𝜑 → 𝐶 Fn 𝑁)    &   ⊢ (𝜑 → 𝐷 Fn 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑀 ∩ 𝑁) = ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷)) = ((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷)))
Theorem	dfqs2 41008*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅)
Theorem	dfqs3 41009*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅}
Theorem	qseq12d 41010	Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	qsalrel 41011*	The quotient set is equal to the singleton of 𝐴 when all elements are related and 𝐴 is nonempty. (Contributed by SN, 8-Jun-2023.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦)    &   ⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴})
Theorem	fsuppfund 41012	A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fsuppsssuppgd 41013	If the support of a function is a subset of a finite support, it is finite. Deduction associated with fsuppsssupp 9375. (Contributed by SN, 6-Mar-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑂)    &   ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑂))    ⇒   ⊢ (𝜑 → 𝐺 finSupp 𝑍)
Theorem	fsuppss 41014	A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025.)
⊢ (𝜑 → 𝐹 ⊆ 𝐺)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑍)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	elmapssresd 41015	A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8835 with some reordering involving mapsspm 8866. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶))    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷))
Theorem	mapcod 41016	Compose two mappings. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶))
Theorem	fzosumm1 41017*	Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵))
Theorem	ccatcan2d 41018	Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ Word 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵))
21.28.3  Structures
Theorem	nelsubginvcld 41019	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 41020	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 41021	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 41022	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 41023	The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝑁 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁))
Theorem	frlmfzwrd 41024	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 41025	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 41026	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 41027	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 41028	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 41029	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 41030	An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋)
Theorem	grpcominv1 41031	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 41032	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 41033	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	ringlzd 41034	The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 0 · 𝑋) = 0 )
Theorem	ringrzd 41035	The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 0 ) = 0 )
Theorem	crngcomd 41036	Multiplication is commutative in a commutative ring. (Contributed by SN, 8-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑌 · 𝑋))
Theorem	crng12d 41037	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by SN, 8-Mar-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · (𝑌 · 𝑍)) = (𝑌 · (𝑋 · 𝑍)))
Theorem	imacrhmcl 41038	The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.)
⊢ 𝐶 = (𝑁 ↾s (𝐹 “ 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀))    ⇒   ⊢ (𝜑 → 𝐶 ∈ CRing)
Theorem	rimrcl1 41039	Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅 ∈ Ring)
Theorem	rimrcl2 41040	Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑆 ∈ Ring)
Theorem	rimcnv 41041	The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025.)
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → ◡𝐹 ∈ (𝑆 RingIso 𝑅))
Theorem	rimco 41042	The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025.)
⊢ ((𝐹 ∈ (𝑆 RingIso 𝑇) ∧ 𝐺 ∈ (𝑅 RingIso 𝑆)) → (𝐹 ∘ 𝐺) ∈ (𝑅 RingIso 𝑇))
Theorem	ricsym 41043	Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅)
Theorem	rictr 41044	Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑆 ≃𝑟 𝑇) → 𝑅 ≃𝑟 𝑇)
Theorem	riccrng1 41045	Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing) → 𝑆 ∈ CRing)
Theorem	riccrng 41046	A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing))
Theorem	drnginvrn0d 41047	A multiplicative inverse in a division ring is nonzero. (recne0d 11980 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 )
Theorem	drngmulcanad 41048	Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11845 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drngmulcan2ad 41049	Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11846 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drnginvmuld 41050	Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋)))
Theorem	ricdrng1 41051	A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing)
Theorem	ricdrng 41052	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	lmodvscld 41053	Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑅 · 𝑋) ∈ 𝑉)
Theorem	flddrngd 41054	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ DivRing)
Theorem	ricfld 41055	A ring is a field if and only if an isomorphic ring is a field. (Contributed by SN, 18-Feb-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Field ↔ 𝑆 ∈ Field))
Theorem	lvecgrp 41056	A vector space is a group. (Contributed by SN, 28-May-2023.)
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp)
Theorem	lvecgrpd 41057	A vector space is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ Grp)
Theorem	lvecring 41058	The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring)
Theorem	frlm0vald 41059	All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 )
Theorem	frlmsnic 41060*	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 41061	A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵)
Theorem	uvcn0 41062	A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 )
Theorem	pwselbasr 41063	The reverse direction of pwselbasb 17430: a function between the index and base set of a structure is an element of the structure power. (Contributed by SN, 29-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑋:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑉)
Theorem	pwsgprod 41064*	Finite products in a power structure are taken componentwise. Compare pwsgsum 19842. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
Theorem	psrbagres 41065*	Restrict a bag of variables in 𝐼 to a bag of variables in 𝐽 ⊆ 𝐼. (Contributed by SN, 10-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐸 = {𝑔 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑔 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐽) ∈ 𝐸)
Theorem	mpllmodd 41066	The polynomial ring is a left module. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑃 ∈ LMod)
Theorem	mplringd 41067	The polynomial ring is a ring. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑃 ∈ Ring)
Theorem	mplcrngd 41068	The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ CRing)
Theorem	mplsubrgcl 41069	An element of a polynomial algebra over a subring is an element of the polynomial algebra. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐶 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐶)
Theorem	mhmcompl 41070	The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶)
Theorem	rhmmpllem1 41071*	Lemma for rhmmpl 41075. A subproof of psrmulcllem 21488. (Contributed by SN, 8-Feb-2025.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))    &   ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp (0g‘𝑅))
Theorem	rhmmpllem2 41072*	Lemma for rhmmpl 41075. A subproof of psrmulcllem 21488. (Contributed by SN, 8-Feb-2025.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))    &   ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ (Base‘𝑅))
Theorem	mhmcoaddmpl 41073	Show that the ring homomorphism in rhmmpl 41075 preserves addition. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ✚ = (+g‘𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺)))
Theorem	rhmcomulmpl 41074	Show that the ring homomorphism in rhmmpl 41075 preserves multiplication. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ∙ = (.r‘𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺)))
Theorem	rhmmpl 41075*	Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm 20267. TODO: Currently mhmvlin 21881 would have to be moved up. Investigate the usefulness of surrounding theorems like mndvcl 21875 and the difference between mhmvlin 21881, ofco 7688, and ofco2 21935. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	mplascl0 41076	The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐴‘𝑂) = 0 )
Theorem	mplascl1 41077	The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑂 = (1r‘𝑅)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐴‘𝑂) = 1 )
Theorem	mplmapghm 41078*	The function 𝐻 mapping polynomials 𝑝 to their coefficient given a bag of variables 𝐹 is a group homomorphism. (Contributed by SN, 15-Mar-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (𝑝 ∈ 𝐵 ↦ (𝑝‘𝐹))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑃 GrpHom 𝑅))
Theorem	evl0 41079	The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂}))
Theorem	evlscl 41080	A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾)
Theorem	evlsval3 41081*	Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝑀 = (mulGrp‘𝑇)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑇)    &   ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑇 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑀 Σg (𝑏 ∘f ↑ 𝐺))))))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝑄 = 𝐸)
Theorem	evlsvval 41082*	Give a formula for the evaluation of a polynomial. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑇 = (𝑆 ↑s (𝐾 ↑m 𝐼))    &   ⊢ 𝑀 = (mulGrp‘𝑇)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑇)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘𝐴) = (𝑇 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝐴‘𝑏)) · (𝑀 Σg (𝑏 ∘f ↑ 𝐺))))))
Theorem	evlsvvvallem 41083*	Lemma for evlsvvval 41085 akin to psrbagev2 21622. (Contributed by SN, 6-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾)
Theorem	evlsvvvallem2 41084*	Lemma for theorems using evlsvvval 41085. (Contributed by SN, 8-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑆))
Theorem	evlsvvval 41085*	Give a formula for the evaluation of a polynomial given assignments from variables to values. This is the sum of the evaluations for each term (corresponding to a bag of variables), that is, the coefficient times the product of each variable raised to the corresponding power. (Contributed by SN, 5-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
Theorem	evlsscaval 41086	Polynomial evaluation builder for a scalar. Compare evl1scad 21836. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21422. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋))
Theorem	evlsvarval 41087	Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlsbagval 41088*	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	evlsexpval 41089	Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ ∙ = (.g‘(mulGrp‘𝑃))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝐵 ∧ ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = (𝑁 ↑ 𝑉)))
Theorem	evlsaddval 41090	Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊)))
Theorem	evlsmulval 41091	Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊)))
Theorem	evlsmaprhm 41092*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 32703. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	evlsevl 41093	Evaluation in a subring is the same as evaluation in the ring itself. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑂 = (𝐼 eval 𝑆)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘𝐹) = (𝑂‘𝐹))
Theorem	evlcl 41094	A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾)
Theorem	evlvvval 41095*	Give a formula for the evaluation of a polynomial given assignments from variables to values. (Contributed by SN, 5-Mar-2025.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑅 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))
Theorem	evlvvvallem 41096*	Lemma for theorems using evlvvval 41095. Version of evlsvvvallem2 41084 using df-evl 21618. (Contributed by SN, 11-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅))
Theorem	evladdval 41097	Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊)))
Theorem	evlmulval 41098	Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊)))
Theorem	selvcllem1 41099	𝑇 is an associative algebra. For simplicity, 𝐼 stands for (𝐼 ∖ 𝐽) and we have 𝐽 ∈ 𝑊 instead of 𝐽 ⊆ 𝐼. TODO-SN: In practice, this "simplification" makes the lemmas harder to use. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑇 ∈ AssAlg)
Theorem	selvcllem2 41100	𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇))