Metamath Proof Explorer

Theorem pmat0opsc

Description: The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebra scalar lifting function algSc ). (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses pmat0opsc.p ⊢ P = Poly 1 ⁡ R
pmat0opsc.c ⊢ C = N Mat P
pmat0opsc.a ⊢ A = algSc ⁡ P
pmat0opsc.z ⊢ 0 ˙ = 0 R
Assertion pmat0opsc ⊢ N ∈ Fin ∧ R ∈ Ring → 0 C = i ∈ N , j ∈ N ⟼ A ⁡ 0 ˙

Proof

Step Hyp Ref Expression
1 pmat0opsc.p ⊢ P = Poly 1 ⁡ R
2 pmat0opsc.c ⊢ C = N Mat P
3 pmat0opsc.a ⊢ A = algSc ⁡ P
4 pmat0opsc.z ⊢ 0 ˙ = 0 R
5 eqid ⊢ 0 P = 0 P
6 1 2 5 pmat0op ⊢ N ∈ Fin ∧ R ∈ Ring → 0 C = i ∈ N , j ∈ N ⟼ 0 P
7 1 3 4 5 ply1scl0 ⊢ R ∈ Ring → A ⁡ 0 ˙ = 0 P
8 7 eqcomd ⊢ R ∈ Ring → 0 P = A ⁡ 0 ˙
9 8 adantl ⊢ N ∈ Fin ∧ R ∈ Ring → 0 P = A ⁡ 0 ˙
10 9 mpoeq3dv ⊢ N ∈ Fin ∧ R ∈ Ring → i ∈ N , j ∈ N ⟼ 0 P = i ∈ N , j ∈ N ⟼ A ⁡ 0 ˙
11 6 10 eqtrd ⊢ N ∈ Fin ∧ R ∈ Ring → 0 C = i ∈ N , j ∈ N ⟼ A ⁡ 0 ˙