Metamath Proof Explorer

Theorem mat0op

Description: Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018)

Ref Expression
Hypotheses mat0op.a ⊢ A = N Mat R
mat0op.z ⊢ 0 ˙ = 0 R
Assertion mat0op ⊢ N ∈ Fin ∧ R ∈ Ring → 0 A = i ∈ N , j ∈ N ⟼ 0 ˙

Proof

Step Hyp Ref Expression
1 mat0op.a ⊢ A = N Mat R
2 mat0op.z ⊢ 0 ˙ = 0 R
3 eqid ⊢ R freeLMod N × N = R freeLMod N × N
4 1 3 mat0 ⊢ N ∈ Fin ∧ R ∈ Ring → 0 R freeLMod N × N = 0 A
5 fconstmpo ⊢ N × N × 0 R = i ∈ N , j ∈ N ⟼ 0 R
6 simpr ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Ring
7 sqxpexg ⊢ N ∈ Fin → N × N ∈ V
8 7 adantr ⊢ N ∈ Fin ∧ R ∈ Ring → N × N ∈ V
9 eqid ⊢ 0 R = 0 R
10 3 9 frlm0 ⊢ R ∈ Ring ∧ N × N ∈ V → N × N × 0 R = 0 R freeLMod N × N
11 6 8 10 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring → N × N × 0 R = 0 R freeLMod N × N
12 2 eqcomi ⊢ 0 R = 0 ˙
13 12 a1i ⊢ i ∈ N ∧ j ∈ N → 0 R = 0 ˙
14 13 mpoeq3ia ⊢ i ∈ N , j ∈ N ⟼ 0 R = i ∈ N , j ∈ N ⟼ 0 ˙
15 14 a1i ⊢ N ∈ Fin ∧ R ∈ Ring → i ∈ N , j ∈ N ⟼ 0 R = i ∈ N , j ∈ N ⟼ 0 ˙
16 5 11 15 3eqtr3a ⊢ N ∈ Fin ∧ R ∈ Ring → 0 R freeLMod N × N = i ∈ N , j ∈ N ⟼ 0 ˙
17 4 16 eqtr3d ⊢ N ∈ Fin ∧ R ∈ Ring → 0 A = i ∈ N , j ∈ N ⟼ 0 ˙