Metamath Proof Explorer


Theorem mamuval

Description: Multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mamufval.f F=RmaMulMNP
mamufval.b B=BaseR
mamufval.t ·˙=R
mamufval.r φRV
mamufval.m φMFin
mamufval.n φNFin
mamufval.p φPFin
mamuval.x φXBM×N
mamuval.y φYBN×P
Assertion mamuval φXFY=iM,kPRjNiXj·˙jYk

Proof

Step Hyp Ref Expression
1 mamufval.f F=RmaMulMNP
2 mamufval.b B=BaseR
3 mamufval.t ·˙=R
4 mamufval.r φRV
5 mamufval.m φMFin
6 mamufval.n φNFin
7 mamufval.p φPFin
8 mamuval.x φXBM×N
9 mamuval.y φYBN×P
10 1 2 3 4 5 6 7 mamufval φF=xBM×N,yBN×PiM,kPRjNixj·˙jyk
11 oveq x=Xixj=iXj
12 oveq y=Yjyk=jYk
13 11 12 oveqan12d x=Xy=Yixj·˙jyk=iXj·˙jYk
14 13 adantl φx=Xy=Yixj·˙jyk=iXj·˙jYk
15 14 mpteq2dv φx=Xy=YjNixj·˙jyk=jNiXj·˙jYk
16 15 oveq2d φx=Xy=YRjNixj·˙jyk=RjNiXj·˙jYk
17 16 mpoeq3dv φx=Xy=YiM,kPRjNixj·˙jyk=iM,kPRjNiXj·˙jYk
18 mpoexga MFinPFiniM,kPRjNiXj·˙jYkV
19 5 7 18 syl2anc φiM,kPRjNiXj·˙jYkV
20 10 17 8 9 19 ovmpod φXFY=iM,kPRjNiXj·˙jYk