P. 448 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44701-44800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sringcat 44701*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	crhmsubc 44702*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	cringcat 44703*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	drhmsubc 44704*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
Theorem	drngcat 44705*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	fldcat 44706*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCat‘𝑈) ↾cat 𝐹) ∈ Cat)
Theorem	fldc 44707*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → (((RingCat‘𝑈) ↾cat 𝐽) ↾cat 𝐹) ∈ Cat)
Theorem	fldhmsubc 44708*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐹 ∈ (Subcat‘((RingCat‘𝑈) ↾cat 𝐽)))
Theorem	rngcrescrhm 44709	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑅) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rhmsubclem1 44710	Lemma 1 for rhmsubc 44714. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅))
Theorem	rhmsubclem2 44711	Lemma 2 for rhmsubc 44714. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	rhmsubclem3 44712*	Lemma 3 for rhmsubc 44714. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCat‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubclem4 44713*	Lemma 4 for rhmsubc 44714. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubc 44714	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCat‘𝑈)))
Theorem	rhmsubccat 44715	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCat‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → ((RngCat‘𝑈) ↾cat 𝐻) ∈ Cat)
Theorem	srhmsubcALTVlem1 44716*	Lemma 1 for srhmsubcALTV 44718. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCatALTV‘𝑈)))
Theorem	srhmsubcALTVlem2 44717*	Lemma 2 for srhmsubcALTV 44718. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCatALTV‘𝑈))𝑌))
Theorem	srhmsubcALTV 44718*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCatALTV‘𝑈)))
Theorem	sringcatALTV 44719*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCatALTV‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	crhmsubcALTV 44720*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCatALTV‘𝑈)))
Theorem	cringcatALTV 44721*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ CRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCatALTV‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	drhmsubcALTV 44722*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐽 ∈ (Subcat‘(RingCatALTV‘𝑈)))
Theorem	drngcatALTV 44723*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCatALTV‘𝑈) ↾cat 𝐽) ∈ Cat)
Theorem	fldcatALTV 44724*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((RingCatALTV‘𝑈) ↾cat 𝐹) ∈ Cat)
Theorem	fldcALTV 44725*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → (((RingCatALTV‘𝑈) ↾cat 𝐽) ↾cat 𝐹) ∈ Cat)
Theorem	fldhmsubcALTV 44726*	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (𝑈 ∩ DivRing)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    &   ⊢ 𝐷 = (𝑈 ∩ Field)    &   ⊢ 𝐹 = (𝑟 ∈ 𝐷, 𝑠 ∈ 𝐷 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝐹 ∈ (Subcat‘((RingCatALTV‘𝑈) ↾cat 𝐽)))
Theorem	rngcrescrhmALTV 44727	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑅) sSet ⟨(Hom ‘ndx), 𝐻⟩))
Theorem	rhmsubcALTVlem1 44728	Lemma 1 for rhmsubcALTV 44732. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅))
Theorem	rhmsubcALTVlem2 44729	Lemma 2 for rhmsubcALTV 44732. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌))
Theorem	rhmsubcALTVlem3 44730*	Lemma 3 for rhmsubcALTV 44732. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥))
Theorem	rhmsubcALTVlem4 44731*	Lemma 4 for rhmsubcALTV 44732. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(RngCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Theorem	rhmsubcALTV 44732	According to df-subc 17074, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17102 and subcss2 17105). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Subcat‘(RngCatALTV‘𝑈)))
Theorem	rhmsubcALTVcat 44733	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) (New usage is discouraged.)
⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ 𝐶 = (RngCatALTV‘𝑈)    &   ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))    &   ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅))    ⇒   ⊢ (𝜑 → ((RngCatALTV‘𝑈) ↾cat 𝐻) ∈ Cat)
20.41.20  Basic algebraic structures (extension)
20.41.20.1  Auxiliary theorems
Theorem	opeliun2xp 44734	Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 5583. (Contributed by AV, 30-Mar-2019.)
⊢ (⟨𝐶, 𝑦⟩ ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴))
Theorem	eliunxp2 44735*	Membership in a union of Cartesian products over its second component, analogous to eliunxp 5672. (Contributed by AV, 30-Mar-2019.)
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
Theorem	mpomptx2 44736*	Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐴(𝑦) is not assumed to be constant w.r.t 𝑦, analogous to mpomptx 7244. (Contributed by AV, 30-Mar-2019.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpox2 44737*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7227 allows 𝐴 to be a function of 𝑦, analogous to cbvmpox 7226. (Contributed by AV, 30-Mar-2019.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐷)    &   ⊢ ((𝑦 = 𝑧 ∧ 𝑥 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ 𝐷, 𝑧 ∈ 𝐵 ↦ 𝐸)
Theorem	dmmpossx2 44738*	The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpossx 7746. (Contributed by AV, 30-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦})
Theorem	mpoexxg2 44739*	Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpoexxg 7756. (Contributed by AV, 30-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐵 𝐴 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	ovmpordxf 44740*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7279. (Contributed by AV, 30-Mar-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑦𝑆    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpordx 44741*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7279. (Contributed by AV, 30-Mar-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpox2 44742*	The value of an operation class abstraction. Variant of ovmpoga 7283 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐿)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐿 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	fdmdifeqresdif 44743*	The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝑌, 𝑋, (𝐺‘𝑥)))    ⇒   ⊢ (𝐺:(𝐷 ∖ {𝑌})⟶𝑅 → 𝐺 = (𝐹 ↾ (𝐷 ∖ {𝑌})))
Theorem	offvalfv 44744*	The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
Theorem	ofaddmndmap 44745	The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f + 𝐵) ∈ (𝑅 ↑m 𝑉))
Theorem	mapsnop 44746	A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐹 = {⟨𝑋, 𝑌⟩}    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊) → 𝐹 ∈ (𝑅 ↑m {𝑋}))
Theorem	fprmappr 44747	A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024.)
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ∈ (𝑋 ↑m {𝐴, 𝐵}))
Theorem	mapprop 44748	An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.) (Proof shortened by AV, 2-Jun-2024.)
⊢ 𝐹 = {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩}    ⇒   ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹 ∈ (𝑅 ↑m {𝑋, 𝑌}))
Theorem	ztprmneprm 44749	A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.)
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵))
Theorem	2t6m3t4e0 44750	2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.)
⊢ ((2 · 6) − (3 · 4)) = 0
Theorem	ssnn0ssfz 44751*	For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 30536. (Contributed by AV, 30-Sep-2019.)
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛))
Theorem	nn0sumltlt 44752	If the sum of two nonnegative integers is less than a third integer, then one of the summands is already less than this third integer. (Contributed by AV, 19-Oct-2019.)
⊢ ((𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0) → ((𝑎 + 𝑏) < 𝑐 → 𝑏 < 𝑐))
20.41.20.2  The binomial coefficient operation (extension)
Theorem	bcpascm1 44753	Pascal's rule for the binomial coefficient, generalized to all integers 𝐾, shifted down by 1. (Contributed by AV, 8-Sep-2019.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (((𝑁 − 1)C𝐾) + ((𝑁 − 1)C(𝐾 − 1))) = (𝑁C𝐾))
Theorem	altgsumbc 44754*	The sum of binomial coefficients for a fixed positive 𝑁 with alternating signs is zero. Notice that this is not valid for 𝑁 = 0 (since ((-1↑0) · (0C0)) = (1 · 1) = 1). For a proof using Pascal's rule (bcpascm1 44753) instead of the binomial theorem (binom 15177) , see altgsumbcALT 44755. (Contributed by AV, 13-Sep-2019.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)
Theorem	altgsumbcALT 44755*	Alternate proof of altgsumbc 44754, using Pascal's rule (bcpascm1 44753) instead of the binomial theorem (binom 15177). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)
20.41.20.3  The ` ZZ `-module ` ZZ X. ZZ `
Theorem	zlmodzxzlmod 44756	The ℤ-module ℤ × ℤ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    ⇒   ⊢ (𝑍 ∈ LMod ∧ ℤring = (Scalar‘𝑍))
Theorem	zlmodzxzel 44757	An element of the (base set of the) ℤ-module ℤ × ℤ. (Contributed by AV, 21-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∈ (Base‘𝑍))
Theorem	zlmodzxz0 44758	The 0 of the ℤ-module ℤ × ℤ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    ⇒   ⊢ 0 = (0g‘𝑍)
Theorem	zlmodzxzscm 44759	The scalar multiplication of the ℤ-module ℤ × ℤ. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {⟨0, 𝐵⟩, ⟨1, 𝐶⟩}) = {⟨0, (𝐴 · 𝐵)⟩, ⟨1, (𝐴 · 𝐶)⟩})
Theorem	zlmodzxzadd 44760	The addition of the ℤ-module ℤ × ℤ. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ + = (+g‘𝑍)    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ({⟨0, 𝐴⟩, ⟨1, 𝐶⟩} + {⟨0, 𝐵⟩, ⟨1, 𝐷⟩}) = {⟨0, (𝐴 + 𝐵)⟩, ⟨1, (𝐶 + 𝐷)⟩})
Theorem	zlmodzxzsubm 44761	The subtraction of the ℤ-module ℤ × ℤ expressed as addition. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ − = (-g‘𝑍)    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ({⟨0, 𝐴⟩, ⟨1, 𝐶⟩} − {⟨0, 𝐵⟩, ⟨1, 𝐷⟩}) = ({⟨0, 𝐴⟩, ⟨1, 𝐶⟩} (+g‘𝑍)(-1( ·𝑠 ‘𝑍){⟨0, 𝐵⟩, ⟨1, 𝐷⟩})))
Theorem	zlmodzxzsub 44762	The subtraction of the ℤ-module ℤ × ℤ. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ − = (-g‘𝑍)    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ({⟨0, 𝐴⟩, ⟨1, 𝐶⟩} − {⟨0, 𝐵⟩, ⟨1, 𝐷⟩}) = {⟨0, (𝐴 − 𝐵)⟩, ⟨1, (𝐶 − 𝐷)⟩})
20.41.20.4  Group sum operation (extension 2)
Theorem	mgpsumunsn 44763*	Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (Contributed by AV, 29-Dec-2018.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅))    &   ⊢ (𝑘 = 𝐼 → 𝐴 = 𝑋)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝑁 ↦ 𝐴)) = ((𝑀 Σg (𝑘 ∈ (𝑁 ∖ {𝐼}) ↦ 𝐴)) · 𝑋))
Theorem	mgpsumz 44764*	If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅))    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝑘 = 𝐼 → 𝐴 = 0 )    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝑁 ↦ 𝐴)) = 0 )
Theorem	mgpsumn 44765*	If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (Contributed by AV, 29-Dec-2018.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ (Base‘𝑅))    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝑘 = 𝐼 → 𝐴 = 1 )    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝑁 ↦ 𝐴)) = (𝑀 Σg (𝑘 ∈ (𝑁 ∖ {𝐼}) ↦ 𝐴)))
20.41.20.5  Symmetric groups (extension)
Theorem	exple2lt6 44766	A nonnegative integer to the power of itself is less than 6 if it is less than or equal to 2. (Contributed by AV, 16-Mar-2019.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2) → (𝑁↑𝑁) < 6)
Theorem	pgrple2abl 44767	Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) ≤ 2) → 𝐺 ∈ Abel)
Theorem	pgrpgt2nabl 44768	Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 2 < (♯‘𝐴)) → 𝐺 ∉ Abel)
20.41.20.6  Divisibility (extension)
Theorem	invginvrid 44769	Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑁‘𝑌) · ((𝐼‘(𝑁‘𝑌)) · 𝑋)) = 𝑋)
20.41.20.7  The support of functions (extension)
Theorem	rmsupp0 44770*	The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = ∅)
Theorem	domnmsuppn0 44771*	The support of a mapping of a multiplication of a nonzero constant with a function into a (ring theoretic) domain equals the support of the function. (Contributed by AV, 11-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋) ∧ (𝐶 ∈ 𝑅 ∧ 𝐶 ≠ (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = (𝐴 supp (0g‘𝑀)))
Theorem	rmsuppss 44772*	The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑀)))
Theorem	mndpsuppss 44773	The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f (+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))))
Theorem	scmsuppss 44774*	The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.)
⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑆)))
20.41.20.8  Finitely supported functions (extension)
Theorem	rmsuppfi 44775*	The support of a mapping of a multiplication of a constant with a function into a ring is finite if the support of the function is finite. (Contributed by AV, 11-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (𝐴 supp (0g‘𝑀)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ∈ Fin)
Theorem	rmfsupp 44776*	A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by AV, 9-Jun-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp (0g‘𝑀)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) finSupp (0g‘𝑀))
Theorem	mndpsuppfi 44777	The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ ((𝐴 supp (0g‘𝑀)) ∈ Fin ∧ (𝐵 supp (0g‘𝑀)) ∈ Fin)) → ((𝐴 ∘f (+g‘𝑀)𝐵) supp (0g‘𝑀)) ∈ Fin)
Theorem	mndpfsupp 44778	A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑀) ∧ 𝐵 finSupp (0g‘𝑀))) → (𝐴 ∘f (+g‘𝑀)𝐵) finSupp (0g‘𝑀))
Theorem	scmsuppfi 44779*	The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.)
⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (𝐴 supp (0g‘𝑆)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ∈ Fin)
Theorem	scmfsupp 44780*	A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.)
⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝑅 = (Base‘𝑆)    ⇒   ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) finSupp (0g‘𝑀))
Theorem	suppmptcfin 44781*	The support of a mapping with value 0 except of one is finite. (Contributed by AV, 27-Apr-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 ))    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) ∈ Fin)
Theorem	mptcfsupp 44782*	A mapping with value 0 except of one is finitely supported. (Contributed by AV, 9-Jun-2019.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 ))    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 𝐹 finSupp 0 )
Theorem	fsuppmptdmf 44783*	A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
20.41.20.9  Left modules (extension)
Theorem	lmodvsmdi 44784	Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘𝑊)    &   ⊢ 𝐸 = (.g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))
Theorem	gsumlsscl 44785*	Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (Scalar‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → ((𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) ∈ 𝑍))
20.41.20.10  Associative algebras (extension)
Theorem	ascl1 44786	The scalar 1 embedded into a left module corresponds to the 1 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑊 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐴‘(1r‘𝐹)) = (1r‘𝑊))
Theorem	assaascl0 44787	The scalar 0 embedded into an associative algebra corresponds to the 0 of the associative algebra. (Contributed by AV, 31-Jul-2019.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    ⇒   ⊢ (𝜑 → (𝐴‘(0g‘𝐹)) = (0g‘𝑊))
Theorem	assaascl1 44788	The scalar 1 embedded into an associative algebra corresponds to the 1 of the an associative algebra. (Contributed by AV, 31-Jul-2019.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    ⇒   ⊢ (𝜑 → (𝐴‘(1r‘𝐹)) = (1r‘𝑊))
20.41.20.11  Univariate polynomials (extension)
Theorem	ply1vr1smo 44789	The variable in a polynomial expressed as scaled monomial. (Contributed by AV, 12-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝑋 = (var1‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → ( 1 · (1 ↑ 𝑋)) = 𝑋)
Theorem	ply1ass23l 44790	Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌)))
Theorem	ply1sclrmsm 44791	The ring multiplication of a polynomial with a scalar polynomial is equal to the scalar multiplication of the polynomial with the corresponding scalar. (Contributed by AV, 14-Aug-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ × = (.r‘𝑃)    &   ⊢ 𝑁 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑁)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸) → ((𝐴‘𝐹) × 𝑍) = (𝐹 · 𝑍))
Theorem	coe1id 44792*	Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐼 = (1r‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (coe1‘𝐼) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, 1 , 0 )))
Theorem	coe1sclmulval 44793	The value of the coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by AV, 14-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝑆 = ( ·𝑠 ‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵) ∧ 𝑁 ∈ ℕ0) → ((coe1‘(𝑌𝑆𝑍))‘𝑁) = (𝑌 · ((coe1‘𝑍)‘𝑁)))
Theorem	ply1mulgsumlem1 44794*	Lemma 1 for ply1mulgsum 44798. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))
Theorem	ply1mulgsumlem2 44795*	Lemma 2 for ply1mulgsum 44798. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))
Theorem	ply1mulgsumlem3 44796*	Lemma 3 for ply1mulgsum 44798. (Contributed by AV, 20-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅))
Theorem	ply1mulgsumlem4 44797*	Lemma 4 for ply1mulgsum 44798. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃))
Theorem	ply1mulgsum 44798*	The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝐾 × 𝐿) = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋)))))
Theorem	evl1at0 44799	Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ CRing → ((𝑂‘𝑍)‘ 0 ) = 0 )
Theorem	evl1at1 44800	Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (1r‘𝑃)    ⇒   ⊢ (𝑅 ∈ CRing → ((𝑂‘𝐼)‘ 1 ) = 1 )