# Metamath Proof Explorer

## Theorem mat1dimscm

Description: The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019)

Ref Expression
Hypotheses mat1dim.a ${⊢}{A}=\left\{{E}\right\}\mathrm{Mat}{R}$
mat1dim.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
mat1dim.o ${⊢}{O}=⟨{E},{E}⟩$
Assertion mat1dimscm ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{\cdot }_{{A}}\left\{⟨{O},{Y}⟩\right\}=\left\{⟨{O},{X}{\cdot }_{{R}}{Y}⟩\right\}$

### Proof

Step Hyp Ref Expression
1 mat1dim.a ${⊢}{A}=\left\{{E}\right\}\mathrm{Mat}{R}$
2 mat1dim.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 mat1dim.o ${⊢}{O}=⟨{E},{E}⟩$
4 opex ${⊢}⟨{E},{E}⟩\in \mathrm{V}$
5 3 4 eqeltri ${⊢}{O}\in \mathrm{V}$
6 5 a1i ${⊢}{Y}\in {B}\to {O}\in \mathrm{V}$
7 6 anim2i ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\in {B}\wedge {O}\in \mathrm{V}\right)$
8 7 ancomd ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({O}\in \mathrm{V}\wedge {X}\in {B}\right)$
9 fnsng ${⊢}\left({O}\in \mathrm{V}\wedge {X}\in {B}\right)\to \left\{⟨{O},{X}⟩\right\}Fn\left\{{O}\right\}$
10 8 9 syl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{X}⟩\right\}Fn\left\{{O}\right\}$
11 10 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{X}⟩\right\}Fn\left\{{O}\right\}$
12 xpsng ${⊢}\left({O}\in \mathrm{V}\wedge {X}\in {B}\right)\to \left\{{O}\right\}×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
13 8 12 syl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{{O}\right\}×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
14 13 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{{O}\right\}×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
15 14 fneq1d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{O}\right\}×\left\{{X}\right\}\right)Fn\left\{{O}\right\}↔\left\{⟨{O},{X}⟩\right\}Fn\left\{{O}\right\}\right)$
16 11 15 mpbird ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left\{{O}\right\}×\left\{{X}\right\}\right)Fn\left\{{O}\right\}$
17 xpsng ${⊢}\left({E}\in {V}\wedge {E}\in {V}\right)\to \left\{{E}\right\}×\left\{{E}\right\}=\left\{⟨{E},{E}⟩\right\}$
18 3 sneqi ${⊢}\left\{{O}\right\}=\left\{⟨{E},{E}⟩\right\}$
19 17 18 syl6eqr ${⊢}\left({E}\in {V}\wedge {E}\in {V}\right)\to \left\{{E}\right\}×\left\{{E}\right\}=\left\{{O}\right\}$
20 19 anidms ${⊢}{E}\in {V}\to \left\{{E}\right\}×\left\{{E}\right\}=\left\{{O}\right\}$
21 20 ad2antlr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{{E}\right\}×\left\{{E}\right\}=\left\{{O}\right\}$
22 21 xpeq1d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}=\left\{{O}\right\}×\left\{{X}\right\}$
23 22 fneq1d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)Fn\left\{{O}\right\}↔\left(\left\{{O}\right\}×\left\{{X}\right\}\right)Fn\left\{{O}\right\}\right)$
24 16 23 mpbird ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)Fn\left\{{O}\right\}$
25 5 a1i ${⊢}{X}\in {B}\to {O}\in \mathrm{V}$
26 fnsng ${⊢}\left({O}\in \mathrm{V}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{Y}⟩\right\}Fn\left\{{O}\right\}$
27 25 26 sylan ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{Y}⟩\right\}Fn\left\{{O}\right\}$
28 27 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{Y}⟩\right\}Fn\left\{{O}\right\}$
29 snex ${⊢}\left\{{O}\right\}\in \mathrm{V}$
30 29 a1i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{{O}\right\}\in \mathrm{V}$
31 inidm ${⊢}\left\{{O}\right\}\cap \left\{{O}\right\}=\left\{{O}\right\}$
32 elsni ${⊢}{x}\in \left\{{O}\right\}\to {x}={O}$
33 fveq2 ${⊢}{x}={O}\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({x}\right)=\left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({O}\right)$
34 17 anidms ${⊢}{E}\in {V}\to \left\{{E}\right\}×\left\{{E}\right\}=\left\{⟨{E},{E}⟩\right\}$
35 34 ad2antlr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{{E}\right\}×\left\{{E}\right\}=\left\{⟨{E},{E}⟩\right\}$
36 35 xpeq1d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}=\left\{⟨{E},{E}⟩\right\}×\left\{{X}\right\}$
37 4 a1i ${⊢}{Y}\in {B}\to ⟨{E},{E}⟩\in \mathrm{V}$
38 37 anim2i ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\in {B}\wedge ⟨{E},{E}⟩\in \mathrm{V}\right)$
39 38 ancomd ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left(⟨{E},{E}⟩\in \mathrm{V}\wedge {X}\in {B}\right)$
40 xpsng ${⊢}\left(⟨{E},{E}⟩\in \mathrm{V}\wedge {X}\in {B}\right)\to \left\{⟨{E},{E}⟩\right\}×\left\{{X}\right\}=\left\{⟨⟨{E},{E}⟩,{X}⟩\right\}$
41 3 eqcomi ${⊢}⟨{E},{E}⟩={O}$
42 41 opeq1i ${⊢}⟨⟨{E},{E}⟩,{X}⟩=⟨{O},{X}⟩$
43 42 sneqi ${⊢}\left\{⟨⟨{E},{E}⟩,{X}⟩\right\}=\left\{⟨{O},{X}⟩\right\}$
44 40 43 syl6eq ${⊢}\left(⟨{E},{E}⟩\in \mathrm{V}\wedge {X}\in {B}\right)\to \left\{⟨{E},{E}⟩\right\}×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
45 39 44 syl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{⟨{E},{E}⟩\right\}×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
46 45 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{E},{E}⟩\right\}×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
47 36 46 eqtrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}=\left\{⟨{O},{X}⟩\right\}$
48 47 fveq1d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({O}\right)=\left\{⟨{O},{X}⟩\right\}\left({O}\right)$
49 fvsng ${⊢}\left({O}\in \mathrm{V}\wedge {X}\in {B}\right)\to \left\{⟨{O},{X}⟩\right\}\left({O}\right)={X}$
50 8 49 syl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{X}⟩\right\}\left({O}\right)={X}$
51 50 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{X}⟩\right\}\left({O}\right)={X}$
52 48 51 eqtrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({O}\right)={X}$
53 33 52 sylan9eq ${⊢}\left({x}={O}\wedge \left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({x}\right)={X}$
54 53 ex ${⊢}{x}={O}\to \left(\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({x}\right)={X}\right)$
55 32 54 syl ${⊢}{x}\in \left\{{O}\right\}\to \left(\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({x}\right)={X}\right)$
56 55 impcom ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {x}\in \left\{{O}\right\}\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right)\left({x}\right)={X}$
57 fveq2 ${⊢}{x}={O}\to \left\{⟨{O},{Y}⟩\right\}\left({x}\right)=\left\{⟨{O},{Y}⟩\right\}\left({O}\right)$
58 fvsng ${⊢}\left({O}\in \mathrm{V}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{Y}⟩\right\}\left({O}\right)={Y}$
59 25 58 sylan ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{Y}⟩\right\}\left({O}\right)={Y}$
60 59 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{Y}⟩\right\}\left({O}\right)={Y}$
61 57 60 sylan9eq ${⊢}\left({x}={O}\wedge \left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\right)\to \left\{⟨{O},{Y}⟩\right\}\left({x}\right)={Y}$
62 61 ex ${⊢}{x}={O}\to \left(\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{Y}⟩\right\}\left({x}\right)={Y}\right)$
63 32 62 syl ${⊢}{x}\in \left\{{O}\right\}\to \left(\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{Y}⟩\right\}\left({x}\right)={Y}\right)$
64 63 impcom ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {x}\in \left\{{O}\right\}\right)\to \left\{⟨{O},{Y}⟩\right\}\left({x}\right)={Y}$
65 24 28 30 30 31 56 64 offval ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}\left\{⟨{O},{Y}⟩\right\}=\left({x}\in \left\{{O}\right\}⟼{X}{\cdot }_{{R}}{Y}\right)$
66 simprl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
67 simpr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
68 67 anim2i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge {Y}\in {B}\right)$
69 df-3an ${⊢}\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\wedge {Y}\in {B}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge {Y}\in {B}\right)$
70 68 69 sylibr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {E}\in {V}\wedge {Y}\in {B}\right)$
71 1 2 3 mat1dimbas ${⊢}\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\wedge {Y}\in {B}\right)\to \left\{⟨{O},{Y}⟩\right\}\in {\mathrm{Base}}_{{A}}$
72 70 71 syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{Y}⟩\right\}\in {\mathrm{Base}}_{{A}}$
73 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
74 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
75 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
76 eqid ${⊢}\left\{{E}\right\}×\left\{{E}\right\}=\left\{{E}\right\}×\left\{{E}\right\}$
77 1 73 2 74 75 76 matvsca2 ${⊢}\left({X}\in {B}\wedge \left\{⟨{O},{Y}⟩\right\}\in {\mathrm{Base}}_{{A}}\right)\to {X}{\cdot }_{{A}}\left\{⟨{O},{Y}⟩\right\}=\left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}\left\{⟨{O},{Y}⟩\right\}$
78 66 72 77 syl2anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{\cdot }_{{A}}\left\{⟨{O},{Y}⟩\right\}=\left(\left(\left\{{E}\right\}×\left\{{E}\right\}\right)×\left\{{X}\right\}\right){{\cdot }_{{R}}}_{f}\left\{⟨{O},{Y}⟩\right\}$
79 3anass ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {Y}\in {B}\right)↔\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)$
80 79 biimpri ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {Y}\in {B}\right)$
81 80 adantlr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {Y}\in {B}\right)$
82 2 75 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}{\cdot }_{{R}}{Y}\in {B}$
83 81 82 syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{\cdot }_{{R}}{Y}\in {B}$
84 fmptsn ${⊢}\left({O}\in \mathrm{V}\wedge {X}{\cdot }_{{R}}{Y}\in {B}\right)\to \left\{⟨{O},{X}{\cdot }_{{R}}{Y}⟩\right\}=\left({x}\in \left\{{O}\right\}⟼{X}{\cdot }_{{R}}{Y}\right)$
85 5 83 84 sylancr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left\{⟨{O},{X}{\cdot }_{{R}}{Y}⟩\right\}=\left({x}\in \left\{{O}\right\}⟼{X}{\cdot }_{{R}}{Y}\right)$
86 65 78 85 3eqtr4d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {E}\in {V}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{\cdot }_{{A}}\left\{⟨{O},{Y}⟩\right\}=\left\{⟨{O},{X}{\cdot }_{{R}}{Y}⟩\right\}$