P. 224 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22301-22400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-evls1 22301*	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 22302*	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 22303	Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.)
⊢ Rel dom evalSub1
Theorem	ply1frcl 22304	Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.)
⊢ 𝑄 = ran (𝑆 evalSub1 𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → (𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 (Base‘𝑆)))
Theorem	evls1fval 22305*	Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐸 = (1o evalSub 𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))
Theorem	evls1val 22306*	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 22307*	Lemma for evl1rhm 22318 and evls1rhm 22308 (formerly part of the proof of evl1rhm 22318): 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 22308	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 22309	Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝐵 × {𝑋}))
Theorem	evls1gsumadd 22310*	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 22311*	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 22312	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 22313	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 22314*	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 22315*	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 22316	Lemma for evl1fval1 22317. (Contributed by AV, 11-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑄 = (𝑅 evalSub1 𝐵))
Theorem	evl1fval1 22317	Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝑄 = (𝑅 evalSub1 𝐵)
Theorem	evl1rhm 22318	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 22319	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 22320	Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑂‘(𝐴‘𝑋)) = (𝐵 × {𝑋}))
Theorem	evl1scad 22321	Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝑈 ∧ ((𝑂‘(𝐴‘𝑋))‘𝑌) = 𝑋))
Theorem	evl1var 22322	Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐵))
Theorem	evl1vard 22323	Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ ((𝑂‘𝑋)‘𝑌) = 𝑌))
Theorem	evls1var 22324	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 22325	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 22326	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 22327	Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ✚ 𝑁))‘𝑌) = (𝑉 + 𝑊)))
Theorem	evl1subd 22328	Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐷 = (-g‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 − 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 − 𝑁))‘𝑌) = (𝑉𝐷𝑊)))
Theorem	evl1muld 22329	Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝑈 ∧ ((𝑂‘𝑁)‘𝑌) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝑈 ∧ ((𝑂‘(𝑀 ∙ 𝑁))‘𝑌) = (𝑉 · 𝑊)))
Theorem	evl1vsd 22330	Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉))    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ ∙ = ( ·𝑠 ‘𝑃)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 · 𝑉)))
Theorem	evl1expd 22331	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 22332	Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝐵 × {𝑋}) ∈ 𝑄)
Theorem	pf1id 22333	The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → ( I ↾ 𝐵) ∈ 𝑄)
Theorem	pf1subrg 22334	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 22335	Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    ⇒   ⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing)
Theorem	pf1f 22336	Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑄 → 𝐹:𝐵⟶𝐵)
Theorem	mpfpf1 22337*	Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = ran (1o eval 𝑅)    ⇒   ⊢ (𝐹 ∈ 𝐸 → (𝐹 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ 𝑄)
Theorem	pf1mpf 22338*	Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = ran (1o eval 𝑅)    ⇒   ⊢ (𝐹 ∈ 𝑄 → (𝐹 ∘ (𝑥 ∈ (𝐵 ↑m 1o) ↦ (𝑥‘∅))) ∈ 𝐸)
Theorem	pf1addcl 22339	The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f + 𝐺) ∈ 𝑄)
Theorem	pf1mulcl 22340	The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑄 = ran (eval1‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄) → (𝐹 ∘f · 𝐺) ∈ 𝑄)
Theorem	pf1ind 22341*	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 22342*	Lemma for evl1gsumd 22343 (induction step). (Contributed by AV, 17-Sep-2019.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((𝑂‘𝑀)‘𝑌)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝑈 → ((𝑂‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝑌) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((𝑂‘𝑀)‘𝑌))))))
Theorem	evl1gsumd 22343*	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 22344*	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 22310. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝑃 = (𝑅 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evl1gsumaddval 22345*	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 22346*	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 22347	Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22344, the proof is shorter using evls1varpw 22313 instead of proving it directly. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋)))
Theorem	evl1varpwval 22348	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 22349	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 22350	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 22351*	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.3.6.1  Specialization of polynomial evaluation as a ring homomorphism
Theorem	evls1scafv 22352	Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐶) = 𝑋)
Theorem	evls1expd 22353	Univariate polynomial evaluation builder for an exponential. See also evl1expd 22331. (Contributed by Thierry Arnoux, 24-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ∧ = (.g‘(mulGrp‘𝑊))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑀))‘𝐶) = (𝑁 ↑ ((𝑄‘𝑀)‘𝐶)))
Theorem	evls1varpwval 22354	Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 22348. (Contributed by Thierry Arnoux, 24-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑋 = (var1‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ ∧ = (.g‘(mulGrp‘𝑊))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑋))‘𝐶) = (𝑁 ↑ 𝐶))
Theorem	evls1fpws 22355*	Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ 𝐴 = (coe1‘𝑀)    ⇒   ⊢ (𝜑 → (𝑄‘𝑀) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))))
Theorem	ressply1evl 22356	Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐸 = (eval1‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝑄 = (𝐸 ↾ 𝐵))
Theorem	evls1addd 22357	Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ⨣ = (+g‘𝑊)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑀 ⨣ 𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) + ((𝑄‘𝑁)‘𝐶)))
Theorem	evls1muld 22358	Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ × = (.r‘𝑊)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑀 × 𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) · ((𝑄‘𝑁)‘𝐶)))
Theorem	evls1vsca 22359	Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴 × 𝑁))‘𝐶) = (𝐴 · ((𝑄‘𝑁)‘𝐶)))
Theorem	asclply1subcl 22360	Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝐴 = (algSc‘𝑉)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝑉 = (Poly1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑃 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴‘𝑍) ∈ 𝑃)
Theorem	evls1fvcl 22361	Variant of fveval1fvcl 22319 for the subring evaluation function evalSub1. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑌) ∈ 𝐵)
Theorem	evls1maprhm 22362*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	evls1maplmhm 22363*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴 is a module homomorphism, when considering the subring algebra. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    &   ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑆)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 LMHom 𝐴))
Theorem	evls1maprnss 22364*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴 takes all values in the subring 𝑆. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    ⇒   ⊢ (𝜑 → 𝑆 ⊆ ran 𝐹)
Theorem	evl1maprhm 22365*	The function 𝐹 mapping polynomials 𝑝 to their evaluation at a given point 𝑋 is a ring homomorphism. (Contributed by metakunt, 19-May-2025.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	rhmmpl 22366*	Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm 20474. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	ply1vscl 22367	Closure of scalar multiplication for univariate polynomials. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · 𝑋) ∈ 𝐵)
Theorem	mhmcoply1 22368	The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶)
Theorem	rhmply1 22369*	Provide a ring homomorphism between two univariate polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	rhmply1vr1 22370*	A ring homomorphism between two univariate polynomial algebras sends one variable to the other. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑌 = (var1‘𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = 𝑌)
Theorem	rhmply1vsca 22371*	Apply a ring homomorphism between two univariate polynomial algebras to a scaled polynomial. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐶 · 𝑋)) = ((𝐻‘𝐶) ∙ (𝐹‘𝑋)))
Theorem	rhmply1mon 22372*	Apply a ring homomorphism between two univariate polynomial algebras to a scaled monomial, as in ply1coe 22284. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑌 = (var1‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝑄)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ 𝑁 = (mulGrp‘𝑄)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ ∧ = (.g‘𝑁)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐶 · (𝐸 ↑ 𝑋))) = ((𝐻‘𝐶) ∙ (𝐸 ∧ 𝑌)))
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 21722) 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 21739) and scalar multiplication (see frlmvscafval 21741) 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 22374. 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 21724. However, for square matrices there is Definition df-mat 22391, 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 22449 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). 22449 Its determinant is the ring unity, see mdet0fv0 22577.
11.4.1  The matrix multiplication This section is about the multiplication of m x n matrices.
Syntax	cmmul 22373	Syntax for the matrix multiplication operator.
class maMul
Definition	df-mamu 22374*	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 22375*	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 22376*	Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑌𝑘))))))
Theorem	mamufv 22377*	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 22378	The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.)
⊢ 𝐸 = (𝑅 freeLMod (𝑀 × 𝑁))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑃))    &   ⊢ 𝐶 = (Base‘𝐹)    &   ⊢ × = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin)) → dom × = (𝐵 × 𝐶))
Theorem	mamufacex 22379	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 22380	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	grpvlinv 22381	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 22382	Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝑁 ∘ 𝑋)) = (𝐼 × { 0 }))
Theorem	ringvcl 22383	Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f · 𝑌) ∈ (𝐵 ↑m 𝐼))
Theorem	mamucl 22384	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 22385	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 22386	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 22387	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 22388	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 22389	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 22412. 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 22390	Syntax for the square matrix algebra.
class Mat
Definition	df-mat 22391*	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 22392	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 𝑅)) = ∅)
Theorem	matbas0 22393	There is no matrix for a not finite dimension or a proper class as the underlying ring. (Contributed by AV, 28-Dec-2018.)
⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘(𝑁 Mat 𝑅)) = ∅)
Theorem	matval 22394	Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    &   ⊢ · = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐴 = (𝐺 sSet ⟨(.r‘ndx), · ⟩))
Theorem	matrcl 22395	Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
Theorem	matbas 22396	The matrix ring has the same base set as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (Base‘𝐺) = (Base‘𝐴))
Theorem	matplusg 22397	The matrix ring has the same addition as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (+g‘𝐺) = (+g‘𝐴))
Theorem	matsca 22398	The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, 12-Nov-2024.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (Scalar‘𝐺) = (Scalar‘𝐴))
Theorem	matvsca 22399	The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, 12-Nov-2024.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ( ·𝑠 ‘𝐺) = ( ·𝑠 ‘𝐴))
Theorem	mat0 22400	The matrix ring has the same zero as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (0g‘𝐺) = (0g‘𝐴))