Metamath Proof Explorer


Theorem matmulcell

Description: Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses matmulcell.a A = N Mat R
matmulcell.b B = Base A
matmulcell.m × ˙ = A
Assertion matmulcell R Ring X B Y B I N J N I X × ˙ Y J = R j N I X j R j Y J

Proof

Step Hyp Ref Expression
1 matmulcell.a A = N Mat R
2 matmulcell.b B = Base A
3 matmulcell.m × ˙ = A
4 1 2 matrcl X B N Fin R V
5 eqid R maMul N N N = R maMul N N N
6 1 5 matmulr N Fin R V R maMul N N N = A
7 3 6 eqtr4id N Fin R V × ˙ = R maMul N N N
8 7 a1d N Fin R V R Ring × ˙ = R maMul N N N
9 4 8 syl X B R Ring × ˙ = R maMul N N N
10 9 adantr X B Y B R Ring × ˙ = R maMul N N N
11 10 impcom R Ring X B Y B × ˙ = R maMul N N N
12 11 3adant3 R Ring X B Y B I N J N × ˙ = R maMul N N N
13 12 oveqd R Ring X B Y B I N J N X × ˙ Y = X R maMul N N N Y
14 13 oveqd R Ring X B Y B I N J N I X × ˙ Y J = I X R maMul N N N Y J
15 eqid Base R = Base R
16 eqid R = R
17 simp1 R Ring X B Y B I N J N R Ring
18 4 simpld X B N Fin
19 18 adantr X B Y B N Fin
20 19 3ad2ant2 R Ring X B Y B I N J N N Fin
21 1 15 2 matbas2i X B X Base R N × N
22 21 adantr X B Y B X Base R N × N
23 22 3ad2ant2 R Ring X B Y B I N J N X Base R N × N
24 1 15 2 matbas2i Y B Y Base R N × N
25 24 adantl X B Y B Y Base R N × N
26 25 3ad2ant2 R Ring X B Y B I N J N Y Base R N × N
27 simp3l R Ring X B Y B I N J N I N
28 simp3r R Ring X B Y B I N J N J N
29 5 15 16 17 20 20 20 23 26 27 28 mamufv R Ring X B Y B I N J N I X R maMul N N N Y J = R j N I X j R j Y J
30 14 29 eqtrd R Ring X B Y B I N J N I X × ˙ Y J = R j N I X j R j Y J