Home | Metamath
Proof Explorer Theorem List (p. 217 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ces1 21601 | Evaluation of a univariate polynomial in a subring. |
class evalSub1 | ||
Syntax | ce1 21602 | Evaluation of a univariate polynomial. |
class eval1 | ||
Definition | df-evls1 21603* | 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 21604* | 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 21605 | Well-behaved binary operation property of evalSub1. (Contributed by AV, 7-Sep-2019.) |
β’ Rel dom evalSub1 | ||
Theorem | ply1frcl 21606 | Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019.) |
β’ π = ran (π evalSub1 π ) β β’ (π β π β (π β V β§ π β π« (Baseβπ))) | ||
Theorem | evls1fval 21607* | Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ πΈ = (1o evalSub π) & β’ π΅ = (Baseβπ) β β’ ((π β π β§ π β π« π΅) β π = ((π₯ β (π΅ βm (π΅ βm 1o)) β¦ (π₯ β (π¦ β π΅ β¦ (1o Γ {π¦})))) β (πΈβπ ))) | ||
Theorem | evls1val 21608* | 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 21609* | Lemma for evl1rhm 21620 and evls1rhm 21610 (formerly part of the proof of evl1rhm 21620): 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 21610 | 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 21611 | Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = (π΅ Γ {π})) | ||
Theorem | evls1gsumadd 21612* | 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 21613* | 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 21614 | 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 21615 | 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 21616* | 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 21617* | 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 21618 | Lemma for evl1fval1 21619. (Contributed by AV, 11-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ (π β π β π = (π evalSub1 π΅)) | ||
Theorem | evl1fval1 21619 | Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ π = (π evalSub1 π΅) | ||
Theorem | evl1rhm 21620 | 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 21621 | 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 21622 | Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) β β’ ((π β CRing β§ π β π΅) β (πβ(π΄βπ)) = (π΅ Γ {π})) | ||
Theorem | evl1scad 21623 | Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π΄βπ) β π β§ ((πβ(π΄βπ))βπ) = π)) | ||
Theorem | evl1var 21624 | Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (eval1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) β β’ (π β CRing β (πβπ) = ( I βΎ π΅)) | ||
Theorem | evl1vard 21625 | Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ (π β (π β π β§ ((πβπ)βπ) = π)) | ||
Theorem | evls1var 21626 | 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 21627 | 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 21628 | 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 21629 | Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (+gβπ) & β’ + = (+gβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π + π))) | ||
Theorem | evl1subd 21630 | Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (-gβπ) & β’ π· = (-gβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (ππ·π))) | ||
Theorem | evl1muld 21631 | Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π Β· π))) | ||
Theorem | evl1vsd 21632 | Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β (π β π β§ ((πβπ)βπ) = π)) & β’ (π β π β π΅) & β’ β = ( Β·π βπ) & β’ Β· = (.rβπ ) β β’ (π β ((π β π) β π β§ ((πβ(π β π))βπ) = (π Β· π))) | ||
Theorem | evl1expd 21633 | 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 21634 | Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ ((π β CRing β§ π β π΅) β (π΅ Γ {π}) β π) | ||
Theorem | pf1id 21635 | The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = ran (eval1βπ ) β β’ (π β CRing β ( I βΎ π΅) β π) | ||
Theorem | pf1subrg 21636 | 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 21637 | Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) β β’ (π β π β π β CRing) | ||
Theorem | pf1f 21638 | Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π β πΉ:π΅βΆπ΅) | ||
Theorem | mpfpf1 21639* | Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) & β’ πΈ = ran (1o eval π ) β β’ (πΉ β πΈ β (πΉ β (π¦ β π΅ β¦ (1o Γ {π¦}))) β π) | ||
Theorem | pf1mpf 21640* | Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ π΅ = (Baseβπ ) & β’ πΈ = ran (1o eval π ) β β’ (πΉ β π β (πΉ β (π₯ β (π΅ βm 1o) β¦ (π₯ββ ))) β πΈ) | ||
Theorem | pf1addcl 21641 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ + = (+gβπ ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf + πΊ) β π) | ||
Theorem | pf1mulcl 21642 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = ran (eval1βπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf Β· πΊ) β π) | ||
Theorem | pf1ind 21643* | 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 21644* | Lemma for evl1gsumd 21645 (induction step). (Contributed by AV, 17-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) | ||
Theorem | evl1gsumd 21645* | 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 21646* | 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 21612. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (π βs πΎ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ 0 = (0gβπ) & β’ (π β (π₯ β π β¦ π) finSupp 0 ) β β’ (π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (π Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evl1gsumaddval 21647* | 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 21648* | 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 21649 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 21646, the proof is shorter using evls1varpw 21615 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ πΊ = (mulGrpβπ) & β’ π = (var1βπ ) & β’ π΅ = (Baseβπ ) & β’ β = (.gβπΊ) & β’ (π β π β CRing) & β’ (π β π β β0) β β’ (π β (πβ(π β π)) = (π(.gβ(mulGrpβ(π βs π΅)))(πβπ))) | ||
Theorem | evl1varpwval 21650 | 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 21651 | 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 21652 | 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 21653* | 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 21076) 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 21093) and scalar multiplication (see frlmvscafval 21095) 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 21655. 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 21078. However, for square matrices there is Definition df-mat 21677, 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 21737 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). 21737 Its determinant is the ring unity, see mdet0fv0 21865. | ||
This section is about the multiplication of m x n matrices. | ||
Syntax | cmmul 21654 | Syntax for the matrix multiplication operator. |
class maMul | ||
Definition | df-mamu 21655* | 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 21656* | 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 21657* | Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ πΉ = (π maMul β¨π, π, πβ©) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β π) & β’ (π β π β Fin) & β’ (π β π β Fin) & β’ (π β π β Fin) & β’ (π β π β (π΅ βm (π Γ π))) & β’ (π β π β (π΅ βm (π Γ π))) β β’ (π β (ππΉπ) = (π β π, π β π β¦ (π Ξ£g (π β π β¦ ((πππ) Β· (πππ)))))) | ||
Theorem | mamufv 21658* | 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 21659 | The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.) |
β’ πΈ = (π freeLMod (π Γ π)) & β’ π΅ = (BaseβπΈ) & β’ πΉ = (π freeLMod (π Γ π)) & β’ πΆ = (BaseβπΉ) & β’ Γ = (π maMul β¨π, π, πβ©) β β’ ((π β π β§ (π β Fin β§ π β Fin β§ π β Fin)) β dom Γ = (π΅ Γ πΆ)) | ||
Theorem | mamufacex 21660 | 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 21661 | 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 21662 | Tuple-wise additive closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β Mnd β§ π β (π΅ βm πΌ) β§ π β (π΅ βm πΌ)) β (π βf + π) β (π΅ βm πΌ)) | ||
Theorem | mndvass 21663 | 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 21664 | Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β Mnd β§ π β (π΅ βm πΌ)) β ((πΌ Γ { 0 }) βf + π) = π) | ||
Theorem | mndvrid 21665 | Tuple-wise right identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β Mnd β§ π β (π΅ βm πΌ)) β (π βf + (πΌ Γ { 0 })) = π) | ||
Theorem | grpvlinv 21666 | 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 21667 | Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π = (invgβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β (π΅ βm πΌ)) β (π βf + (π β π)) = (πΌ Γ { 0 })) | ||
Theorem | mhmvlin 21668 | Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π MndHom π) β§ π β (π΅ βm πΌ) β§ π β (π΅ βm πΌ)) β (πΉ β (π βf + π)) = ((πΉ β π) βf ⨣ (πΉ β π))) | ||
Theorem | ringvcl 21669 | Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β (π΅ βm πΌ) β§ π β (π΅ βm πΌ)) β (π βf Β· π) β (π΅ βm πΌ)) | ||
Theorem | mamucl 21670 | 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 21671 | 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 21672 | 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 21673 | 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 21674 | 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 21675 | 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 21700. 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 21676 | Syntax for the square matrix algebra. |
class Mat | ||
Definition | df-mat 21677* | 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 21678 | 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 21679 | 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 21680 | Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ πΊ = (π freeLMod (π Γ π)) & β’ Β· = (π maMul β¨π, π, πβ©) β β’ ((π β Fin β§ π β π) β π΄ = (πΊ sSet β¨(.rβndx), Β· β©)) | ||
Theorem | matrcl 21681 | Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β (π β Fin β§ π β V)) | ||
Theorem | matbas 21682 | 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 21683 | 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 21684 | 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 | matscaOLD 21685 | Obsolete proof of matsca 21684 as of 12-Nov-2024. The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΄ = (π Mat π ) & β’ πΊ = (π freeLMod (π Γ π)) β β’ ((π β Fin β§ π β π) β (ScalarβπΊ) = (Scalarβπ΄)) | ||
Theorem | matvsca 21686 | 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 | matvscaOLD 21687 | Obsolete proof of matvsca 21686 as of 12-Nov-2024. The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΄ = (π Mat π ) & β’ πΊ = (π freeLMod (π Γ π)) β β’ ((π β Fin β§ π β π) β ( Β·π βπΊ) = ( Β·π βπ΄)) | ||
Theorem | mat0 21688 | 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βπ΄)) | ||
Theorem | matinvg 21689 | The matrix ring has the same additive inverse as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ πΊ = (π freeLMod (π Γ π)) β β’ ((π β Fin β§ π β π) β (invgβπΊ) = (invgβπ΄)) | ||
Theorem | mat0op 21690* | Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ 0 = (0gβπ ) β β’ ((π β Fin β§ π β Ring) β (0gβπ΄) = (π β π, π β π β¦ 0 )) | ||
Theorem | matsca2 21691 | The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (π Mat π ) β β’ ((π β Fin β§ π β π) β π = (Scalarβπ΄)) | ||
Theorem | matbas2 21692 | The base set of the matrix ring as a set exponential. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 16-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ ) β β’ ((π β Fin β§ π β π) β (πΎ βm (π Γ π)) = (Baseβπ΄)) | ||
Theorem | matbas2i 21693 | A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β π β (πΎ βm (π Γ π))) | ||
Theorem | matbas2d 21694* | The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ΄) & β’ (π β π β Fin) & β’ (π β π β π) & β’ ((π β§ π₯ β π β§ π¦ β π) β πΆ β πΎ) β β’ (π β (π₯ β π, π¦ β π β¦ πΆ) β π΅) | ||
Theorem | eqmat 21695* | Two square matrices of the same dimension are equal if they have the same entries. (Contributed by AV, 25-Sep-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π = π β βπ β π βπ β π (πππ) = (πππ))) | ||
Theorem | matecl 21696 | Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring. (Contributed by AV, 16-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ ) β β’ ((πΌ β π β§ π½ β π β§ π β (Baseβπ΄)) β (πΌππ½) β πΎ) | ||
Theorem | matecld 21697 | Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring, deduction form. (Contributed by AV, 27-Nov-2019.) |
β’ π΄ = (π Mat π ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ΄) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β π β π΅) β β’ (π β (πΌππ½) β πΎ) | ||
Theorem | matplusg2 21698 | Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ β = (+gβπ΄) & β’ + = (+gβπ ) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π βf + π)) | ||
Theorem | matvsca2 21699 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ΄) & β’ Γ = (.rβπ ) & β’ πΆ = (π Γ π) β β’ ((π β πΎ β§ π β π΅) β (π Β· π) = ((πΆ Γ {π}) βf Γ π)) | ||
Theorem | matlmod 21700 | The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΄ = (π Mat π ) β β’ ((π β Fin β§ π β Ring) β π΄ β LMod) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |