P. 489 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48801-48900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ringcsectALTV 48801	A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐸 = (Base‘𝑋)    &   ⊢ 𝑆 = (Sect‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingHom 𝑌) ∧ 𝐺 ∈ (𝑌 RingHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸))))
Theorem	ringcinvALTV 48802	An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑁 = (Inv‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹)))
Theorem	ringcisoALTV 48803	An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐼 = (Iso‘𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))
Theorem	ringcbasbasALTV 48804	An element of the base set of the base set of the category of rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝐶 = (RingCatALTV‘𝑈)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ 𝐵) → (Base‘𝑅) ∈ 𝑈)
Theorem	funcringcsetclem1ALTV 48805*	Lemma 1 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋))
Theorem	funcringcsetclem2ALTV 48806*	Lemma 2 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈)
Theorem	funcringcsetclem3ALTV 48807*	Lemma 3 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
Theorem	funcringcsetclem4ALTV 48808*	Lemma 4 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
Theorem	funcringcsetclem5ALTV 48809*	Lemma 5 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑋 RingHom 𝑌)))
Theorem	funcringcsetclem6ALTV 48810*	Lemma 6 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑋 RingHom 𝑌)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻)
Theorem	funcringcsetclem7ALTV 48811*	Lemma 7 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝑅)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋)))
Theorem	funcringcsetclem8ALTV 48812*	Lemma 8 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑅)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌)))
Theorem	funcringcsetclem9ALTV 48813*	Lemma 9 for funcringcsetcALTV 48814. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑅)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑅)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(⟨𝑋, 𝑌⟩(comp‘𝑅)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(⟨(𝐹‘𝑋), (𝐹‘𝑌)⟩(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻)))
Theorem	funcringcsetcALTV 48814*	The "natural forgetful functor" from the category of rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.) (New usage is discouraged.)
⊢ 𝑅 = (RingCatALTV‘𝑈)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))    ⇒   ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)
Theorem	srhmsubcALTVlem1 48815*	Lemma 1 for srhmsubcALTV 48817. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCatALTV‘𝑈)))
Theorem	srhmsubcALTVlem2 48816*	Lemma 2 for srhmsubcALTV 48817. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring    &   ⊢ 𝐶 = (𝑈 ∩ 𝑆)    &   ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠))    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCatALTV‘𝑈))𝑌))
Theorem	srhmsubcALTV 48817*	According to df-subc 17777, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17805 and subcss2 17808). 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 48818*	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 48819*	According to df-subc 17777, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17805 and subcss2 17808). 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 48820*	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 48821*	According to df-subc 17777, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17805 and subcss2 17808). 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 48822*	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 48823*	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 48824*	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 48825*	According to df-subc 17777, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17805 and subcss2 17808). 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 𝐽)))
21.48.19  Basic algebraic structures (extension)
21.48.19.1  Auxiliary theorems
Theorem	eliunxp2 48826*	Membership in a union of Cartesian products over its second component, analogous to eliunxp 5786. (Contributed by AV, 30-Mar-2019.)
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
Theorem	mpomptx2 48827*	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 7476. (Contributed by AV, 30-Mar-2019.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpox2 48828*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7457 allows 𝐴 to be a function of 𝑦, analogous to cbvmpox 7456. (Contributed by AV, 30-Mar-2019.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐷)    &   ⊢ ((𝑦 = 𝑧 ∧ 𝑥 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ 𝐷, 𝑧 ∈ 𝐵 ↦ 𝐸)
Theorem	dmmpossx2 48829*	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 8015. (Contributed by AV, 30-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦})
Theorem	mpoexxg2 48830*	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 8024. (Contributed by AV, 30-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐵 𝐴 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	ovmpordxf 48831*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7513. (Contributed by AV, 30-Mar-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑦𝑆    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpordx 48832*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7513. (Contributed by AV, 30-Mar-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpox2 48833*	The value of an operation class abstraction. Variant of ovmpoga 7517 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐿)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐿 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	fdmdifeqresdif 48834*	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	ofaddmndmap 48835	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 48836	A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐹 = {⟨𝑋, 𝑌⟩}    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊) → 𝐹 ∈ (𝑅 ↑m {𝑋}))
Theorem	fprmappr 48837	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 48838	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 48839	A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.)
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵))
Theorem	2t6m3t4e0 48840	2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.)
⊢ ((2 · 6) − (3 · 4)) = 0
Theorem	ssnn0ssfz 48841*	For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 32886. (Contributed by AV, 30-Sep-2019.)
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛))
Theorem	nn0sumltlt 48842	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) → ((𝑎 + 𝑏) < 𝑐 → 𝑏 < 𝑐))
21.48.19.2  The binomial coefficient operation (extension)
Theorem	bcpascm1 48843	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 48844*	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 48843) instead of the binomial theorem (binom 15793), see altgsumbcALT 48845. (Contributed by AV, 13-Sep-2019.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)
Theorem	altgsumbcALT 48845*	Alternate proof of altgsumbc 48844, using Pascal's rule (bcpascm1 48843) instead of the binomial theorem (binom 15793). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)
21.48.19.3  The ` ZZ `-module ` ZZ X. ZZ `
Theorem	zlmodzxzlmod 48846	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 48847	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 48848	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 48849	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 48850	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 48851	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 48852	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, (𝐶 − 𝐷)⟩})
21.48.19.4  Group sum operation (extension 2)
Theorem	mgpsumunsn 48853*	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 48854*	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 48855*	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 (𝑘 ∈ (𝑁 ∖ {𝐼}) ↦ 𝐴)))
21.48.19.5  Symmetric groups (extension)
Theorem	exple2lt6 48856	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 48857	Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) ≤ 2) → 𝐺 ∈ Abel)
Theorem	pgrpgt2nabl 48858	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)
21.48.19.6  Divisibility (extension)
Theorem	invginvrid 48859	Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑁‘𝑌) · ((𝐼‘(𝑁‘𝑌)) · 𝑋)) = 𝑋)
21.48.19.7  The support of functions (extension)
Theorem	rmsupp0 48860*	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 48861*	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 48862*	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	scmsuppss 48863*	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‘𝑆)))
21.48.19.8  Finitely supported functions (extension)
Theorem	rmsuppfi 48864*	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 48865*	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	scmsuppfi 48866*	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 48867*	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 48868*	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 48869*	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 48870*	A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
21.48.19.9  Left modules (extension)
Theorem	lmodvsmdi 48871	Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ ↑ = (.g‘𝑊)    &   ⊢ 𝐸 = (.g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋))
Theorem	gsumlsscl 48872*	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 (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) ∈ 𝑍))
21.48.19.10  Associative algebras (extension)
Theorem	assaascl0 48873	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 48874	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‘𝑊))
21.48.19.11  Univariate polynomials (extension)
Theorem	ply1vr1smo 48875	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	ply1sclrmsm 48876	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	coe1sclmulval 48877	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 48878*	Lemma 1 for ply1mulgsum 48882. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅))))
Theorem	ply1mulgsumlem2 48879*	Lemma 2 for ply1mulgsum 48882. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅)))
Theorem	ply1mulgsumlem3 48880*	Lemma 3 for ply1mulgsum 48882. (Contributed by AV, 20-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙)))))) finSupp (0g‘𝑅))
Theorem	ply1mulgsumlem4 48881*	Lemma 4 for ply1mulgsum 48882. (Contributed by AV, 19-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∗ = (.r‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑅 Σg (𝑙 ∈ (0...𝑘) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑘 − 𝑙))))) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃))
Theorem	ply1mulgsum 48882*	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 48883	Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ CRing → ((𝑂‘𝑍)‘ 0 ) = 0 )
Theorem	evl1at1 48884	Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (1r‘𝑃)    ⇒   ⊢ (𝑅 ∈ CRing → ((𝑂‘𝐼)‘ 1 ) = 1 )
21.48.19.12  Univariate polynomials (examples)
Theorem	linply1 48885	A term of the form 𝑥 − 𝐶 is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 26155). (Contributed by AV, 3-Jul-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐵)
Theorem	lineval 48886	A term of the form 𝑥 − 𝐶 evaluated for 𝑥 = 𝑉 results in 𝑉 − 𝐶 (part of ply1remlem 26155). (Contributed by AV, 3-Jul-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝑉) = (𝑉(-g‘𝑅)𝐶))
Theorem	linevalexample 48887	The polynomial 𝑥 − 3 over ℤ evaluated for 𝑥 = 5 results in 2. (Contributed by AV, 3-Jul-2019.)
⊢ 𝑃 = (Poly1‘ℤring)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘ℤring)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐺 = (𝑋 − (𝐴‘3))    &   ⊢ 𝑂 = (eval1‘ℤring)    ⇒   ⊢ ((𝑂‘(𝑋 − (𝐴‘3)))‘5) = 2
21.48.20  Linear algebra (extension)
21.48.20.1  The subalgebras of diagonal and scalar matrices (extension) In the following, alternative definitions for diagonal and scalar matrices are provided. These definitions define diagonal and scalar matrices as extensible structures, whereas Definitions df-dmat 22480 and df-scmat 22481 define diagonal and scalar matrices as sets.
Syntax	cdmatalt 48888	Alternative notation for the algebra of diagonal matrices.
class DMatALT
Syntax	cscmatalt 48889	Alternative notation for the algebra of scalar matrices.
class ScMatALT
Definition	df-dmatalt 48890*	Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in [Roman] p. 4 or Definition 3.12 in [Hefferon] p. 240. (Contributed by AV, 8-Dec-2019.)
⊢ DMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}))
Definition	df-scmatalt 48891*	Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in [Connell] p. 57: "A scalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cIn";. (Contributed by AV, 8-Dec-2019.)
⊢ ScMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))}))
Theorem	dmatALTval 48892*	The algebra of 𝑁 x 𝑁 diagonal matrices over a ring 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMatALT 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐷 = (𝐴 ↾s {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}))
Theorem	dmatALTbas 48893*	The base set of the algebra of 𝑁 x 𝑁 diagonal matrices over a ring 𝑅, i.e. the set of all 𝑁 x 𝑁 diagonal matrices over the ring 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMatALT 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐷) = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )})
Theorem	dmatALTbasel 48894*	An element of the base set of the algebra of 𝑁 x 𝑁 diagonal matrices over a ring 𝑅, i.e. an 𝑁 x 𝑁 diagonal matrix over the ring 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMatALT 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑀 ∈ (Base‘𝐷) ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ))))
Theorem	dmatbas 48895	The set of all 𝑁 x 𝑁 diagonal matrices over (the ring) 𝑅 is the base set of the algebra of 𝑁 x 𝑁 diagonal matrices over (the ring) 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = (Base‘(𝑁 DMatALT 𝑅)))
21.48.20.2  Linear combinations According to Wikipedia ("Linear combination", 29-Mar-2019, https://en.wikipedia.org/wiki/Linear_combination) "In mathematics, a linear combination is an expression constructed from a set of terms by multiplying each term by a constant and adding the results (e.g., a linear combination of x and y would be any expression of the form ax + by, where a and b are constants). The concept of linear combinations is central to linear algebra and related fields of mathematics." In linear algebra, these "terms" are "vectors" (elements from vector spaces or left modules), and the constants are elements of the underlying field resp. ring. This corresponds to the definition in [Lang] p. 129: "Let M be a module over a ring A and let S be a subset of M. By a linear combination of elements of S (with coefficients in A) one means a sum ∑x ∈S axx where {ax} is a set of elements of A, ...". In the definition in [Lang] p. 129, it is additionally claimed that "..., almost all of which [elements of A] are equal to 0.". This is not necessarily required in the following definition df-linc 48898, but it is essential if additions and scalar multiplications of linear combinations are considered. Therefore, we define the set of all linear combinations with finite support in df-lco 48899, so that we can show that such sets are submodules of the corresponding modules, see lincolss 48926. Remark:According to Wikipedia ("Linear span", 28-Apr-2019, https://en.wikipedia.org/wiki/Linear_span 48926) "In linear algebra, the linear span (also called the linear hull or just span) of a set of vectors in a vector space [or module] is the intersection of all linear subspaces which each contain every vector in that set.", and "Alternately, the span of [a set] S may be defined as the set of all finite linear combinations of elements (vectors) of S". Whereas spans are defined according to the first approach in df-lsp 20969, the set of all linear combinations as defined by df-lco 48899 follows the alternative approach. That both definitions are equivalent is shown by lspeqlco 48931.
Syntax	clinc 48896	Extend class notation with the operation constructing a linear combination (of vectors from a left module).
class linC
Syntax	clinco 48897	Extend class notation with the operation constructing a set of linear combinations (of vectors from a left module) with finite support.
class LinCo
Definition	df-linc 48898*	Define the operation constructing a linear combination. Although this definition is taylored for linear combinations of vectors from left modules, it can be used for any structure having a Base, Scalar s and a scalar multiplication ·𝑠. (Contributed by AV, 29-Mar-2019.)
⊢ linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑚)𝑥)))))
Definition	df-lco 48899*	Define the operation constructing the set of all linear combinations for a set of vectors. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 28-Jul-2019.)
⊢ LinCo = (𝑚 ∈ V, 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp (0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))})
Theorem	lincop 48900*	A linear combination as operation. (Contributed by AV, 30-Mar-2019.)
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠 ‘𝑀)𝑥)))))