![]() |
Metamath
Proof Explorer Theorem List (p. 223 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ply1idvr1 22201 | 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 22202* | 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 22203* | The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe 22204. (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 22204* | 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 22205* | 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 22206* | 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 22207* | 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 22208* | 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 22209* | Lemma for coe1fzgsumd 22210 (induction step). (Contributed by AV, 8-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β πΎ β β0) β β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π΅ β ((coe1β(π Ξ£g (π₯ β π β¦ π)))βπΎ) = (π Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β (βπ₯ β (π βͺ {π})π β π΅ β ((coe1β(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))))) | ||
Theorem | coe1fzgsumd 22210* | 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 | ply1scleq 22211 | Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β ((π΄βπΈ) = (π΄βπΉ) β πΈ = πΉ)) | ||
Theorem | ply1chr 22212 | The characteristic of a polynomial ring is the characteristic of the underlying ring. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (Poly1βπ ) β β’ (π β CRing β (chrβπ) = (chrβπ )) | ||
Theorem | gsumsmonply1 22213* | 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 22214* | 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 22215* | 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 22216* | 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 22217* | 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π) Β· ((πβ((π β π)πΈπ΄)) Γ (π β π)))))) | ||
Theorem | ply1fermltlchr 22218 | Fermat's little theorem for polynomials in a commutative ring πΉ of characteristic π prime: we have the polynomial equation (π + π΄)βπ = ((πβπ) + π΄). (Contributed by Thierry Arnoux, 9-Jan-2025.) |
β’ π = (Poly1βπΉ) & β’ π = (var1βπΉ) & β’ + = (+gβπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ πΆ = (algScβπ) & β’ π΄ = (πΆβ((β€RHomβπΉ)βπΈ)) & β’ π = (chrβπΉ) & β’ (π β πΉ β CRing) & β’ (π β π β β) & β’ (π β πΈ β β€) β β’ (π β (π β (π + π΄)) = ((π β π) + π΄)) | ||
Syntax | ces1 22219 | Evaluation of a univariate polynomial in a subring. |
class evalSub1 | ||
Syntax | ce1 22220 | Evaluation of a univariate polynomial. |
class eval1 | ||
Definition | df-evls1 22221* | 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 22222* | 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 22223 | Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.) |
β’ Rel dom evalSub1 | ||
Theorem | ply1frcl 22224 | Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.) |
β’ π = ran (π evalSub1 π ) β β’ (π β π β (π β V β§ π β π« (Baseβπ))) | ||
Theorem | evls1fval 22225* | Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ πΈ = (1o evalSub π) & β’ π΅ = (Baseβπ) β β’ ((π β π β§ π β π« π΅) β π = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦ (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β (πΈβπ ))) | ||
Theorem | evls1val 22226* | 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 22227* | Lemma for evl1rhm 22238 and evls1rhm 22228 (formerly part of the proof of evl1rhm 22238): 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 22228 | 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 22229 | Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = (π΅ Γ {π})) | ||
Theorem | evls1gsumadd 22230* | 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 22231* | 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 22232 | 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 22233 | 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 22234* | 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 22235* | 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 22236 | Lemma for evl1fval1 22237. (Contributed by AV, 11-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ (π β π β π = (π evalSub1 π΅)) | ||
Theorem | evl1fval1 22237 | Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ π = (π evalSub1 π΅) | ||
Theorem | evl1rhm 22238 | 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 22239 | 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 22240 | Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) β β’ ((π β CRing β§ π β π΅) β (πβ(π΄βπ)) = (π΅ Γ {π})) | ||
Theorem | evl1scad 22241 | Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π΄βπ) β π β§ ((πβ(π΄βπ))βπ) = π)) | ||
Theorem | evl1var 22242 | Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) β β’ (π β CRing β (πβπ) = ( I βΎ π΅)) | ||
Theorem | evl1vard 22243 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ (π β (π β π β§ ((πβπ)βπ) = π)) | ||
Theorem | evls1var 22244 | 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 22245 | 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 22246 | 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 22247 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (+gβπ) & β’ + = (+gβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π + π))) | ||
Theorem | evl1subd 22248 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (-gβπ) & β’ π· = (-gβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (ππ·π))) | ||
Theorem | evl1muld 22249 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π Β· π))) | ||
Theorem | evl1vsd 22250 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β π β π΅) & β’ β = ( Β·π βπ) & β’ Β· = (.rβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π Β· π))) | ||
Theorem | evl1expd 22251 | 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 22252 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ ((π β CRing β§ π β π΅) β (π΅ Γ {π}) β π) | ||
Theorem | pf1id 22253 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ (π β CRing β ( I βΎ π΅) β π) | ||
Theorem | pf1subrg 22254 | 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 22255 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) β β’ (π β π β π β CRing) | ||
Theorem | pf1f 22256 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π β πΉ:π΅βΆπ΅) | ||
Theorem | mpfpf1 22257* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) & β’ πΈ = ran (1o eval π ) β β’ (πΉ β πΈ β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π) | ||
Theorem | pf1mpf 22258* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) & β’ πΈ = ran (1o eval π ) β β’ (πΉ β π β (πΉ β (π₯ β (π΅ βm 1o) β¦ (π₯ββ ))) β πΈ) | ||
Theorem | pf1addcl 22259 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ + = (+gβπ ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf + πΊ) β π) | ||
Theorem | pf1mulcl 22260 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf Β· πΊ) β π) | ||
Theorem | pf1ind 22261* | 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 22262* | Lemma for evl1gsumd 22263 (induction step). (Contributed by AV, 17-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) | ||
Theorem | evl1gsumd 22263* | 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 22264* | 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 22230. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (π βs πΎ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ 0 = (0gβπ) & β’ (π β (π₯ β π β¦ π) finSupp 0 ) β β’ (π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (π Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evl1gsumaddval 22265* | 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 22266* | 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 22267 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22264, the proof is shorter using evls1varpw 22233 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β β0) β β’ (π β (πβ(π β π)) = (π(.gβ(mulGrpβ(π βs π΅)))(πβπ))) | ||
Theorem | evl1varpwval 22268 | 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 22269 | 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 22270 | 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 22271* | 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 (π₯ β π β¦ (π΄ Β· (ππΈπΆ))))) | ||
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 21668) 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 21685) and scalar multiplication (see frlmvscafval 21687) 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 22273. 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 21670. However, for square matrices there is Definition df-mat 22295, 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 22355 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). 22355 Its determinant is the ring unity, see mdet0fv0 22483. | ||
This section is about the multiplication of m x n matrices. | ||
Syntax | cmmul 22272 | Syntax for the matrix multiplication operator. |
class maMul | ||
Definition | df-mamu 22273* | 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 22274* | 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 22275* | Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ πΉ = (π maMul β¨π, π, πβ©) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β π) & β’ (π β π β Fin) & β’ (π β π β Fin) & β’ (π β π β Fin) & β’ (π β π β (π΅ βm (π Γ π))) & β’ (π β π β (π΅ βm (π Γ π))) β β’ (π β (ππΉπ) = (π β π, π β π β¦ (π Ξ£g (π β π β¦ ((πππ) Β· (πππ)))))) | ||
Theorem | mamufv 22276* | 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 22277 | The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.) |
β’ πΈ = (π freeLMod (π Γ π)) & β’ π΅ = (BaseβπΈ) & β’ πΉ = (π freeLMod (π Γ π)) & β’ πΆ = (BaseβπΉ) & β’ Γ = (π maMul β¨π, π, πβ©) β β’ ((π β π β§ (π β Fin β§ π β Fin β§ π β Fin)) β dom Γ = (π΅ Γ πΆ)) | ||
Theorem | mamufacex 22278 | 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 22279 | 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 22280 | Tuple-wise additive closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β Mnd β§ π β (π΅ βm πΌ) β§ π β (π΅ βm πΌ)) β (π βf + π) β (π΅ βm πΌ)) | ||
Theorem | mndvass 22281 | 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 22282 | Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β Mnd β§ π β (π΅ βm πΌ)) β ((πΌ Γ { 0 }) βf + π) = π) | ||
Theorem | mndvrid 22283 | Tuple-wise right identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β Mnd β§ π β (π΅ βm πΌ)) β (π βf + (πΌ Γ { 0 })) = π) | ||
Theorem | grpvlinv 22284 | 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 22285 | Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π = (invgβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β (π΅ βm πΌ)) β (π βf + (π β π)) = (πΌ Γ { 0 })) | ||
Theorem | mhmvlin 22286 | Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π MndHom π) β§ π β (π΅ βm πΌ) β§ π β (π΅ βm πΌ)) β (πΉ β (π βf + π)) = ((πΉ β π) βf ⨣ (πΉ β π))) | ||
Theorem | ringvcl 22287 | Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β (π΅ βm πΌ) β§ π β (π΅ βm πΌ)) β (π βf Β· π) β (π΅ βm πΌ)) | ||
Theorem | mamucl 22288 | 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 22289 | 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 22290 | 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 22291 | 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 22292 | 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 22293 | 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 Β· (ππΉπ))) | ||
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 22318. 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 22294 | Syntax for the square matrix algebra. |
class Mat | ||
Definition | df-mat 22295* | 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 22296 | 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 22297 | 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 22298 | Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ πΊ = (π freeLMod (π Γ π)) & β’ Β· = (π maMul β¨π, π, πβ©) β β’ ((π β Fin β§ π β π) β π΄ = (πΊ sSet β¨(.rβndx), Β· β©)) | ||
Theorem | matrcl 22299 | Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β (π β Fin β§ π β V)) | ||
Theorem | matbas 22300 | 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βπ΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |