P. 403 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40201-40300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sn-iotanul 40201*	Version of iotanul 6415 using df-iota 6395 instead of dfiota2 6396. (Contributed by SN, 6-Nov-2024.)
⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
Theorem	sn-iotaval 40202*	iotaval 6411 without ax-10 2138, ax-11 2155, ax-12 2172. (Contributed by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦)
Theorem	sn-iotassuni 40203	iotassuni 6416 without ax-10 2138, ax-11 2155, ax-12 2172. (Contributed by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑}
Theorem	sn-iotaex 40204	iotaex 6417 without ax-10 2138, ax-11 2155, ax-12 2172. (Contributed by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ∈ V
Theorem	brif1 40205	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (if(𝜑, 𝐴, 𝐵)𝑅𝐶 ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐶))
Theorem	brif2 40206	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (𝐶𝑅if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝐶𝑅𝐴, 𝐶𝑅𝐵))
Theorem	brif12 40207	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (if(𝜑, 𝐴, 𝐵)𝑅if(𝜑, 𝐶, 𝐷) ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐷))
Theorem	pssexg 40208	The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	pssn0 40209	A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅)
Theorem	psspwb 40210	Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵)
Theorem	xppss12 40211	Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷))
Theorem	elpwbi 40212	Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵)
Theorem	opelxpii 40213	Ordered pair membership in a Cartesian product (implication). (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ 𝐴 ∈ 𝐶    &   ⊢ 𝐵 ∈ 𝐷    ⇒   ⊢ ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷)
Theorem	imaopab 40214*	The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	fnsnbt 40215	A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023.)
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩}))
Theorem	fnimasnd 40216	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 40217*	Deduction version of fvmpt 6884 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	ofun 40218	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 40219*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅)
Theorem	dfqs3 40220*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅}
Theorem	qseq12d 40221	Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	qsalrel 40222*	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	elmapdd 40223	Deduction associated with elmapd 8638. (Contributed by SN, 29-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶:𝐵⟶𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑m 𝐵))
Theorem	isfsuppd 40224	Deduction form of isfsupp 9141. (Contributed by SN, 29-Jul-2024.)
⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝑅)    &   ⊢ (𝜑 → (𝑅 supp 𝑍) ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑅 finSupp 𝑍)
Theorem	fzosumm1 40225*	Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵))
Theorem	ccatcan2d 40226	Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ Word 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵))
20.26.3  Structures
Theorem	nelsubginvcld 40227	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 40228	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 40229	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 40230	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	selvval2lem1 40231	𝑇 is an associative algebra. For simplicity, 𝐼 stands for (𝐼 ∖ 𝐽) and we have 𝐽 ∈ 𝑊 instead of 𝐽 ⊆ 𝐼. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑇 ∈ AssAlg)
Theorem	selvval2lem2 40232	𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇))
Theorem	selvval2lem3 40233	The third argument passed to evalSub is in the domain. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → ran 𝐷 ∈ (SubRing‘𝑇))
Theorem	selvval2lemn 40234	A lemma to illustrate the purpose of selvval2lem3 40233 and the value of 𝑄. Will be renamed in the future when this section is moved to main. (Contributed by SN, 5-Nov-2023.)
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ 𝑄 = ((𝐼 evalSub 𝑇)‘ran 𝐷)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝑆 = (𝑇 ↾s ran 𝐷)    &   ⊢ 𝑋 = (𝑇 ↑s (𝐵 ↑m 𝐼))    &   ⊢ 𝐵 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom 𝑋))
Theorem	selvval2lem4 40235	The fourth argument passed to evalSub is in the domain (a polynomial in (𝐼 mPoly (𝐽 mPoly ((𝐼 ∖ 𝐽) mPoly 𝑅)))). (Contributed by SN, 5-Nov-2023.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ 𝑆 = (𝑇 ↾s ran 𝐷)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑆)    &   ⊢ 𝑋 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ 𝑋)
Theorem	selvval2lem5 40236*	The fifth argument passed to evalSub is in the domain (a function 𝐼⟶𝐸). (Contributed by SN, 22-Feb-2024.)
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐸 = (Base‘𝑇)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐸 ↑m 𝐼))
Theorem	selvcl 40237	Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐸 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸)
Theorem	frlmfielbas 40238	The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝑁 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁))
Theorem	frlmfzwrd 40239	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 40240	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 40241	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 40242	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 40243	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 40244	Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿))    &   ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀))    &   ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ 𝐷 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐷)    &   ⊢ 𝑂 = ( ·𝑠 ‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝑋)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉)))
Theorem	ismhmd 40245*	Deduction version of ismhm 18441. (Contributed by SN, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑍 = (0g‘𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ Mnd)    &   ⊢ (𝜑 → 𝑇 ∈ Mnd)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ (𝜑 → (𝐹‘ 0 ) = 𝑍)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	ablcmnd 40246	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ CMnd)
Theorem	ringcld 40247	Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
Theorem	ringassd 40248	Associative law for multiplication in a ring. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍)))
Theorem	ringlidmd 40249	The unit element of a ring is a left multiplicative identity. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 1 · 𝑋) = 𝑋)
Theorem	ringridmd 40250	The unit element of a ring is a right multiplicative identity. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 1 ) = 𝑋)
Theorem	ringabld 40251	A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Abel)
Theorem	ringcmnd 40252	A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CMnd)
Theorem	drngringd 40253	A division ring is a ring. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Ring)
Theorem	drnggrpd 40254	A division ring is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑅 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑅 ∈ Grp)
Theorem	drnginvrcld 40255	Closure of the multiplicative inverse in a division ring. (reccld 11753 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ 𝐵)
Theorem	drnginvrn0d 40256	A multiplicative inverse in a division ring is nonzero. (recne0d 11754 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 )
Theorem	drnginvrld 40257	Property of the multiplicative inverse in a division ring. (recid2d 11756 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → ((𝐼‘𝑋) · 𝑋) = 1 )
Theorem	drnginvrrd 40258	Property of the multiplicative inverse in a division ring. (recidd 11755 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝑋 · (𝐼‘𝑋)) = 1 )
Theorem	drngmulcanad 40259	Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11619 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drngmulcan2ad 40260	Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11620 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drnginvmuld 40261	Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋)))
Theorem	fldcrngd 40262	A field is a commutative ring. EDITORIAL: Shortens recrng 20835. Also recrng 20835 should be named resrng. Also fldcrng 36171 is misnamed. (Contributed by SN, 23-Nov-2024.)
⊢ (𝜑 → 𝑅 ∈ Field)    ⇒   ⊢ (𝜑 → 𝑅 ∈ CRing)
Theorem	lmodgrpd 40263	A left module is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → 𝑊 ∈ Grp)
Theorem	lvecgrp 40264	A vector space is a group. (Contributed by SN, 28-May-2023.)
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp)
Theorem	lveclmodd 40265	A vector space is a left module. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ LMod)
Theorem	lvecgrpd 40266	A vector space is a group. (Contributed by SN, 16-May-2024.)
⊢ (𝜑 → 𝑊 ∈ LVec)    ⇒   ⊢ (𝜑 → 𝑊 ∈ Grp)
Theorem	lvecring 40267	The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring)
Theorem	lmhmlvec 40268	The property for modules to be vector spaces is invariant under module isomorphism. (Contributed by Steven Nguyen, 15-Aug-2023.)
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	frlm0vald 40269	All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 )
Theorem	frlmsnic 40270*	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 40271	A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵)
Theorem	uvcn0 40272	A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 )
Theorem	pwselbasr 40273	The reverse direction of pwselbasb 17208: 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	pwspjmhmmgpd 40274*	The projection given by pwspjmhm 18477 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑀 MndHom 𝑇))
Theorem	pwsexpg 40275	Value of a group exponentiation in a structure power. Compare pwsmulg 18757. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ ∙ = (.g‘𝑀)    &   ⊢ · = (.g‘𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴)))
Theorem	pwsgprod 40276*	Finite products in a power structure are taken componentwise. Compare pwsgsum 19592. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
Theorem	mplascl0 40277	The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝐴‘𝑂) = 0 )
Theorem	evl0 40278	The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂}))
Theorem	evlsval3 40279*	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	evlsscaval 40280	Polynomial evaluation builder for a scalar. Compare evl1scad 21510. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21099. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋))
Theorem	evlsvarval 40281	Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlsbagval 40282*	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 𝑆 is convenient for its sole use case mhphf 40292, but may not be convenient for other uses. (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 40283	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 40284	Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊)))
Theorem	evlsmulval 40285	Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊)))
Theorem	fsuppind 40286*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 20972 and frlmplusgval 20980). This theorem is structurally general for polynomial proof usage (see mplelbas 21208 and mpladd 21222). 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 40287*	Lemma for fsuppssind 40289. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, ((𝐹 ↾ 𝑆)‘𝑥), 0 )))
Theorem	fsuppssindlem2 40288*	Lemma for fsuppssind 40289. Write a function as a union. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻)))
Theorem	fsuppssind 40289*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support (see fsuppind 40286) 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 40290*	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)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐺)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐺)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ 𝐺)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐺)
Theorem	mhphflem 40291*	Lemma for mhphf 40292. 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 40292	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.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf2 40293	A homogeneous polynomial defines a homogeneous function; this is mhphf 40292 with simpler notation in the conclusion in exchange for a complex definition of ∙, which is based on frlmvscafval 20982 but without the finite support restriction (frlmpws 20966, frlmbas 20971) on the assignments 𝐴 from variables to values. TODO?: Polynomials (df-mpl 21123) 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‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf3 40294	A homogeneous polynomial defines a homogeneous function; this is mhphf2 40293 with the finite support restriction (frlmpws 20966, frlmbas 20971) on the assignments 𝐴 from variables to values. See comment of mhphf2 40293. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐹 = (𝑆 freeLMod 𝐼)    &   ⊢ 𝑀 = (Base‘𝐹)    &   ⊢ ∙ = ( ·𝑠 ‘𝐹)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf4 40295	A homogeneous polynomial defines a homogeneous function; this is mhphf3 40294 with evalSub collapsed to eval. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐹 = (𝑆 freeLMod 𝐼)    &   ⊢ 𝑀 = (Base‘𝐹)    &   ⊢ ∙ = ( ·𝑠 ‘𝐹)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
20.26.4  Arithmetic theorems Towards the start of this section are several proofs regarding the different complex number axioms that could be used to prove some results. For example, ax-1rid 10950 is used in mulid1 10982 related theorems, so one could trade off the extra axioms in mulid1 10982 for the axioms needed to prove that something is a real number. Another example is avoiding complex number closure laws by using real number closure laws and then using ax-resscn 10937; in the other direction, real number closure laws can be avoided by using ax-resscn 10937 and then the complex number closure laws. (This only works if the result of (𝐴 + 𝐵) only needs to be a complex number). The natural numbers are especially amenable to axiom reductions, as the set ℕ is the recursive set {1, (1 + 1), ((1 + 1) + 1)}, etc., i.e. the set of numbers formed by only additions of 1. The digits 2 through 9 are defined so that they expand into additions of 1. This makes adding natural numbers conveniently only require the rearrangement of parentheses, as shown with the following: (4 + 3) = 7 ((3 + 1) + (2 + 1)) = (6 + 1) ((((1 + 1) + 1) + 1) + ((1 + 1) + 1)) = ((((((1 + 1) + 1) + 1) + 1) + 1) + 1) This only requires ax-addass 10945, ax-1cn 10938, and ax-addcl 10940. (And in practice, the expression isn't completely expanded into ones.) Multiplication by 1 requires either mulid2i 10989 or (ax-1rid 10950 and 1re 10984) as seen in 1t1e1 12144 and 1t1e1ALT 40299. Multiplying with greater natural numbers uses ax-distr 10947. Still, this takes fewer axioms than adding zero, which is often implicit in theorems such as (9 + 1) = ;10. Adding zero uses almost every complex number axiom, though notably not ax-mulcom 10944 (see readdid1 40399 and readdid2 40393).
Theorem	c0exALT 40296	Alternate proof of c0ex 10978 using more set theory axioms but fewer complex number axioms (add ax-10 2138, ax-11 2155, ax-13 2373, ax-nul 5231, and remove ax-1cn 10938, ax-icn 10939, ax-addcl 10940, and ax-mulcl 10942). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ V
Theorem	0cnALT3 40297	Alternate proof of 0cn 10976 using ax-resscn 10937, ax-addrcl 10941, ax-rnegex 10951, ax-cnre 10953 instead of ax-icn 10939, ax-addcl 10940, ax-mulcl 10942, ax-i2m1 10948. Version of 0cnALT 11218 using ax-1cn 10938 instead of ax-icn 10939. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	elre0re 40298	Specialized version of 0red 10987 without using ax-1cn 10938 and ax-cnre 10953. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
Theorem	1t1e1ALT 40299	Alternate proof of 1t1e1 12144 using a different set of axioms (add ax-mulrcl 10943, ax-i2m1 10948, ax-1ne0 10949, ax-rrecex 10952 and remove ax-resscn 10937, ax-mulcom 10944, ax-mulass 10946, ax-distr 10947). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	remulcan2d 40300	mulcan2d 11618 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))