# Metamath Proof Explorer

## Theorem mulmarep1el

Description: Element by element multiplication of a matrix with an identity matrix with a column replaced by a vector. (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 mulmarep1el

### 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 simp3 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\to {L}\in {N}$
8 simp2 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\to {J}\in {N}$
9 7 8 jca ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\to \left({L}\in {N}\wedge {J}\in {N}\right)$
10 1 2 3 4 5 6 ma1repveval
11 9 10 syl3an3
12 11 oveq2d
13 ovif2
14 13 a1i
15 ovif2
16 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
17 simp1 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\to {I}\in {N}$
18 17 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\right)\to {I}\in {N}$
19 7 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\right)\to {L}\in {N}$
20 2 eleq2i ${⊢}{X}\in {B}↔{X}\in {\mathrm{Base}}_{{A}}$
21 20 biimpi ${⊢}{X}\in {B}\to {X}\in {\mathrm{Base}}_{{A}}$
22 21 3ad2ant1 ${⊢}\left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\to {X}\in {\mathrm{Base}}_{{A}}$
23 22 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\right)\to {X}\in {\mathrm{Base}}_{{A}}$
24 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
25 1 24 matecl ${⊢}\left({I}\in {N}\wedge {L}\in {N}\wedge {X}\in {\mathrm{Base}}_{{A}}\right)\to {I}{X}{L}\in {\mathrm{Base}}_{{R}}$
26 18 19 23 25 syl3anc ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\right)\to {I}{X}{L}\in {\mathrm{Base}}_{{R}}$
27 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
28 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
29 24 27 28 ringridm ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}{X}{L}\in {\mathrm{Base}}_{{R}}\right)\to \left({I}{X}{L}\right){\cdot }_{{R}}{1}_{{R}}={I}{X}{L}$
30 16 26 29 syl2anc ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {C}\in {V}\wedge {K}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {L}\in {N}\right)\right)\to \left({I}{X}{L}\right){\cdot }_{{R}}{1}_{{R}}={I}{X}{L}$
31 24 27 5 ringrz
32 16 26 31 syl2anc
33 30 32 ifeq12d
34 15 33 syl5eq
35 34 ifeq2d
36 12 14 35 3eqtrd