# Metamath Proof Explorer

## Theorem minmar1cl

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

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

### Proof

Step Hyp Ref Expression
1 minmar1cl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 minmar1cl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
4 1 2 3 minmar1marrep ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({N}\mathrm{minMatR1}{R}\right)\left({M}\right)={M}\left({N}\mathrm{matRRep}{R}\right){1}_{{R}}$
5 4 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to \left({N}\mathrm{minMatR1}{R}\right)\left({M}\right)={M}\left({N}\mathrm{matRRep}{R}\right){1}_{{R}}$
6 5 oveqd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){L}={K}\left({M}\left({N}\mathrm{matRRep}{R}\right){1}_{{R}}\right){L}$
7 simpl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {R}\in \mathrm{Ring}$
8 simpr ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {M}\in {B}$
9 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
10 9 3 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {\mathrm{Base}}_{{R}}$
11 10 adantr ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {1}_{{R}}\in {\mathrm{Base}}_{{R}}$
12 7 8 11 3jca ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {1}_{{R}}\in {\mathrm{Base}}_{{R}}\right)$
13 1 2 marrepcl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {1}_{{R}}\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){1}_{{R}}\right){L}\in {B}$
14 12 13 sylan ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({M}\left({N}\mathrm{matRRep}{R}\right){1}_{{R}}\right){L}\in {B}$
15 6 14 eqeltrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\right)\to {K}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){L}\in {B}$