P. 224 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	evl1gsumd 22301*	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 22302*	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 22268. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝑃 = (𝑅 ↑s 𝐾)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑁 ↦ 𝑌) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑥 ∈ 𝑁 ↦ 𝑌))) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ (𝑄‘𝑌))))
Theorem	evl1gsumaddval 22303*	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 22304*	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 22305	Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd 22302, the proof is shorter using evls1varpw 22271 instead of proving it directly. (Contributed by AV, 15-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑁 ↑ 𝑋)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑄‘𝑋)))
Theorem	evl1varpwval 22306	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 22307	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 22308	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 22309*	Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019.)
⊢ 𝑄 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐻 = (mulGrp‘𝑅)    &   ⊢ 𝐸 = (.g‘𝐻)    &   ⊢ 𝐺 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑀 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑀 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑊 Σg (𝑥 ∈ 𝑀 ↦ (𝐴 × (𝑁 ↑ 𝑋)))))‘𝐶) = (𝑅 Σg (𝑥 ∈ 𝑀 ↦ (𝐴 · (𝑁𝐸𝐶)))))
11.3.5.1  Specialization of polynomial evaluation as a ring homomorphism
Theorem	evls1scafv 22310	Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐶) = 𝑋)
Theorem	evls1expd 22311	Univariate polynomial evaluation builder for an exponential. See also evl1expd 22289. (Contributed by Thierry Arnoux, 24-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ ∧ = (.g‘(mulGrp‘𝑊))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑀))‘𝐶) = (𝑁 ↑ ((𝑄‘𝑀)‘𝐶)))
Theorem	evls1varpwval 22312	Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 22306. (Contributed by Thierry Arnoux, 24-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑋 = (var1‘𝑈)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ ∧ = (.g‘(mulGrp‘𝑊))    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑁 ∧ 𝑋))‘𝐶) = (𝑁 ↑ 𝐶))
Theorem	evls1fpws 22313*	Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ 𝐴 = (coe1‘𝑀)    ⇒   ⊢ (𝜑 → (𝑄‘𝑀) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))))
Theorem	ressply1evl 22314	Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐸 = (eval1‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝑄 = (𝐸 ↾ 𝐵))
Theorem	evls1addd 22315	Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ⨣ = (+g‘𝑊)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑀 ⨣ 𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) + ((𝑄‘𝑁)‘𝐶)))
Theorem	evls1muld 22316	Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ × = (.r‘𝑊)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝑀 × 𝑁))‘𝐶) = (((𝑄‘𝑀)‘𝐶) · ((𝑄‘𝑁)‘𝐶)))
Theorem	evls1vsca 22317	Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑄 = (𝑆 evalSub1 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ × = ( ·𝑠 ‘𝑊)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴 × 𝑁))‘𝐶) = (𝐴 · ((𝑄‘𝑁)‘𝐶)))
Theorem	asclply1subcl 22318	Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝐴 = (algSc‘𝑉)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝑉 = (Poly1‘𝑅)    &   ⊢ 𝑊 = (Poly1‘𝑈)    &   ⊢ 𝑃 = (Base‘𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴‘𝑍) ∈ 𝑃)
Theorem	evls1fvcl 22319	Variant of fveval1fvcl 22277 for the subring evaluation function evalSub1 (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑌) ∈ 𝐵)
Theorem	evls1maprhm 22320*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	evls1maplmhm 22321*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴 is a module homomorphism, when considering the subring algebra. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    &   ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑆)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 LMHom 𝐴))
Theorem	evls1maprnss 22322*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴 takes all values in the subring 𝑆. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    ⇒   ⊢ (𝜑 → 𝑆 ⊆ ran 𝐹)
Theorem	evl1maprhm 22323*	The function 𝐹 mapping polynomials 𝑝 to their evaluation at a given point 𝑋 is a ring homomorphism. (Contributed by metakunt, 19-May-2025.)
⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	mhmcompl 22324	The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶)
Theorem	mhmcoaddmpl 22325	Show that the ring homomorphism in rhmmpl 22327 preserves addition. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ✚ = (+g‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺)))
Theorem	rhmcomulmpl 22326	Show that the ring homomorphism in rhmmpl 22327 preserves multiplication. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ∙ = (.r‘𝑄)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺)))
Theorem	rhmmpl 22327*	Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm 20454. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	ply1vscl 22328	Closure of scalar multiplication for univariate polynomials. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · 𝑋) ∈ 𝐵)
Theorem	mhmcoply1 22329	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 22330*	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 22331*	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 22332*	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 22333*	Apply a ring homomorphism between two univariate polynomial algebras to a scaled monomial, as in ply1coe 22242. (Contributed by SN, 20-May-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑌 = (var1‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ ∙ = ( ·𝑠 ‘𝑄)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ 𝑁 = (mulGrp‘𝑄)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ ∧ = (.g‘𝑁)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐶 · (𝐸 ↑ 𝑋))) = ((𝐻‘𝐶) ∙ (𝐸 ∧ 𝑌)))
11.4  Matrices According to Wikipedia ("Matrix (mathemetics)", 02-Apr-2019, https://en.wikipedia.org/wiki/Matrix_(mathematics)) "A matrix is a rectangular array of numbers or other mathematical objects for which operations such as addition and multiplication are defined. Most commonly, a matrix over a field F is a rectangular array of scalars each of which is a member of F. The numbers, symbols or expressions in the matrix are called its entries or its elements. The horizontal and vertical lines of entries in a matrix are called rows and columns, respectively.", and in the definition of [Lang] p. 503 "By an m x n matrix in [a commutative ring] R one means a doubly indexed family of elements of R, (aij), (i= 1,..., m and j = 1,... n) ... We call the elements aij the coefficients or components of the matrix. A 1 x n matrix is called a row vector (of dimension, or size, n) and a m x 1 matrix is called a column vector (of dimension, or size, m). In general, we say that (m,n) is the size of the matrix, ...". In contrast to these definitions, we denote any free module over a (not necessarily commutative) ring (in the meaning of df-frlm 21698) 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 21715) and scalar multiplication (see frlmvscafval 21717) 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 22335. 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 21700. However, for square matrices there is Definition df-mat 22352, 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 22412 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). 22412 Its determinant is the ring unity, see mdet0fv0 22540.
11.4.1  The matrix multiplication This section is about the multiplication of m x n matrices.
Syntax	cmmul 22334	Syntax for the matrix multiplication operator.
class maMul
Definition	df-mamu 22335*	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 22336*	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 22337*	Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑌𝑘))))))
Theorem	mamufv 22338*	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 22339	The domain of the matrix multiplication function. (Contributed by AV, 10-Feb-2019.)
⊢ 𝐸 = (𝑅 freeLMod (𝑀 × 𝑁))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐹 = (𝑅 freeLMod (𝑁 × 𝑃))    &   ⊢ 𝐶 = (Base‘𝐹)    &   ⊢ × = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin)) → dom × = (𝐵 × 𝐶))
Theorem	mamufacex 22340	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 22341	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 22342	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 22343	Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝑁 ∘ 𝑋)) = (𝐼 × { 0 }))
Theorem	ringvcl 22344	Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f · 𝑌) ∈ (𝐵 ↑m 𝐼))
Theorem	mamucl 22345	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 22346	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 22347	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 22348	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 22349	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 22350	Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.)
⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)))
11.4.2  Square matrices In the following, the square matrix algebra is defined as extensible structure Mat. In this subsection, however, only square matrices and their basic properties are regarded. This includes showing that (𝑁 Mat 𝑅) is a left module, see matlmod 22375. 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 22351	Syntax for the square matrix algebra.
class Mat
Definition	df-mat 22352*	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 22353	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 22354	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 22355	Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    &   ⊢ · = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐴 = (𝐺 sSet ⟨(.r‘ndx), · ⟩))
Theorem	matrcl 22356	Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
Theorem	matbas 22357	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 22358	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 22359	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 22360	Obsolete proof of matsca 22359 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 22361	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 22362	Obsolete proof of matvsca 22361 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 22363	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 22364	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 22365*	Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 ))
Theorem	matsca2 22366	The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 = (Scalar‘𝐴))
Theorem	matbas2 22367	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 22368	A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
Theorem	matbas2d 22369*	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 22370*	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 22371	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 22372	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 22373	Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ ✚ = (+g‘𝐴)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌))
Theorem	matvsca2 22374	Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐶 = (𝑁 × 𝑁)    ⇒   ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = ((𝐶 × {𝑋}) ∘f × 𝑌))
Theorem	matlmod 22375	The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod)
Theorem	matgrp 22376	The matrix ring is a group. (Contributed by AV, 21-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp)
Theorem	matvscl 22377	Closure of the scalar multiplication in the matrix ring. (lmodvscl 20773 analog.) (Contributed by AV, 27-Nov-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵)) → (𝐶 · 𝑋) ∈ 𝐵)
Theorem	matsubg 22378	The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (-g‘𝐺) = (-g‘𝐴))
Theorem	matplusgcell 22379	Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ ✚ = (+g‘𝐴)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 ✚ 𝑌)𝐽) = ((𝐼𝑋𝐽) + (𝐼𝑌𝐽)))
Theorem	matsubgcell 22380	Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (-g‘𝐴)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋𝑆𝑌)𝐽) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽)))
Theorem	matinvgcell 22381	Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = (invg‘𝑅)    &   ⊢ 𝑊 = (invg‘𝐴)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑊‘𝑋)𝐽) = (𝑉‘(𝐼𝑋𝐽)))
Theorem	matvscacell 22382	Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 · 𝑌)𝐽) = (𝑋 × (𝐼𝑌𝐽)))
Theorem	matgsum 22383*	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 (𝑦 ∈ 𝐽 ↦ 𝑈))))
11.4.3  The matrix algebra The main result of this subsection are the theorems showing that (𝑁 Mat 𝑅) is a ring (see matring 22389) and an associative algebra (see matassa 22390). Additionally, theorems for the identity matrix and transposed matrices are provided.
Theorem	matmulr 22384	Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → · = (.r‘𝐴))
Theorem	mamumat1cl 22385*	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 22386*	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 22387*	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 22388*	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 22389	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 22390	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 22391*	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 22392*	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 22393*	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 22394	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 22395	The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘(𝑁 Mat 𝑅))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 1 ∈ 𝐵)
Theorem	matsc 22396*	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 22397	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 22398	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 22399	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 22400	The transpose of the transpose of a square matrix is the square matrix itself. (Contributed by SO, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → tpos tpos 𝑀 = 𝑀)