# Metamath Proof Explorer

## Theorem matsubgcell

Description: Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses matplusgcell.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matplusgcell.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
matsubgcell.s ${⊢}{S}={-}_{{A}}$
matsubgcell.m
Assertion matsubgcell

### Proof

Step Hyp Ref Expression
1 matplusgcell.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matplusgcell.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 matsubgcell.s ${⊢}{S}={-}_{{A}}$
4 matsubgcell.m
5 1 2 matrcl ${⊢}{X}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
6 5 simpld ${⊢}{X}\in {B}\to {N}\in \mathrm{Fin}$
7 6 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {N}\in \mathrm{Fin}$
8 7 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
9 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
10 eqid ${⊢}{R}\mathrm{freeLMod}\left({N}×{N}\right)={R}\mathrm{freeLMod}\left({N}×{N}\right)$
11 1 10 matsubg ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {-}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={-}_{{A}}$
12 8 9 11 syl2anc ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {-}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={-}_{{A}}$
13 12 3 syl6reqr ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {S}={-}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
14 13 oveqd ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {X}{S}{Y}={X}{-}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}{Y}$
15 eqid ${⊢}{\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
16 xpfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {N}×{N}\in \mathrm{Fin}$
17 16 anidms ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{Fin}$
18 17 adantr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {N}×{N}\in \mathrm{Fin}$
19 5 18 syl ${⊢}{X}\in {B}\to {N}×{N}\in \mathrm{Fin}$
20 19 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {N}×{N}\in \mathrm{Fin}$
21 20 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {N}×{N}\in \mathrm{Fin}$
22 2 eleq2i ${⊢}{X}\in {B}↔{X}\in {\mathrm{Base}}_{{A}}$
23 22 biimpi ${⊢}{X}\in {B}\to {X}\in {\mathrm{Base}}_{{A}}$
24 1 10 matbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
25 5 24 syl ${⊢}{X}\in {B}\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
26 23 25 eleqtrrd ${⊢}{X}\in {B}\to {X}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
27 26 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
28 27 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {X}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
29 2 eleq2i ${⊢}{Y}\in {B}↔{Y}\in {\mathrm{Base}}_{{A}}$
30 29 biimpi ${⊢}{Y}\in {B}\to {Y}\in {\mathrm{Base}}_{{A}}$
31 1 2 matrcl ${⊢}{Y}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
32 31 24 syl ${⊢}{Y}\in {B}\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
33 30 32 eleqtrrd ${⊢}{Y}\in {B}\to {Y}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
34 33 adantl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
35 34 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {Y}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
36 eqid ${⊢}{-}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={-}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
37 10 15 9 21 28 35 4 36 frlmsubgval
38 14 37 eqtrd
39 38 oveqd
40 df-ov
41 opelxpi ${⊢}\left({I}\in {N}\wedge {J}\in {N}\right)\to ⟨{I},{J}⟩\in \left({N}×{N}\right)$
42 41 anim2i ${⊢}\left(\left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to \left(\left({X}\in {B}\wedge {Y}\in {B}\right)\wedge ⟨{I},{J}⟩\in \left({N}×{N}\right)\right)$
43 42 3adant1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to \left(\left({X}\in {B}\wedge {Y}\in {B}\right)\wedge ⟨{I},{J}⟩\in \left({N}×{N}\right)\right)$
44 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
45 1 44 2 matbas2i ${⊢}{X}\in {B}\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
46 elmapfn ${⊢}{X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {X}Fn\left({N}×{N}\right)$
47 45 46 syl ${⊢}{X}\in {B}\to {X}Fn\left({N}×{N}\right)$
48 47 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}Fn\left({N}×{N}\right)$
49 1 44 2 matbas2i ${⊢}{Y}\in {B}\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
50 elmapfn ${⊢}{Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {Y}Fn\left({N}×{N}\right)$
51 49 50 syl ${⊢}{Y}\in {B}\to {Y}Fn\left({N}×{N}\right)$
52 51 adantl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {Y}Fn\left({N}×{N}\right)$
53 inidm ${⊢}\left({N}×{N}\right)\cap \left({N}×{N}\right)={N}×{N}$
54 df-ov ${⊢}{I}{X}{J}={X}\left(⟨{I},{J}⟩\right)$
55 54 eqcomi ${⊢}{X}\left(⟨{I},{J}⟩\right)={I}{X}{J}$
56 55 a1i ${⊢}\left(\left({X}\in {B}\wedge {Y}\in {B}\right)\wedge ⟨{I},{J}⟩\in \left({N}×{N}\right)\right)\to {X}\left(⟨{I},{J}⟩\right)={I}{X}{J}$
57 df-ov ${⊢}{I}{Y}{J}={Y}\left(⟨{I},{J}⟩\right)$
58 57 eqcomi ${⊢}{Y}\left(⟨{I},{J}⟩\right)={I}{Y}{J}$
59 58 a1i ${⊢}\left(\left({X}\in {B}\wedge {Y}\in {B}\right)\wedge ⟨{I},{J}⟩\in \left({N}×{N}\right)\right)\to {Y}\left(⟨{I},{J}⟩\right)={I}{Y}{J}$
60 48 52 20 20 53 56 59 ofval
61 43 60 syl
62 40 61 syl5eq
63 39 62 eqtrd