# Metamath Proof Explorer

## Theorem marrepcl

Description: Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019)

Ref Expression
Hypotheses marrepcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
marrepcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion marrepcl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({M}\left({N}\mathrm{matRRep}{R}\right){S}\right){L}\in {B}$

### Proof

Step Hyp Ref Expression
1 marrepcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 marrepcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 eqid ${⊢}{N}\mathrm{matRRep}{R}={N}\mathrm{matRRep}{R}$
4 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
5 1 2 3 4 marrepval ${⊢}\left(\left({M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({M}\left({N}\mathrm{matRRep}{R}\right){S}\right){L}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={L},{S},{0}_{{R}}\right),{i}{M}{j}\right)\right)$
6 5 3adantl1 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({M}\left({N}\mathrm{matRRep}{R}\right){S}\right){L}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={L},{S},{0}_{{R}}\right),{i}{M}{j}\right)\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
8 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
9 8 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
10 9 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\to {N}\in \mathrm{Fin}$
11 10 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
12 simpl1 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
13 simp3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\to {S}\in {\mathrm{Base}}_{{R}}$
14 7 4 ring0cl ${⊢}{R}\in \mathrm{Ring}\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
15 14 3ad2ant1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
16 13 15 ifcld ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\to if\left({j}={L},{S},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
17 16 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to if\left({j}={L},{S},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
18 17 3ad2ant1 ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to if\left({j}={L},{S},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
19 simp2 ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}\in {N}$
20 simp3 ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {j}\in {N}$
21 2 eleq2i ${⊢}{M}\in {B}↔{M}\in {\mathrm{Base}}_{{A}}$
22 21 biimpi ${⊢}{M}\in {B}\to {M}\in {\mathrm{Base}}_{{A}}$
23 22 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
24 23 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {M}\in {\mathrm{Base}}_{{A}}$
25 24 3ad2ant1 ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
26 1 7 matecl ${⊢}\left({i}\in {N}\wedge {j}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to {i}{M}{j}\in {\mathrm{Base}}_{{R}}$
27 19 20 25 26 syl3anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{M}{j}\in {\mathrm{Base}}_{{R}}$
28 18 27 ifcld ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to if\left({i}={K},if\left({j}={L},{S},{0}_{{R}}\right),{i}{M}{j}\right)\in {\mathrm{Base}}_{{R}}$
29 1 7 2 11 12 28 matbas2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼if\left({i}={K},if\left({j}={L},{S},{0}_{{R}}\right),{i}{M}{j}\right)\right)\in {B}$
30 6 29 eqeltrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({M}\left({N}\mathrm{matRRep}{R}\right){S}\right){L}\in {B}$