![]() |
Metamath
Proof Explorer Theorem List (p. 225 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rhmcomulmpl 22401 | Show that the ring homomorphism in rhmmpl 22402 preserves multiplication. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑄 = (𝐼 mPoly 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ · = (.r‘𝑃) & ⊢ ∙ = (.r‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmmpl 22402* | Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm 20519. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑄 = (𝐼 mPoly 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄)) | ||
Theorem | ply1vscl 22403 | Closure of scalar multiplication for univariate polynomials. (Contributed by SN, 20-May-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · 𝑋) ∈ 𝐵) | ||
Theorem | mhmcoply1 22404 | The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 20-May-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑄 = (Poly1‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶) | ||
Theorem | rhmply1 22405* | Provide a ring homomorphism between two univariate polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 20-May-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑄 = (Poly1‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄)) | ||
Theorem | rhmply1vr1 22406* | A ring homomorphism between two univariate polynomial algebras sends one variable to the other. (Contributed by SN, 20-May-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑄 = (Poly1‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑌 = (var1‘𝑆) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = 𝑌) | ||
Theorem | rhmply1vsca 22407* | Apply a ring homomorphism between two univariate polynomial algebras to a scaled polynomial. (Contributed by SN, 20-May-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑄 = (Poly1‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∙ = ( ·𝑠 ‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘(𝐶 · 𝑋)) = ((𝐻‘𝐶) ∙ (𝐹‘𝑋))) | ||
Theorem | rhmply1mon 22408* | Apply a ring homomorphism between two univariate polynomial algebras to a scaled monomial, as in ply1coe 22317. (Contributed by SN, 20-May-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑄 = (Poly1‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑌 = (var1‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∙ = ( ·𝑠 ‘𝑄) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑄) & ⊢ ↑ = (.g‘𝑀) & ⊢ ∧ = (.g‘𝑁) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝐸 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹‘(𝐶 · (𝐸 ↑ 𝑋))) = ((𝐻‘𝐶) ∙ (𝐸 ∧ 𝑌))) | ||
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 21784) 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 21801) and scalar multiplication (see frlmvscafval 21803) 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 22410. 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 21786. However, for square matrices there is Definition df-mat 22427, 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 22487 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). 22487 Its determinant is the ring unity, see mdet0fv0 22615. | ||
This section is about the multiplication of m x n matrices. | ||
Syntax | cmmul 22409 | Syntax for the matrix multiplication operator. |
class maMul | ||
Definition | df-mamu 22410* | 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 22411* | 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 22412* | Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃))) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑌𝑘)))))) | ||
Theorem | mamufv 22413* | 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 22414 | The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.) |
⊢ 𝐸 = (𝑅 freeLMod (𝑀 × 𝑁)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑃)) & ⊢ 𝐶 = (Base‘𝐹) & ⊢ × = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin)) → dom × = (𝐵 × 𝐶)) | ||
Theorem | mamufacex 22415 | 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 22416 | Rows in a matrix product are functions only of the corresponding rows in the left argument. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) & ⊢ 𝐺 = (𝑅 maMul 〈𝐼, 𝑁, 𝑃〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ Fin) & ⊢ (𝜑 → 𝐼 ⊆ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃))) ⇒ ⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌)) | ||
Theorem | grpvlinv 22417 | 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 22418 | Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝑁 ∘ 𝑋)) = (𝐼 × { 0 })) | ||
Theorem | ringvcl 22419 | Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f · 𝑌) ∈ (𝐵 ↑m 𝐼)) | ||
Theorem | mamucl 22420 | 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 22421 | 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 22422 | 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 22423 | 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 22424 | 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 22425 | 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 22450. 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 22426 | Syntax for the square matrix algebra. |
class Mat | ||
Definition | df-mat 22427* | 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 22428 | 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 22429 | 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 22430 | Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁)) & ⊢ · = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐴 = (𝐺 sSet 〈(.r‘ndx), · 〉)) | ||
Theorem | matrcl 22431 | Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) | ||
Theorem | matbas 22432 | 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 22433 | 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 22434 | 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 22435 | Obsolete version of matsca 22434 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 22436 | 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 22437 | Obsolete version of matvsca 22436 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 22438 | 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 22439 | 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 22440* | Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 )) | ||
Theorem | matsca2 22441 | The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 = (Scalar‘𝐴)) | ||
Theorem | matbas2 22442 | 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 22443 | A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁))) | ||
Theorem | matbas2d 22444* | 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 22445* | 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 22446 | 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 22447 | 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 22448 | Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ ✚ = (+g‘𝐴) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | matvsca2 22449 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐴) & ⊢ × = (.r‘𝑅) & ⊢ 𝐶 = (𝑁 × 𝑁) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = ((𝐶 × {𝑋}) ∘f × 𝑌)) | ||
Theorem | matlmod 22450 | The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) | ||
Theorem | matgrp 22451 | The matrix ring is a group. (Contributed by AV, 21-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp) | ||
Theorem | matvscl 22452 | Closure of the scalar multiplication in the matrix ring. (lmodvscl 20892 analog.) (Contributed by AV, 27-Nov-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵)) → (𝐶 · 𝑋) ∈ 𝐵) | ||
Theorem | matsubg 22453 | The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (-g‘𝐺) = (-g‘𝐴)) | ||
Theorem | matplusgcell 22454 | Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ ✚ = (+g‘𝐴) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 ✚ 𝑌)𝐽) = ((𝐼𝑋𝐽) + (𝐼𝑌𝐽))) | ||
Theorem | matsubgcell 22455 | Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (-g‘𝐴) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋𝑆𝑌)𝐽) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽))) | ||
Theorem | matinvgcell 22456 | Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = (invg‘𝑅) & ⊢ 𝑊 = (invg‘𝐴) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑊‘𝑋)𝐽) = (𝑉‘(𝐼𝑋𝐽))) | ||
Theorem | matvscacell 22457 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐴) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 · 𝑌)𝐽) = (𝑋 × (𝐼𝑌𝐽))) | ||
Theorem | matgsum 22458* | 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 22464) and an associative algebra (see matassa 22465). Additionally, theorems for the identity matrix and transposed matrices are provided. | ||
Theorem | matmulr 22459 | Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ · = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → · = (.r‘𝐴)) | ||
Theorem | mamumat1cl 22460* | 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 22461* | 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 22462* | 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 22463* | 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 22464 | 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 22465 | 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 22466* | 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 22467* | 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 22468* | 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 22469 | 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 22470 | The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘(𝑁 Mat 𝑅)) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 1 ∈ 𝐵) | ||
Theorem | matsc 22471* | 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 22472 | 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 22473 | 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 22474 | 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 22475 | 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 22476 | 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 22477 | 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 22478 | 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 22479 | 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 22480 | 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 22481* | 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 22482* | 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 22483* | 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 22484* | 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 22485* | 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 22486* | 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 22487, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 22487 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 22491. 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 22508. | ||
Theorem | mat0dimbas0 22487 | 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 22488 | The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐴 = (∅ Mat 𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (0g‘𝐴) = ∅) | ||
Theorem | mat0dimid 22489 | The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐴 = (∅ Mat 𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (1r‘𝐴) = ∅) | ||
Theorem | mat0dimscm 22490 | The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐴 = (∅ Mat 𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋( ·𝑠 ‘𝐴)∅) = ∅) | ||
Theorem | mat0dimcrng 22491 | 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 22492* | 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 22493 | 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 22494 | The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (0g‘𝐴) = {〈𝑂, (0g‘𝑅)〉}) | ||
Theorem | mat1dimid 22495 | The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {〈𝑂, (1r‘𝑅)〉}) | ||
Theorem | mat1dimscm 22496 | The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝐴){〈𝑂, 𝑌〉}) = {〈𝑂, (𝑋(.r‘𝑅)𝑌)〉}) | ||
Theorem | mat1dimmul 22497 | 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 22498 | 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) | ||
Theorem | mat1f1o 22499* | There is a 1-1 function from a ring onto the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹:𝐾–1-1-onto→𝐵) | ||
Theorem | mat1rhmval 22500* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = {〈𝑂, 𝑋〉}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |