Metamath Proof Explorer

Theorem mat1dimmul

Description: The ring multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Hypotheses mat1dim.a ⊢A=EMatR
mat1dim.b ⊢B=BaseR
mat1dim.o ⊢O=EE
Assertion mat1dimmul ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX⋅AOY=OX⋅RY

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢A=EMatR
2 mat1dim.b ⊢B=BaseR
3 mat1dim.o ⊢O=EE
4 snfi ⊢E∈Fin
5 simpl ⊢R∈Ring∧E∈V→R∈Ring
6 eqid ⊢RmaMulEEE=RmaMulEEE
7 1 6 matmulr ⊢E∈Fin∧R∈Ring→RmaMulEEE=⋅A
8 7 eqcomd ⊢E∈Fin∧R∈Ring→⋅A=RmaMulEEE
9 4 5 8 sylancr ⊢R∈Ring∧E∈V→⋅A=RmaMulEEE
10 9 adantr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→⋅A=RmaMulEEE
11 10 oveqd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX⋅AOY=OXRmaMulEEEOY
12 eqid ⊢⋅R=⋅R
13 5 adantr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→R∈Ring
14 4 a1i ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→E∈Fin
15 opex ⊢EE∈V
16 15 a1i ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EE∈V
17 simpl ⊢X∈B∧Y∈B→X∈B
18 17 adantl ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→X∈B
19 16 18 fsnd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EEX:EE⟶B
20 3 opeq1i ⊢OX=EEX
21 20 sneqi ⊢OX=EEX
22 21 a1i ⊢E∈V→OX=EEX
23 xpsng ⊢E∈V∧E∈V→E×E=EE
24 23 anidms ⊢E∈V→E×E=EE
25 22 24 feq12d ⊢E∈V→OX:E×E⟶B↔EEX:EE⟶B
26 25 ad2antlr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX:E×E⟶B↔EEX:EE⟶B
27 19 26 mpbird ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX:E×E⟶B
28 2 fvexi ⊢B∈V
29 28 a1i ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→B∈V
30 snex ⊢E∈V
31 30 30 xpex ⊢E×E∈V
32 31 a1i ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→E×E∈V
33 29 32 elmapd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX∈BE×E↔OX:E×E⟶B
34 27 33 mpbird ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX∈BE×E
35 simpr ⊢X∈B∧Y∈B→Y∈B
36 35 adantl ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→Y∈B
37 16 36 fsnd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EEY:EE⟶B
38 3 opeq1i ⊢OY=EEY
39 38 sneqi ⊢OY=EEY
40 39 a1i ⊢E∈V→OY=EEY
41 40 24 feq12d ⊢E∈V→OY:E×E⟶B↔EEY:EE⟶B
42 41 ad2antlr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OY:E×E⟶B↔EEY:EE⟶B
43 37 42 mpbird ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OY:E×E⟶B
44 29 32 elmapd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OY∈BE×E↔OY:E×E⟶B
45 43 44 mpbird ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OY∈BE×E
46 6 2 12 13 14 14 14 34 45 mamuval ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OXRmaMulEEEOY=x∈E,y∈E⟼∑Rk∈ExOXk⋅RkOYy
47 simpr ⊢R∈Ring∧E∈V→E∈V
48 47 adantr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→E∈V
49 eqid ⊢BaseR=BaseR
50 ringcmn ⊢R∈Ring→R∈CMnd
51 50 ad2antrr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→R∈CMnd
52 df-ov ⊢EOXE=OX⁡EE
53 21 fveq1i ⊢OX⁡EE=EEX⁡EE
54 52 53 eqtri ⊢EOXE=EEX⁡EE
55 15 a1i ⊢Y∈B→EE∈V
56 55 anim2i ⊢X∈B∧Y∈B→X∈B∧EE∈V
57 56 ancomd ⊢X∈B∧Y∈B→EE∈V∧X∈B
58 fvsng ⊢EE∈V∧X∈B→EEX⁡EE=X
59 57 58 syl ⊢X∈B∧Y∈B→EEX⁡EE=X
60 59 adantl ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EEX⁡EE=X
61 54 60 eqtrid ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EOXE=X
62 61 18 eqeltrd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EOXE∈B
63 df-ov ⊢EOYE=OY⁡EE
64 39 fveq1i ⊢OY⁡EE=EEY⁡EE
65 63 64 eqtri ⊢EOYE=EEY⁡EE
66 15 a1i ⊢X∈B→EE∈V
67 fvsng ⊢EE∈V∧Y∈B→EEY⁡EE=Y
68 66 67 sylan ⊢X∈B∧Y∈B→EEY⁡EE=Y
69 68 adantl ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EEY⁡EE=Y
70 65 69 eqtrid ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EOYE=Y
71 70 36 eqeltrd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EOYE∈B
72 2 12 ringcl ⊢R∈Ring∧EOXE∈B∧EOYE∈B→EOXE⋅REOYE∈B
73 13 62 71 72 syl3anc ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EOXE⋅REOYE∈B
74 oveq2 ⊢k=E→EOXk=EOXE
75 oveq1 ⊢k=E→kOYE=EOYE
76 74 75 oveq12d ⊢k=E→EOXk⋅RkOYE=EOXE⋅REOYE
77 2 eqcomi ⊢BaseR=B
78 77 a1i ⊢k=E→BaseR=B
79 76 78 eleq12d ⊢k=E→EOXk⋅RkOYE∈BaseR↔EOXE⋅REOYE∈B
80 79 ralsng ⊢E∈V→∀k∈EEOXk⋅RkOYE∈BaseR↔EOXE⋅REOYE∈B
81 80 ad2antlr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→∀k∈EEOXk⋅RkOYE∈BaseR↔EOXE⋅REOYE∈B
82 73 81 mpbird ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→∀k∈EEOXk⋅RkOYE∈BaseR
83 49 51 14 82 gsummptcl ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→∑Rk∈EEOXk⋅RkOYE∈BaseR
84 eqid ⊢x∈E,y∈E⟼∑Rk∈ExOXk⋅RkOYy=x∈E,y∈E⟼∑Rk∈ExOXk⋅RkOYy
85 oveq1 ⊢x=E→xOXk=EOXk
86 85 oveq1d ⊢x=E→xOXk⋅RkOYy=EOXk⋅RkOYy
87 86 mpteq2dv ⊢x=E→k∈E⟼xOXk⋅RkOYy=k∈E⟼EOXk⋅RkOYy
88 87 oveq2d ⊢x=E→∑Rk∈ExOXk⋅RkOYy=∑Rk∈EEOXk⋅RkOYy
89 oveq2 ⊢y=E→kOYy=kOYE
90 89 oveq2d ⊢y=E→EOXk⋅RkOYy=EOXk⋅RkOYE
91 90 mpteq2dv ⊢y=E→k∈E⟼EOXk⋅RkOYy=k∈E⟼EOXk⋅RkOYE
92 91 oveq2d ⊢y=E→∑Rk∈EEOXk⋅RkOYy=∑Rk∈EEOXk⋅RkOYE
93 84 88 92 mposn ⊢E∈V∧E∈V∧∑Rk∈EEOXk⋅RkOYE∈BaseR→x∈E,y∈E⟼∑Rk∈ExOXk⋅RkOYy=EE∑Rk∈EEOXk⋅RkOYE
94 48 48 83 93 syl3anc ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→x∈E,y∈E⟼∑Rk∈ExOXk⋅RkOYy=EE∑Rk∈EEOXk⋅RkOYE
95 3 eqcomi ⊢EE=O
96 95 a1i ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EE=O
97 ringmnd ⊢R∈Ring→R∈Mnd
98 97 ad2antrr ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→R∈Mnd
99 2 76 gsumsn ⊢R∈Mnd∧E∈V∧EOXE⋅REOYE∈B→∑Rk∈EEOXk⋅RkOYE=EOXE⋅REOYE
100 98 48 73 99 syl3anc ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→∑Rk∈EEOXk⋅RkOYE=EOXE⋅REOYE
101 96 100 opeq12d ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EE∑Rk∈EEOXk⋅RkOYE=OEOXE⋅REOYE
102 101 sneqd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EE∑Rk∈EEOXk⋅RkOYE=OEOXE⋅REOYE
103 61 70 oveq12d ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→EOXE⋅REOYE=X⋅RY
104 103 opeq2d ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OEOXE⋅REOYE=OX⋅RY
105 104 sneqd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OEOXE⋅REOYE=OX⋅RY
106 94 102 105 3eqtrd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→x∈E,y∈E⟼∑Rk∈ExOXk⋅RkOYy=OX⋅RY
107 11 46 106 3eqtrd ⊢R∈Ring∧E∈V∧X∈B∧Y∈B→OX⋅AOY=OX⋅RY