# Metamath Proof Explorer

## Theorem scmatmulcl

Description: The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-Aug-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatid.a ${⊢}{A}={N}\mathrm{Mat}{R}$
scmatid.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
scmatid.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
scmatid.0
scmatid.s ${⊢}{S}={N}\mathrm{ScMat}{R}$
Assertion scmatmulcl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({X}\in {S}\wedge {Y}\in {S}\right)\right)\to {X}{\cdot }_{{A}}{Y}\in {S}$

### Proof

Step Hyp Ref Expression
1 scmatid.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 scmatid.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 scmatid.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
4 scmatid.0
5 scmatid.s ${⊢}{S}={N}\mathrm{ScMat}{R}$
6 eqid ${⊢}{1}_{{A}}={1}_{{A}}$
7 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
8 3 1 2 6 7 5 scmatel ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({X}\in {S}↔\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\right)$
9 3 1 2 6 7 5 scmatel ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({Y}\in {S}↔\left({Y}\in {B}\wedge \exists {d}\in {E}\phantom{\rule{.4em}{0ex}}{Y}={d}{\cdot }_{{A}}{1}_{{A}}\right)\right)$
10 oveq12 ${⊢}\left({X}={c}{\cdot }_{{A}}{1}_{{A}}\wedge {Y}={d}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}=\left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)$
11 10 adantll ${⊢}\left(\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\wedge {X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\wedge {Y}={d}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}=\left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)$
12 simp-4l ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
13 simplr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\to {d}\in {E}$
14 13 anim1ci ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\to \left({c}\in {E}\wedge {d}\in {E}\right)$
15 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
16 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
17 1 3 4 6 7 15 16 scmatscmiddistr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({c}\in {E}\wedge {d}\in {E}\right)\right)\to \left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)=\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}$
18 12 14 17 syl2anc ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\to \left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)=\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}$
19 simpl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
20 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to {R}\in \mathrm{Ring}$
21 simprr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to {c}\in {E}$
22 simpl ${⊢}\left({d}\in {E}\wedge {c}\in {E}\right)\to {d}\in {E}$
23 22 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to {d}\in {E}$
24 3 15 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {c}\in {E}\wedge {d}\in {E}\right)\to {c}{\cdot }_{{R}}{d}\in {E}$
25 20 21 23 24 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to {c}{\cdot }_{{R}}{d}\in {E}$
26 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
27 2 6 ringidcl ${⊢}{A}\in \mathrm{Ring}\to {1}_{{A}}\in {B}$
28 26 27 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {1}_{{A}}\in {B}$
29 28 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to {1}_{{A}}\in {B}$
30 3 1 2 7 matvscl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({c}{\cdot }_{{R}}{d}\in {E}\wedge {1}_{{A}}\in {B}\right)\right)\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {B}$
31 19 25 29 30 syl12anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {B}$
32 oveq1 ${⊢}{e}={c}{\cdot }_{{R}}{d}\to {e}{\cdot }_{{A}}{1}_{{A}}=\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}$
33 32 eqeq2d ${⊢}{e}={c}{\cdot }_{{R}}{d}\to \left(\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}={e}{\cdot }_{{A}}{1}_{{A}}↔\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}=\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\right)$
34 33 adantl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\wedge {e}={c}{\cdot }_{{R}}{d}\right)\to \left(\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}={e}{\cdot }_{{A}}{1}_{{A}}↔\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}=\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\right)$
35 eqidd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}=\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}$
36 25 34 35 rspcedvd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to \exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}={e}{\cdot }_{{A}}{1}_{{A}}$
37 3 1 2 6 7 5 scmatel ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left(\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}↔\left(\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {B}\wedge \exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}={e}{\cdot }_{{A}}{1}_{{A}}\right)\right)$
38 37 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to \left(\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}↔\left(\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {B}\wedge \exists {e}\in {E}\phantom{\rule{.4em}{0ex}}\left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}={e}{\cdot }_{{A}}{1}_{{A}}\right)\right)$
39 31 36 38 mpbir2and ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({d}\in {E}\wedge {c}\in {E}\right)\right)\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}$
40 39 exp32 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({d}\in {E}\to \left({c}\in {E}\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}\right)\right)$
41 40 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\to \left({d}\in {E}\to \left({c}\in {E}\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}\right)\right)$
42 41 imp ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\to \left({c}\in {E}\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}\right)$
43 42 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\to \left({c}\in {E}\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}\right)$
44 43 imp ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\to \left({c}{\cdot }_{{R}}{d}\right){\cdot }_{{A}}{1}_{{A}}\in {S}$
45 18 44 eqeltrd ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\to \left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)\in {S}$
46 45 adantr ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\wedge {X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to \left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)\in {S}$
47 46 adantr ${⊢}\left(\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\wedge {X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\wedge {Y}={d}{\cdot }_{{A}}{1}_{{A}}\right)\to \left({c}{\cdot }_{{A}}{1}_{{A}}\right){\cdot }_{{A}}\left({d}{\cdot }_{{A}}{1}_{{A}}\right)\in {S}$
48 11 47 eqeltrd ${⊢}\left(\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\wedge {X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\wedge {Y}={d}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}\in {S}$
49 48 exp31 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\wedge {c}\in {E}\right)\to \left({X}={c}{\cdot }_{{A}}{1}_{{A}}\to \left({Y}={d}{\cdot }_{{A}}{1}_{{A}}\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
50 49 rexlimdva ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\wedge {X}\in {B}\right)\to \left(\exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\to \left({Y}={d}{\cdot }_{{A}}{1}_{{A}}\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
51 50 expimpd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\to \left(\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to \left({Y}={d}{\cdot }_{{A}}{1}_{{A}}\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
52 51 com23 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\wedge {d}\in {E}\right)\to \left({Y}={d}{\cdot }_{{A}}{1}_{{A}}\to \left(\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
53 52 rexlimdva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Y}\in {B}\right)\to \left(\exists {d}\in {E}\phantom{\rule{.4em}{0ex}}{Y}={d}{\cdot }_{{A}}{1}_{{A}}\to \left(\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
54 53 expimpd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left(\left({Y}\in {B}\wedge \exists {d}\in {E}\phantom{\rule{.4em}{0ex}}{Y}={d}{\cdot }_{{A}}{1}_{{A}}\right)\to \left(\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
55 9 54 sylbid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({Y}\in {S}\to \left(\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
56 55 com23 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left(\left({X}\in {B}\wedge \exists {c}\in {E}\phantom{\rule{.4em}{0ex}}{X}={c}{\cdot }_{{A}}{1}_{{A}}\right)\to \left({Y}\in {S}\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
57 8 56 sylbid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({X}\in {S}\to \left({Y}\in {S}\to {X}{\cdot }_{{A}}{Y}\in {S}\right)\right)$
58 57 imp32 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({X}\in {S}\wedge {Y}\in {S}\right)\right)\to {X}{\cdot }_{{A}}{Y}\in {S}$