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 = E Mat R
mat1dim.b ⊢ B = Base R
mat1dim.o ⊢ O = E E
Assertion mat1dimmul ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X ⋅ A O Y = O X ⋅ R Y

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ A = E Mat R
2 mat1dim.b ⊢ B = Base R
3 mat1dim.o ⊢ O = E E
4 snfi ⊢ E ∈ Fin
5 simpl ⊢ R ∈ Ring ∧ E ∈ V → R ∈ Ring
6 eqid ⊢ R maMul E E E = R maMul E E E
7 1 6 matmulr ⊢ E ∈ Fin ∧ R ∈ Ring → R maMul E E E = ⋅ A
8 7 eqcomd ⊢ E ∈ Fin ∧ R ∈ Ring → ⋅ A = R maMul E E E
9 4 5 8 sylancr ⊢ R ∈ Ring ∧ E ∈ V → ⋅ A = R maMul E E E
10 9 adantr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → ⋅ A = R maMul E E E
11 10 oveqd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X ⋅ A O Y = O X R maMul E E E O Y
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 ⊢ E E ∈ V
16 15 a1i ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E E ∈ 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 → E E X : E E ⟶ B
20 3 opeq1i ⊢ O X = E E X
21 20 sneqi ⊢ O X = E E X
22 21 a1i ⊢ E ∈ V → O X = E E X
23 xpsng ⊢ E ∈ V ∧ E ∈ V → E × E = E E
24 23 anidms ⊢ E ∈ V → E × E = E E
25 22 24 feq12d ⊢ E ∈ V → O X : E × E ⟶ B ↔ E E X : E E ⟶ B
26 25 ad2antlr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X : E × E ⟶ B ↔ E E X : E E ⟶ B
27 19 26 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X : 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 → O X ∈ B E × E ↔ O X : E × E ⟶ B
34 27 33 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X ∈ B E × 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 → E E Y : E E ⟶ B
38 3 opeq1i ⊢ O Y = E E Y
39 38 sneqi ⊢ O Y = E E Y
40 39 a1i ⊢ E ∈ V → O Y = E E Y
41 40 24 feq12d ⊢ E ∈ V → O Y : E × E ⟶ B ↔ E E Y : E E ⟶ B
42 41 ad2antlr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O Y : E × E ⟶ B ↔ E E Y : E E ⟶ B
43 37 42 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O Y : E × E ⟶ B
44 29 32 elmapd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O Y ∈ B E × E ↔ O Y : E × E ⟶ B
45 43 44 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O Y ∈ B E × E
46 6 2 12 13 14 14 14 34 45 mamuval ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X R maMul E E E O Y = x ∈ E , y ∈ E ⟼ ∑ R k ∈ E x O X k ⋅ R k O Y y
47 simpr ⊢ R ∈ Ring ∧ E ∈ V → E ∈ V
48 47 adantr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E ∈ V
49 eqid ⊢ Base R = Base R
50 ringcmn ⊢ R ∈ Ring → R ∈ CMnd
51 50 ad2antrr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → R ∈ CMnd
52 df-ov ⊢ E O X E = O X ⁡ E E
53 21 fveq1i ⊢ O X ⁡ E E = E E X ⁡ E E
54 52 53 eqtri ⊢ E O X E = E E X ⁡ E E
55 15 a1i ⊢ Y ∈ B → E E ∈ V
56 55 anim2i ⊢ X ∈ B ∧ Y ∈ B → X ∈ B ∧ E E ∈ V
57 56 ancomd ⊢ X ∈ B ∧ Y ∈ B → E E ∈ V ∧ X ∈ B
58 fvsng ⊢ E E ∈ V ∧ X ∈ B → E E X ⁡ E E = X
59 57 58 syl ⊢ X ∈ B ∧ Y ∈ B → E E X ⁡ E E = X
60 59 adantl ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E E X ⁡ E E = X
61 54 60 syl5eq ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E O X E = X
62 61 18 eqeltrd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E O X E ∈ B
63 df-ov ⊢ E O Y E = O Y ⁡ E E
64 39 fveq1i ⊢ O Y ⁡ E E = E E Y ⁡ E E
65 63 64 eqtri ⊢ E O Y E = E E Y ⁡ E E
66 15 a1i ⊢ X ∈ B → E E ∈ V
67 fvsng ⊢ E E ∈ V ∧ Y ∈ B → E E Y ⁡ E E = Y
68 66 67 sylan ⊢ X ∈ B ∧ Y ∈ B → E E Y ⁡ E E = Y
69 68 adantl ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E E Y ⁡ E E = Y
70 65 69 syl5eq ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E O Y E = Y
71 70 36 eqeltrd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E O Y E ∈ B
72 2 12 ringcl ⊢ R ∈ Ring ∧ E O X E ∈ B ∧ E O Y E ∈ B → E O X E ⋅ R E O Y E ∈ B
73 13 62 71 72 syl3anc ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E O X E ⋅ R E O Y E ∈ B
74 oveq2 ⊢ k = E → E O X k = E O X E
75 oveq1 ⊢ k = E → k O Y E = E O Y E
76 74 75 oveq12d ⊢ k = E → E O X k ⋅ R k O Y E = E O X E ⋅ R E O Y E
77 2 eqcomi ⊢ Base R = B
78 77 a1i ⊢ k = E → Base R = B
79 76 78 eleq12d ⊢ k = E → E O X k ⋅ R k O Y E ∈ Base R ↔ E O X E ⋅ R E O Y E ∈ B
80 79 ralsng ⊢ E ∈ V → ∀ k ∈ E E O X k ⋅ R k O Y E ∈ Base R ↔ E O X E ⋅ R E O Y E ∈ B
81 80 ad2antlr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → ∀ k ∈ E E O X k ⋅ R k O Y E ∈ Base R ↔ E O X E ⋅ R E O Y E ∈ B
82 73 81 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → ∀ k ∈ E E O X k ⋅ R k O Y E ∈ Base R
83 49 51 14 82 gsummptcl ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → ∑ R k ∈ E E O X k ⋅ R k O Y E ∈ Base R
84 eqid ⊢ x ∈ E , y ∈ E ⟼ ∑ R k ∈ E x O X k ⋅ R k O Y y = x ∈ E , y ∈ E ⟼ ∑ R k ∈ E x O X k ⋅ R k O Y y
85 oveq1 ⊢ x = E → x O X k = E O X k
86 85 oveq1d ⊢ x = E → x O X k ⋅ R k O Y y = E O X k ⋅ R k O Y y
87 86 mpteq2dv ⊢ x = E → k ∈ E ⟼ x O X k ⋅ R k O Y y = k ∈ E ⟼ E O X k ⋅ R k O Y y
88 87 oveq2d ⊢ x = E → ∑ R k ∈ E x O X k ⋅ R k O Y y = ∑ R k ∈ E E O X k ⋅ R k O Y y
89 oveq2 ⊢ y = E → k O Y y = k O Y E
90 89 oveq2d ⊢ y = E → E O X k ⋅ R k O Y y = E O X k ⋅ R k O Y E
91 90 mpteq2dv ⊢ y = E → k ∈ E ⟼ E O X k ⋅ R k O Y y = k ∈ E ⟼ E O X k ⋅ R k O Y E
92 91 oveq2d ⊢ y = E → ∑ R k ∈ E E O X k ⋅ R k O Y y = ∑ R k ∈ E E O X k ⋅ R k O Y E
93 84 88 92 mposn ⊢ E ∈ V ∧ E ∈ V ∧ ∑ R k ∈ E E O X k ⋅ R k O Y E ∈ Base R → x ∈ E , y ∈ E ⟼ ∑ R k ∈ E x O X k ⋅ R k O Y y = E E ∑ R k ∈ E E O X k ⋅ R k O Y E
94 48 48 83 93 syl3anc ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → x ∈ E , y ∈ E ⟼ ∑ R k ∈ E x O X k ⋅ R k O Y y = E E ∑ R k ∈ E E O X k ⋅ R k O Y E
95 3 eqcomi ⊢ E E = O
96 95 a1i ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E E = 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 ∧ E O X E ⋅ R E O Y E ∈ B → ∑ R k ∈ E E O X k ⋅ R k O Y E = E O X E ⋅ R E O Y E
100 98 48 73 99 syl3anc ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → ∑ R k ∈ E E O X k ⋅ R k O Y E = E O X E ⋅ R E O Y E
101 96 100 opeq12d ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E E ∑ R k ∈ E E O X k ⋅ R k O Y E = O E O X E ⋅ R E O Y E
102 101 sneqd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E E ∑ R k ∈ E E O X k ⋅ R k O Y E = O E O X E ⋅ R E O Y E
103 61 70 oveq12d ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → E O X E ⋅ R E O Y E = X ⋅ R Y
104 103 opeq2d ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O E O X E ⋅ R E O Y E = O X ⋅ R Y
105 104 sneqd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O E O X E ⋅ R E O Y E = O X ⋅ R Y
106 94 102 105 3eqtrd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → x ∈ E , y ∈ E ⟼ ∑ R k ∈ E x O X k ⋅ R k O Y y = O X ⋅ R Y
107 11 46 106 3eqtrd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B ∧ Y ∈ B → O X ⋅ A O Y = O X ⋅ R Y