# Metamath Proof Explorer

## Theorem ma1repveval

Description: An entry of an identity matrix with a replaced column. (Contributed by AV, 16-Feb-2019) (Revised by AV, 26-Feb-2019)

Ref Expression
Hypotheses marepvcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
marepvcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
marepvcl.v ${⊢}{V}={{\mathrm{Base}}_{{R}}}^{{N}}$
ma1repvcl.1
mulmarep1el.0
mulmarep1el.e
Assertion ma1repveval

### Proof

Step Hyp Ref Expression
1 marepvcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 marepvcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 marepvcl.v ${⊢}{V}={{\mathrm{Base}}_{{R}}}^{{N}}$
4 ma1repvcl.1
5 mulmarep1el.0
6 mulmarep1el.e
7 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
8 7 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
9 1 fveq2i ${⊢}{1}_{{A}}={1}_{\left({N}\mathrm{Mat}{R}\right)}$
10 4 9 eqtri
11 1 2 10 mat1bas
12 11 expcom
13 8 12 syl
15 14 impcom
16 simpr2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\right)\to {C}\in {V}$
17 simpr3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\right)\to {K}\in {N}$
18 15 16 17 3jca
19 6 a1i
20 19 oveqd
21 eqid ${⊢}{N}\mathrm{matRepV}{R}={N}\mathrm{matRepV}{R}$
22 1 2 21 3 marepveval
23 20 22 eqtrd
24 18 23 stoic3
25 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
26 8 3ad2ant1 ${⊢}\left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\to {N}\in \mathrm{Fin}$
27 26 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
28 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
29 simp3l ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\in {N}$
30 simp3r ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {J}\in {N}$
31 1 25 5 27 28 29 30 4 mat1ov
32 eqcom ${⊢}{I}={J}↔{J}={I}$
33 32 a1i ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({M}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to \left({I}={J}↔{J}={I}\right)$
34 33 ifbid
35 31 34 eqtrd
36 35 ifeq2d
37 24 36 eqtrd