![]() |
Metamath
Proof Explorer Theorem List (p. 222 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | evl1varpw 22101 | Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22098, the proof is shorter using evls1varpw 22067 instead of proving it directly. (Contributed by AV, 15-Sep-2019.) |
โข ๐ = (eval1โ๐ ) & โข ๐ = (Poly1โ๐ ) & โข ๐บ = (mulGrpโ๐) & โข ๐ = (var1โ๐ ) & โข ๐ต = (Baseโ๐ ) & โข โ = (.gโ๐บ) & โข (๐ โ ๐ โ CRing) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐โ(๐ โ ๐)) = (๐(.gโ(mulGrpโ(๐ โs ๐ต)))(๐โ๐))) | ||
Theorem | evl1varpwval 22102 | 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 22103 | 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 22104 | 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 22105* | 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 21522) 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 21539) and scalar multiplication (see frlmvscafval 21541) 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 22107. 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 21524. However, for square matrices there is Definition df-mat 22129, 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 22189 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). 22189 Its determinant is the ring unity, see mdet0fv0 22317. | ||
This section is about the multiplication of m x n matrices. | ||
Syntax | cmmul 22106 | Syntax for the matrix multiplication operator. |
class maMul | ||
Definition | df-mamu 22107* | 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 22108* | 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 22109* | Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
โข ๐น = (๐ maMul โจ๐, ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) โ โข (๐ โ (๐๐น๐) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐๐๐)))))) | ||
Theorem | mamufv 22110* | 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 22111 | The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.) |
โข ๐ธ = (๐ freeLMod (๐ ร ๐)) & โข ๐ต = (Baseโ๐ธ) & โข ๐น = (๐ freeLMod (๐ ร ๐)) & โข ๐ถ = (Baseโ๐น) & โข ร = (๐ maMul โจ๐, ๐, ๐โฉ) โ โข ((๐ โ ๐ โง (๐ โ Fin โง ๐ โ Fin โง ๐ โ Fin)) โ dom ร = (๐ต ร ๐ถ)) | ||
Theorem | mamufacex 22112 | 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 22113 | 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 22114 | Tuple-wise additive closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) โ โข ((๐ โ Mnd โง ๐ โ (๐ต โm ๐ผ) โง ๐ โ (๐ต โm ๐ผ)) โ (๐ โf + ๐) โ (๐ต โm ๐ผ)) | ||
Theorem | mndvass 22115 | 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 22116 | Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข 0 = (0gโ๐) โ โข ((๐ โ Mnd โง ๐ โ (๐ต โm ๐ผ)) โ ((๐ผ ร { 0 }) โf + ๐) = ๐) | ||
Theorem | mndvrid 22117 | Tuple-wise right identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข 0 = (0gโ๐) โ โข ((๐ โ Mnd โง ๐ โ (๐ต โm ๐ผ)) โ (๐ โf + (๐ผ ร { 0 })) = ๐) | ||
Theorem | grpvlinv 22118 | 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 22119 | Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ = (invgโ๐บ) & โข 0 = (0gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ (๐ต โm ๐ผ)) โ (๐ โf + (๐ โ ๐)) = (๐ผ ร { 0 })) | ||
Theorem | mhmvlin 22120 | Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+gโ๐) โ โข ((๐น โ (๐ MndHom ๐) โง ๐ โ (๐ต โm ๐ผ) โง ๐ โ (๐ต โm ๐ผ)) โ (๐น โ (๐ โf + ๐)) = ((๐น โ ๐) โf โจฃ (๐น โ ๐))) | ||
Theorem | ringvcl 22121 | Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ (๐ต โm ๐ผ) โง ๐ โ (๐ต โm ๐ผ)) โ (๐ โf ยท ๐) โ (๐ต โm ๐ผ)) | ||
Theorem | mamucl 22122 | 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 22123 | 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 22124 | 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 22125 | 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 22126 | 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 22127 | 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 22152. 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 22128 | Syntax for the square matrix algebra. |
class Mat | ||
Definition | df-mat 22129* | 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 22130 | 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 22131 | 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 22132 | Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐บ = (๐ freeLMod (๐ ร ๐)) & โข ยท = (๐ maMul โจ๐, ๐, ๐โฉ) โ โข ((๐ โ Fin โง ๐ โ ๐) โ ๐ด = (๐บ sSet โจ(.rโndx), ยท โฉ)) | ||
Theorem | matrcl 22133 | Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (๐ โ ๐ต โ (๐ โ Fin โง ๐ โ V)) | ||
Theorem | matbas 22134 | 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 22135 | 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 22136 | 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 22137 | Obsolete proof of matsca 22136 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 22138 | 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 22139 | Obsolete proof of matvsca 22138 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 22140 | 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 22141 | 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 22142* | Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ (0gโ๐ด) = (๐ โ ๐, ๐ โ ๐ โฆ 0 )) | ||
Theorem | matsca2 22143 | The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) โ โข ((๐ โ Fin โง ๐ โ ๐) โ ๐ = (Scalarโ๐ด)) | ||
Theorem | matbas2 22144 | 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 22145 | A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐พ = (Baseโ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (๐ โ ๐ต โ ๐ โ (๐พ โm (๐ ร ๐))) | ||
Theorem | matbas2d 22146* | 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 22147* | 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 22148 | 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 22149 | 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 22150 | Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข โ = (+gโ๐ด) & โข + = (+gโ๐ ) โ โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) = (๐ โf + ๐)) | ||
Theorem | matvsca2 22151 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข ยท = ( ยท๐ โ๐ด) & โข ร = (.rโ๐ ) & โข ๐ถ = (๐ ร ๐) โ โข ((๐ โ ๐พ โง ๐ โ ๐ต) โ (๐ ยท ๐) = ((๐ถ ร {๐}) โf ร ๐)) | ||
Theorem | matlmod 22152 | The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐ด โ LMod) | ||
Theorem | matgrp 22153 | The matrix ring is a group. (Contributed by AV, 21-Dec-2019.) |
โข ๐ด = (๐ Mat ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐ด โ Grp) | ||
Theorem | matvscl 22154 | Closure of the scalar multiplication in the matrix ring. (lmodvscl 20633 analog.) (Contributed by AV, 27-Nov-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ยท = ( ยท๐ โ๐ด) โ โข (((๐ โ Fin โง ๐ โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ต)) โ (๐ถ ยท ๐) โ ๐ต) | ||
Theorem | matsubg 22155 | The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐บ = (๐ freeLMod (๐ ร ๐)) โ โข ((๐ โ Fin โง ๐ โ ๐) โ (-gโ๐บ) = (-gโ๐ด)) | ||
Theorem | matplusgcell 22156 | Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข โ = (+gโ๐ด) & โข + = (+gโ๐ ) โ โข (((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐ โ ๐)๐ฝ) = ((๐ผ๐๐ฝ) + (๐ผ๐๐ฝ))) | ||
Theorem | matsubgcell 22157 | Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (-gโ๐ด) & โข โ = (-gโ๐ ) โ โข ((๐ โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐๐๐)๐ฝ) = ((๐ผ๐๐ฝ) โ (๐ผ๐๐ฝ))) | ||
Theorem | matinvgcell 22158 | Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (invgโ๐ ) & โข ๐ = (invgโ๐ด) โ โข ((๐ โ Ring โง ๐ โ ๐ต โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐โ๐)๐ฝ) = (๐โ(๐ผ๐๐ฝ))) | ||
Theorem | matvscacell 22159 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข ยท = ( ยท๐ โ๐ด) & โข ร = (.rโ๐ ) โ โข ((๐ โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐ ยท ๐)๐ฝ) = (๐ ร (๐ผ๐๐ฝ))) | ||
Theorem | matgsum 22160* | Finite commutative sums in a matrix algebra are taken componentwise. (Contributed by AV, 26-Sep-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 0 = (0gโ๐ด) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ฝ โ ๐) & โข (๐ โ ๐ โ Ring) & โข ((๐ โง ๐ฆ โ ๐ฝ) โ (๐ โ ๐, ๐ โ ๐ โฆ ๐) โ ๐ต) & โข (๐ โ (๐ฆ โ ๐ฝ โฆ (๐ โ ๐, ๐ โ ๐ โฆ ๐)) finSupp 0 ) โ โข (๐ โ (๐ด ฮฃg (๐ฆ โ ๐ฝ โฆ (๐ โ ๐, ๐ โ ๐ โฆ ๐))) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ฆ โ ๐ฝ โฆ ๐)))) | ||
The main result of this subsection are the theorems showing that (๐ Mat ๐ ) is a ring (see matring 22166) and an associative algebra (see matassa 22167). Additionally, theorems for the identity matrix and transposed matrices are provided. | ||
Theorem | matmulr 22161 | Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข ยท = (๐ maMul โจ๐, ๐, ๐โฉ) โ โข ((๐ โ Fin โง ๐ โ ๐) โ ยท = (.rโ๐ด)) | ||
Theorem | mamumat1cl 22162* | The identity matrix (as operation in maps-to notation) is a matrix. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
โข ๐ต = (Baseโ๐ ) & โข (๐ โ ๐ โ Ring) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข ๐ผ = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, 1 , 0 )) & โข (๐ โ ๐ โ Fin) โ โข (๐ โ ๐ผ โ (๐ต โm (๐ ร ๐))) | ||
Theorem | mat1comp 22163* | The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019.) |
โข ๐ต = (Baseโ๐ ) & โข (๐ โ ๐ โ Ring) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข ๐ผ = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, 1 , 0 )) & โข (๐ โ ๐ โ Fin) โ โข ((๐ด โ ๐ โง ๐ฝ โ ๐) โ (๐ด๐ผ๐ฝ) = if(๐ด = ๐ฝ, 1 , 0 )) | ||
Theorem | mamulid 22164* | The identity matrix (as operation in maps-to notation) is a left identity (for any matrix with the same number of rows). (Contributed by Stefan O'Rear, 3-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.) |
โข ๐ต = (Baseโ๐ ) & โข (๐ โ ๐ โ Ring) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข ๐ผ = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, 1 , 0 )) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข ๐น = (๐ maMul โจ๐, ๐, ๐โฉ) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) โ โข (๐ โ (๐ผ๐น๐) = ๐) | ||
Theorem | mamurid 22165* | The identity matrix (as operation in maps-to notation) is a right identity (for any matrix with the same number of columns). (Contributed by Stefan O'Rear, 3-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.) |
โข ๐ต = (Baseโ๐ ) & โข (๐ โ ๐ โ Ring) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข ๐ผ = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, 1 , 0 )) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข ๐น = (๐ maMul โจ๐, ๐, ๐โฉ) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) โ โข (๐ โ (๐๐น๐ผ) = ๐) | ||
Theorem | matring 22166 | Existence of the matrix ring, see also the statement in [Lang] p. 504: "For a given integer n > 0 the set of square n x n matrices form a ring." (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐ด โ Ring) | ||
Theorem | matassa 22167 | Existence of the matrix algebra, see also the statement in [Lang] p. 505: "Then Matn(R) is an algebra over R" . (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) โ โข ((๐ โ Fin โง ๐ โ CRing) โ ๐ด โ AssAlg) | ||
Theorem | matmulcell 22168* | Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019.) (Revised by AV, 3-Jul-2022.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ร = (.rโ๐ด) โ โข ((๐ โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐ ร ๐)๐ฝ) = (๐ ฮฃg (๐ โ ๐ โฆ ((๐ผ๐๐)(.rโ๐ )(๐๐๐ฝ))))) | ||
Theorem | mpomatmul 22169* | Multiplication of two N x N matrices given in maps-to notation. (Contributed by AV, 29-Oct-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ร = (.rโ๐ด) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข ๐ = (๐ โ ๐, ๐ โ ๐ โฆ ๐ถ) & โข ๐ = (๐ โ ๐, ๐ โ ๐ โฆ ๐ธ) & โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ถ โ ๐ต) & โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ธ โ ๐ต) & โข ((๐ โง (๐ = ๐ โง ๐ = ๐)) โ ๐ท = ๐ถ) & โข ((๐ โง (๐ = ๐ โง ๐ = ๐)) โ ๐น = ๐ธ) & โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ท โ ๐) & โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐น โ ๐) โ โข (๐ โ (๐ ร ๐) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ (๐ท ยท ๐น))))) | ||
Theorem | mat1 22170* | Value of an identity matrix, see also the statement in [Lang] p. 504: "The unit element of the ring of n x n matrices is the matrix In ... whose components are equal to 0 except on the diagonal, in which case they are equal to 1.". (Contributed by Stefan O'Rear, 7-Sep-2015.) |
โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ (1rโ๐ด) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, 1 , 0 ))) | ||
Theorem | mat1ov 22171 | Entries of an identity matrix, deduction form. (Contributed by Stefan O'Rear, 10-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ฝ โ ๐) & โข ๐ = (1rโ๐ด) โ โข (๐ โ (๐ผ๐๐ฝ) = if(๐ผ = ๐ฝ, 1 , 0 )) | ||
Theorem | mat1bas 22172 | The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข 1 = (1rโ(๐ Mat ๐ )) โ โข ((๐ โ Ring โง ๐ โ Fin) โ 1 โ ๐ต) | ||
Theorem | matsc 22173* | The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐พ = (Baseโ๐ ) & โข ยท = ( ยท๐ โ๐ด) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring โง ๐ฟ โ ๐พ) โ (๐ฟ ยท (1rโ๐ด)) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ๐ฟ, 0 ))) | ||
Theorem | ofco2 22174 | Distribution law for the function operation and the composition of functions. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข (((๐น โ V โง ๐บ โ V) โง (Fun ๐ป โง (๐น โ ๐ป) โ V โง (๐บ โ ๐ป) โ V)) โ ((๐น โf ๐ ๐บ) โ ๐ป) = ((๐น โ ๐ป) โf ๐ (๐บ โ ๐ป))) | ||
Theorem | oftpos 22175 | The transposition of the value of a function operation for two functions is the value of the function operation for the two functions transposed. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข ((๐น โ ๐ โง ๐บ โ ๐) โ tpos (๐น โf ๐ ๐บ) = (tpos ๐น โf ๐ tpos ๐บ)) | ||
Theorem | mattposcl 22176 | The transpose of a square matrix is a square matrix of the same size. (Contributed by SO, 9-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (๐ โ ๐ต โ tpos ๐ โ ๐ต) | ||
Theorem | mattpostpos 22177 | The transpose of the transpose of a square matrix is the square matrix itself. (Contributed by SO, 17-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (๐ โ ๐ต โ tpos tpos ๐ = ๐) | ||
Theorem | mattposvs 22178 | The transposition of a matrix multiplied with a scalar equals the transposed matrix multiplied with the scalar, see also the statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข ยท = ( ยท๐ โ๐ด) โ โข ((๐ โ ๐พ โง ๐ โ ๐ต) โ tpos (๐ ยท ๐) = (๐ ยท tpos ๐)) | ||
Theorem | mattpos1 22179 | The transposition of the identity matrix is the identity matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) โ โข ((๐ โ Fin โง ๐ โ Ring) โ tpos 1 = 1 ) | ||
Theorem | tposmap 22180 | The transposition of an I X J -matrix is a J X I -matrix, see also the statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
โข (๐ด โ (๐ต โm (๐ผ ร ๐ฝ)) โ tpos ๐ด โ (๐ต โm (๐ฝ ร ๐ผ))) | ||
Theorem | mamutpos 22181 | Behavior of transposes in matrix products, see also the statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
โข ๐น = (๐ maMul โจ๐, ๐, ๐โฉ) & โข ๐บ = (๐ maMul โจ๐, ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข (๐ โ ๐ โ CRing) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) โ โข (๐ โ tpos (๐๐น๐) = (tpos ๐๐บtpos ๐)) | ||
Theorem | mattposm 22182 | Multiplying two transposed matrices results in the transposition of the product of the two matrices. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ยท = (.rโ๐ด) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง ๐ โ ๐ต) โ tpos (๐ ยท ๐) = (tpos ๐ ยท tpos ๐)) | ||
Theorem | matgsumcl 22183* | Closure of a group sum over the diagonal coefficients of a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018.) (Proof shortened by AV, 23-Jul-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (mulGrpโ๐ ) โ โข ((๐ โ CRing โง ๐ โ ๐ต) โ (๐ ฮฃg (๐ โ ๐ โฆ (๐๐๐))) โ (Baseโ๐ )) | ||
Theorem | madetsumid 22184* | The identity summand in the Leibniz' formula of a determinant for a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง ๐ = ( I โพ ๐)) โ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = (๐ ฮฃg (๐ โ ๐ โฆ (๐๐๐)))) | ||
Theorem | matepmcl 22185* | Each entry of a matrix with an index as permutation of the other is an element of the underlying ring. (Contributed by AV, 1-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Baseโ(SymGrpโ๐)) โ โข ((๐ โ Ring โง ๐ โ ๐ โง ๐ โ ๐ต) โ โ๐ โ ๐ ((๐โ๐)๐๐) โ (Baseโ๐ )) | ||
Theorem | matepm2cl 22186* | Each entry of a matrix with an index as permutation of the other is an element of the underlying ring. (Contributed by AV, 1-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Baseโ(SymGrpโ๐)) โ โข ((๐ โ Ring โง ๐ โ ๐ โง ๐ โ ๐ต) โ โ๐ โ ๐ (๐๐(๐โ๐)) โ (Baseโ๐ )) | ||
Theorem | madetsmelbas 22187* | A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (pmSgnโ๐) & โข ๐ = (โคRHomโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐บ = (mulGrpโ๐ ) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง ๐ โ ๐) โ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (Baseโ๐ )) | ||
Theorem | madetsmelbas2 22188* | A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (pmSgnโ๐) & โข ๐ = (โคRHomโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐บ = (mulGrpโ๐ ) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง ๐ โ ๐) โ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ (Baseโ๐ )) | ||
As already mentioned before, and shown in mat0dimbas0 22189, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 22189 In the following, some properties of the empty matrix are shown, especially that the empty matrix over an arbitrary ring forms a commutative ring, see mat0dimcrng 22193. For the one-dimensional case, it can be shown that a ring of matrices with dimension 1 is isomorphic to the underlying ring, see mat1ric 22210. | ||
Theorem | mat0dimbas0 22189 | The empty set is the one and only matrix of dimension 0, called "the empty matrix". (Contributed by AV, 27-Feb-2019.) |
โข (๐ โ ๐ โ (Baseโ(โ Mat ๐ )) = {โ }) | ||
Theorem | mat0dim0 22190 | The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
โข ๐ด = (โ Mat ๐ ) โ โข (๐ โ Ring โ (0gโ๐ด) = โ ) | ||
Theorem | mat0dimid 22191 | The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
โข ๐ด = (โ Mat ๐ ) โ โข (๐ โ Ring โ (1rโ๐ด) = โ ) | ||
Theorem | mat0dimscm 22192 | The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
โข ๐ด = (โ Mat ๐ ) โ โข ((๐ โ Ring โง ๐ โ (Baseโ๐ )) โ (๐( ยท๐ โ๐ด)โ ) = โ ) | ||
Theorem | mat0dimcrng 22193 | The algebra of matrices with dimension 0 (over an arbitrary ring!) is a commutative ring. (Contributed by AV, 10-Aug-2019.) |
โข ๐ด = (โ Mat ๐ ) โ โข (๐ โ Ring โ ๐ด โ CRing) | ||
Theorem | mat1dimelbas 22194* | A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข ((๐ โ Ring โง ๐ธ โ ๐) โ (๐ โ (Baseโ๐ด) โ โ๐ โ ๐ต ๐ = {โจ๐, ๐โฉ})) | ||
Theorem | mat1dimbas 22195 | A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข ((๐ โ Ring โง ๐ธ โ ๐ โง ๐ โ ๐ต) โ {โจ๐, ๐โฉ} โ (Baseโ๐ด)) | ||
Theorem | mat1dim0 22196 | The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข ((๐ โ Ring โง ๐ธ โ ๐) โ (0gโ๐ด) = {โจ๐, (0gโ๐ )โฉ}) | ||
Theorem | mat1dimid 22197 | The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข ((๐ โ Ring โง ๐ธ โ ๐) โ (1rโ๐ด) = {โจ๐, (1rโ๐ )โฉ}) | ||
Theorem | mat1dimscm 22198 | The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข (((๐ โ Ring โง ๐ธ โ ๐) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐( ยท๐ โ๐ด){โจ๐, ๐โฉ}) = {โจ๐, (๐(.rโ๐ )๐)โฉ}) | ||
Theorem | mat1dimmul 22199 | The ring multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.) (Proof shortened by AV, 18-Apr-2021.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข (((๐ โ Ring โง ๐ธ โ ๐) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ({โจ๐, ๐โฉ} (.rโ๐ด){โจ๐, ๐โฉ}) = {โจ๐, (๐(.rโ๐ )๐)โฉ}) | ||
Theorem | mat1dimcrng 22200 | The algebra of matrices with dimension 1 over a commutative ring is a commutative ring. (Contributed by AV, 16-Aug-2019.) |
โข ๐ด = ({๐ธ} Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐ = โจ๐ธ, ๐ธโฉ โ โข ((๐ โ CRing โง ๐ธ โ ๐) โ ๐ด โ CRing) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |