P. 219 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21801-21900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ply1sclid 21801	Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → 𝑋 = ((coe1‘(𝐴‘𝑋))‘0))
Theorem	ply1sclf1 21802	The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐴:𝐾–1-1→𝐵)
Theorem	ply1scl0 21803	The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑌 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐴‘ 0 ) = 𝑌)
Theorem	ply1scl0OLD 21804	Obsolete version of ply1scl1 21806 as of 12-Mar-2025. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑌 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐴‘ 0 ) = 𝑌)
Theorem	ply1scln0 21805	Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑌 = (0g‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → (𝐴‘𝑋) ≠ 𝑌)
Theorem	ply1scl1 21806	The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015.) (Proof shortened by SN, 12-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐴‘ 1 ) = 𝑁)
Theorem	ply1scl1OLD 21807	Obsolete version of ply1scl1 21806 as of 12-Mar-2025. (Contributed by Stefan O'Rear, 1-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑁 = (1r‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐴‘ 1 ) = 𝑁)
Theorem	ply1idvr1 21808	The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑁)    ⇒   ⊢ (𝑅 ∈ Ring → (0 ↑ 𝑋) = (1r‘𝑃))
Theorem	cply1mul 21809*	The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ × = (.r‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (∀𝑐 ∈ ℕ (((coe1‘𝐹)‘𝑐) = 0 ∧ ((coe1‘𝐺)‘𝑐) = 0 ) → ∀𝑐 ∈ ℕ ((coe1‘(𝐹 × 𝐺))‘𝑐) = 0 ))
Theorem	ply1coefsupp 21810*	The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 21811. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ 𝐴 = (coe1‘𝐾)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃))
Theorem	ply1coe 21811*	Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 7-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ 𝐴 = (coe1‘𝐾)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
Theorem	eqcoe1ply1eq 21812*	Two polynomials over the same ring are equal if they have identical coefficients. (Contributed by AV, 7-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∀𝑘 ∈ ℕ0 (𝐴‘𝑘) = (𝐶‘𝑘) → 𝐾 = 𝐿))
Theorem	ply1coe1eq 21813*	Two polynomials over the same ring are equal iff they have identical coefficients. (Contributed by AV, 13-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (coe1‘𝐾)    &   ⊢ 𝐶 = (coe1‘𝐿)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → (∀𝑘 ∈ ℕ0 (𝐴‘𝑘) = (𝐶‘𝑘) ↔ 𝐾 = 𝐿))
Theorem	cply1coe0 21814*	All but the first coefficient of a constant polynomial ( i.e. a "lifted scalar") are zero. (Contributed by AV, 16-Nov-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾) → ∀𝑛 ∈ ℕ ((coe1‘(𝐴‘𝑆))‘𝑛) = 0 )
Theorem	cply1coe0bi 21815*	A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient are zero. (Contributed by AV, 16-Nov-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ 𝐾 𝑀 = (𝐴‘𝑠) ↔ ∀𝑛 ∈ ℕ ((coe1‘𝑀)‘𝑛) = 0 ))
Theorem	coe1fzgsumdlem 21816*	Lemma for coe1fzgsumd 21817 (induction step). (Contributed by AV, 8-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))
Theorem	coe1fzgsumd 21817*	Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾))))
Theorem	gsumsmonply1 21818*	A finite group sum of scaled monomials is a univariate polynomial. (Contributed by AV, 8-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))) ∈ 𝐵)
Theorem	gsummoncoe1 21819*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 )    &   ⊢ (𝜑 → 𝐿 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = ⦋𝐿 / 𝑘⦌𝐴)
Theorem	gsumply1eq 21820*	Two univariate polynomials given as (finitely supported) sum of scaled monomials are equal iff the corresponding coefficients are equal. (Contributed by AV, 21-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐴) finSupp 0 )    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐵 ∈ 𝐾)    &   ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐵) finSupp 0 )    &   ⊢ (𝜑 → 𝑂 = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))    &   ⊢ (𝜑 → 𝑄 = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐵 ∗ (𝑘 ↑ 𝑋)))))    ⇒   ⊢ (𝜑 → (𝑂 = 𝑄 ↔ ∀𝑘 ∈ ℕ0 𝐴 = 𝐵))
Theorem	lply1binom 21821*	The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings: (𝑋 + 𝐴)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝑋↑𝑘)). (Contributed by AV, 25-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = (.g‘𝑃)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵) → (𝑁 ↑ (𝑋 + 𝐴)) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝑋))))))
Theorem	lply1binomsc 21822*	The binomial theorem for linear polynomials (monic polynomials of degree 1) over commutative rings, expressed by an element of this ring: (𝑋 + 𝐴)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝑋↑𝑘)). (Contributed by AV, 25-Aug-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ × = (.r‘𝑃)    &   ⊢ · = (.g‘𝑃)    &   ⊢ 𝐺 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾) → (𝑁 ↑ (𝑋 + (𝑆‘𝐴))) = (𝑃 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · ((𝑆‘((𝑁 − 𝑘)𝐸𝐴)) × (𝑘 ↑ 𝑋))))))
11.3.5  Univariate polynomial evaluation
Syntax	ces1 21823	Evaluation of a univariate polynomial in a subring.
class evalSub1
Syntax	ce1 21824	Evaluation of a univariate polynomial.
class eval1
Definition	df-evls1 21825*	Define the evaluation map for the univariate polynomial algebra. The function (𝑆 evalSub1 𝑅):𝑉⟶(𝑆 ↑m 𝑆) makes sense when 𝑆 is a ring and 𝑅 is a subring of 𝑆, and where 𝑉 is the set of polynomials in (Poly1‘𝑅). This function maps an element of the formal polynomial algebra (with coefficients in 𝑅) to a function from assignments to the variable from 𝑆 into an element of 𝑆 formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
Definition	df-evl1 21826*	Define the evaluation map for the univariate polynomial algebra. The function (eval1‘𝑅):𝑉⟶(𝑅 ↑m 𝑅) makes sense when 𝑅 is a ring, and 𝑉 is the set of polynomials in (Poly1‘𝑅). This function maps an element of the formal polynomial algebra (with coefficients in 𝑅) to a function from assignments to the variable from 𝑅 into an element of 𝑅 formed by evaluating the polynomial with the given assignment. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ eval1 = (𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ (1o eval 𝑟)))
Theorem	reldmevls1 21827	Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.)
⊢ Rel dom evalSub1
Theorem	ply1frcl 21828	Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.)
⊢ 𝑄 = ran (𝑆 evalSub1 𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → (𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 (Base‘𝑆)))
Theorem	evls1fval 21829*	Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐸 = (1o evalSub 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))
Theorem	evls1val 21830*	Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐸 = (1o evalSub 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (1o mPoly (𝑆 ↾s 𝑅))    &   ⊢ 𝐾 = (Base‘𝑀)    ⇒   ⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆) ∧ 𝐴 ∈ 𝐾) → (𝑄‘𝐴) = (((𝐸‘𝑅)‘𝐴) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))))
Theorem	evls1rhmlem 21831*	Lemma for evl1rhm 21842 and evls1rhm 21832 (formerly part of the proof of evl1rhm 21842): The first function of the composition forming the univariate polynomial evaluation map function for a (sub)ring is a ring homomorphism. (Contributed by AV, 11-Sep-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑇 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))))    ⇒   ⊢ (𝑅 ∈ CRing → 𝐹 ∈ ((𝑅 ↑s (𝐵 ↑m 1o)) RingHom 𝑇))
Theorem	evls1rhm 21832	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑇 = (𝑆 ↑s 𝐵)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    ⇒   ⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom 𝑇))
Theorem	evls1sca 21833	Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝐵 × {𝑋}))
Theorem	evls1gsumadd 21834*	Univariate polynomial evaluation maps (additive) group sums to group sums. (Contributed by AV, 14-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evls1gsummul 21835*	Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 14-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (𝑆 ↑s 𝐾)    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝐺 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝐻 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evls1pw 21836	Univariate polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑆 ↑s 𝐾)))(𝑄‘𝑋)))
Theorem	evls1varpw 21837	Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑆 ↑s 𝐵)))(𝑄‘𝑋)))
Theorem	evl1fval 21838*	Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑄 = (1o eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝑂 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ 𝑄)
Theorem	evl1val 21839*	Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑄 = (1o eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (1o mPoly 𝑅)    &   ⊢ 𝐾 = (Base‘𝑀)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ 𝐾) → (𝑂‘𝐴) = ((𝑄‘𝐴) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))))
Theorem	evl1fval1lem 21840	Lemma for evl1fval1 21841. (Contributed by AV, 11-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑄 = (𝑅 evalSub1 𝐵))
Theorem	evl1fval1 21841	Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝑄 = (𝑅 evalSub1 𝐵)
Theorem	evl1rhm 21842	Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015.) (Proof shortened by AV, 13-Sep-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑇 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom 𝑇))
Theorem	fveval1fvcl 21843	The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑌) ∈ 𝐵)
Theorem	evl1sca 21844	Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑂‘(𝐴‘𝑋)) = (𝐵 × {𝑋}))
Theorem	evl1scad 21845	Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝑈 ∧ ((𝑂‘(𝐴‘𝑋))‘𝑌) = 𝑋))
Theorem	evl1var 21846	Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐵))
Theorem	evl1vard 21847	Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ ((𝑂‘𝑋)‘𝑌) = 𝑌))
Theorem	evls1var 21848	Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑋 = (var1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → (𝑄‘𝑋) = ( I ↾ 𝐵))
Theorem	evls1scasrng 21849	The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 13-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑂 = (eval1‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐶 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝑂‘(𝐶‘𝑋)))
Theorem	evls1varsrng 21850	The evaluation of the variable of univariate polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑂 = (eval1‘𝑆)    &   ⊢ 𝑉 = (var1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → (𝑄‘𝑉) = (𝑂‘𝑉))
Theorem	evl1addd 21851	Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊)))
Theorem	evl1subd 21852	Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐷 = (-g‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊)))
Theorem	evl1muld 21853	Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊)))
Theorem	evl1vsd 21854	Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ ∙ = ( ·𝑠 ‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉)))
Theorem	evl1expd 21855	Polynomial evaluation builder for an exponential. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ ∙ = (.g‘(mulGrp‘𝑃))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 ↑ 𝑉)))
Theorem	pf1const 21856	Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄)
Theorem	pf1id 21857	The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄)
Theorem	pf1subrg 21858	Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑄 ∈ (SubRing‘(𝑅 ↑s 𝐵)))
Theorem	pf1rcl 21859	Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing)
Theorem	pf1f 21860	Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵)
Theorem	mpfpf1 21861*	Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = ran (1o eval 𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄)
Theorem	pf1mpf 21862*	Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = ran (1o eval 𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦ (𝑥‘∅))) ∈ 𝐸)
Theorem	pf1addcl 21863	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄)
Theorem	pf1mulcl 21864	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄)
Theorem	pf1ind 21865*	Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁)    &   ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎)    &   ⊢ (𝑥 = (𝐵 × {𝑓}) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = ( I ↾ 𝐵) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂))    &   ⊢ (𝑥 = (𝑓 ∘f + 𝑔) → (𝜓 ↔ 𝜁))    &   ⊢ (𝑥 = (𝑓 ∘f · 𝑔) → (𝜓 ↔ 𝜎))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑄)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	evl1gsumdlem 21866*	Lemma for evl1gsumd 21867 (induction step). (Contributed by AV, 17-Sep-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))))
Theorem	evl1gsumd 21867*	Polynomial evaluation builder for a finite group sum of polynomials. (Contributed by AV, 17-Sep-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((𝑂‘𝑀)‘𝑌))))
Theorem	evl1gsumadd 21868*	Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd 21834. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝑃 = (𝑅 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evl1gsumaddval 21869*	Value of a univariate polynomial evaluation mapping an additive group sum to a group sum of the evaluated variable. (Contributed by AV, 17-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝑃 = (𝑅 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌)))‘𝐶) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((𝑄‘𝑌)‘𝐶))))
Theorem	evl1gsummul 21870*	Univariate polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝑃 = (𝑅 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝐻 = (mulGrp‘𝑃)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝐺 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝐻 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evl1varpw 21871	Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 21868, the proof is shorter using evls1varpw 21837 instead of proving it directly. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋)))
Theorem	evl1varpwval 21872	Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑁 ↑ 𝑋))‘𝐶) = (𝑁𝐸𝐶))
Theorem	evl1scvarpw 21873	Univariate polynomial evaluation maps a multiple of an exponentiation of a variable to the multiple of an exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑆 = (𝑅 ↑s 𝐵)    &   ⊢ ∙ = (.r‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ 𝐹 = (.g‘𝑀)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴 × (𝑁 ↑ 𝑋))) = ((𝐵 × {𝐴}) ∙ (𝑁𝐹(𝑄‘𝑋))))
Theorem	evl1scvarpwval 21874	Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴 × (𝑁 ↑ 𝑋)))‘𝐶) = (𝐴 · (𝑁𝐸𝐶)))
Theorem	evl1gsummon 21875*	Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑀 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑊 Σg (𝑥 ∈ 𝑀 ↦ (𝐴 × (𝑁 ↑ 𝑋)))))‘𝐶) = (𝑅 Σg (𝑥 ∈ 𝑀 ↦ (𝐴 · (𝑁𝐸𝐶)))))
11.4  Matrices According to Wikipedia ("Matrix (mathemetics)", 02-Apr-2019, https://en.wikipedia.org/wiki/Matrix_(mathematics)) "A matrix is a rectangular array of numbers or other mathematical objects for which operations such as addition and multiplication are defined. Most commonly, a matrix over a field F is a rectangular array of scalars each of which is a member of F. The numbers, symbols or expressions in the matrix are called its entries or its elements. The horizontal and vertical lines of entries in a matrix are called rows and columns, respectively.", and in the definition of [Lang] p. 503 "By an m x n matrix in [a commutative ring] R one means a doubly indexed family of elements of R, (aij), (i= 1,..., m and j = 1,... n) ... We call the elements aij the coefficients or components of the matrix. A 1 x n matrix is called a row vector (of dimension, or size, n) and a m x 1 matrix is called a column vector (of dimension, or size, m). In general, we say that (m,n) is the size of the matrix, ...". In contrast to these definitions, we denote any free module over a (not necessarily commutative) ring (in the meaning of df-frlm 21293) with a Cartesian product as index set as "matrix". The two sets of the Cartesian product even need neither to be ordered or a range of (nonnegative/positive) integers nor finite. By this, the addition and scalar multiplication for matrices correspond to the addition (see frlmplusgval 21310) and scalar multiplication (see frlmvscafval 21312) for free modules. Actually, there is no definition for (arbitrary) matrices: Even the (general) matrix multiplication can be defined using functions from Cartesian products into a ring (which are elements of the base set of free modules), see df-mamu 21877. Thus, a statement like "Then the set of m x n matrices in R is a module (i.e., an R-module)" as in [Lang] p. 504 follows immediately from frlmlmod 21295. However, for square matrices there is Definition df-mat 21899, defining the algebras of square matrices (of the same size over the same ring), extending the structure of the corresponding free module by the matrix multiplication as ring multiplication. A "usual" matrix (aij), (i = 1,..., m and j = 1,... n) would be represented as an element of (the base set of) (𝑅 freeLMod ((1...𝑚) × (1...𝑛))) and a square matrix (aij), (i = 1,..., n and j = 1,... n) would be represented as an element of (the base set of) ((1...𝑛) Mat 𝑅). Finally, it should be mentioned that our definitions of matrices include the zero-dimensional cases, which are excluded from the definitions of many authors, e.g., in [Lang] p. 503. It is shown in mat0dimbas0 21959 that the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 21959 Its determinant is the ring unity, see mdet0fv0 22087.
11.4.1  The matrix multiplication This section is about the multiplication of m x n matrices.
Syntax	cmmul 21876	Syntax for the matrix multiplication operator.
class maMul
Definition	df-mamu 21877*	The operator which multiplies an m x n matrix with an n x p matrix, see also the definition in [Lang] p. 504. Note that it is not generally possible to recover the dimensions from the matrix, since all n x 0 and all 0 x n matrices are represented by the empty set. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd ‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))))
Theorem	mamufval 21878*	Functional value of the matrix multiplication operator. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))))
Theorem	mamuval 21879*	Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑌𝑘))))))
Theorem	mamufv 21880*	A cell in the multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝐼(𝑋𝐹𝑌)𝐾) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑗𝑌𝐾)))))
Theorem	mamudm 21881	The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.)
⊢ 𝐸 = (𝑅 freeLMod (𝑀 × 𝑁))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑃))    &   ⊢ 𝐶 = (Base‘𝐹)    &   ⊢ × = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin)) → dom × = (𝐵 × 𝐶))
Theorem	mamufacex 21882	Every solution of the equation 𝐴∗𝑋 = 𝐵 for matrices 𝐴 and 𝐵 is a matrix. (Contributed by AV, 10-Feb-2019.)
⊢ 𝐸 = (𝑅 freeLMod (𝑀 × 𝑁))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑃))    &   ⊢ 𝐶 = (Base‘𝐹)    &   ⊢ × = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑀 × 𝑃))    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (((𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅) ∧ (𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷) ∧ (𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin)) → ((𝑋 × 𝑍) = 𝑌 → 𝑍 ∈ 𝐶))
Theorem	mamures 21883	Rows in a matrix product are functions only of the corresponding rows in the left argument. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐺 = (𝑅 maMul ⟨𝐼, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌))
Theorem	mndvcl 21884	Tuple-wise additive closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m 𝐼))
Theorem	mndvass 21885	Tuple-wise associativity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ (𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼) ∧ 𝑍 ∈ (𝐵 ↑m 𝐼))) → ((𝑋 ∘f + 𝑌) ∘f + 𝑍) = (𝑋 ∘f + (𝑌 ∘f + 𝑍)))
Theorem	mndvlid 21886	Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → ((𝐼 × { 0 }) ∘f + 𝑋) = 𝑋)
Theorem	mndvrid 21887	Tuple-wise right identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝐼 × { 0 })) = 𝑋)
Theorem	grpvlinv 21888	Tuple-wise left inverse in groups. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → ((𝑁 ∘ 𝑋) ∘f + 𝑋) = (𝐼 × { 0 }))
Theorem	grpvrinv 21889	Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝑁 ∘ 𝑋)) = (𝐼 × { 0 }))
Theorem	mhmvlin 21890	Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ⨣ = (+g‘𝑁)    ⇒   ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝐹 ∘ (𝑋 ∘f + 𝑌)) = ((𝐹 ∘ 𝑋) ∘f ⨣ (𝐹 ∘ 𝑌)))
Theorem	ringvcl 21891	Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f · 𝑌) ∈ (𝐵 ↑m 𝐼))
Theorem	mamucl 21892	Operation closure of matrix multiplication. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑃)))
Theorem	mamuass 21893	Matrix multiplication is associative, see also statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑂 × 𝑃)))    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ 𝐺 = (𝑅 maMul ⟨𝑀, 𝑂, 𝑃⟩)    &   ⊢ 𝐻 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐼 = (𝑅 maMul ⟨𝑁, 𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌)𝐺𝑍) = (𝑋𝐻(𝑌𝐼𝑍)))
Theorem	mamudi 21894	Matrix multiplication distributes over addition on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)))
Theorem	mamudir 21895	Matrix multiplication distributes over addition on the right. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → (𝑋𝐹(𝑌 ∘f + 𝑍)) = ((𝑋𝐹𝑌) ∘f + (𝑋𝐹𝑍)))
Theorem	mamuvs1 21896	Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)))
Theorem	mamuvs2 21897	Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.)
⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)))
11.4.2  Square matrices In the following, the square matrix algebra is defined as extensible structure Mat. In this subsection, however, only square matrices and their basic properties are regarded. This includes showing that (𝑁 Mat 𝑅) is a left module, see matlmod 21922. That (𝑁 Mat 𝑅) is a ring and an associative algebra is shown in the next subsection, after theorems about the identity matrix are available. Nevertheless, (𝑁 Mat 𝑅) is called "matrix ring" or "matrix algebra" already in this subsection.
Syntax	cmat 21898	Syntax for the square matrix algebra.
class Mat
Definition	df-mat 21899*	Define the algebra of n x n matrices over a ring r. (Contributed by Stefan O'Rear, 31-Aug-2015.)
⊢ Mat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ((𝑟 freeLMod (𝑛 × 𝑛)) sSet ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩))
Theorem	matbas0pc 21900	There is no matrix with a proper class either as dimension or as underlying ring. (Contributed by AV, 28-Dec-2018.)
⊢ (¬ (𝑁 ∈ V ∧ 𝑅 ∈ V) → (Base‘(𝑁 Mat 𝑅)) = ∅)