# 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}\mathrm{Mat}{R}$
mat0op.z
Assertion mat0op

### Proof

Step Hyp Ref Expression
1 mat0op.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mat0op.z
3 eqid ${⊢}{R}\mathrm{freeLMod}\left({N}×{N}\right)={R}\mathrm{freeLMod}\left({N}×{N}\right)$
4 1 3 mat0 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={0}_{{A}}$
5 fconstmpo ${⊢}\left({N}×{N}\right)×\left\{{0}_{{R}}\right\}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
6 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\in \mathrm{Ring}$
7 sqxpexg ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{V}$
8 7 adantr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}×{N}\in \mathrm{V}$
9 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
10 3 9 frlm0 ${⊢}\left({R}\in \mathrm{Ring}\wedge {N}×{N}\in \mathrm{V}\right)\to \left({N}×{N}\right)×\left\{{0}_{{R}}\right\}={0}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
11 6 8 10 syl2anc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({N}×{N}\right)×\left\{{0}_{{R}}\right\}={0}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
12 2 eqcomi
13 12 a1i
14 13 mpoeq3ia
15 14 a1i
16 5 11 15 3eqtr3a
17 4 16 eqtr3d