Metamath Proof Explorer


Theorem mavmul0

Description: Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019)

Ref Expression
Hypothesis mavmul0.t · ˙ = R maVecMul N N
Assertion mavmul0 N = R V · ˙ =

Proof

Step Hyp Ref Expression
1 mavmul0.t · ˙ = R maVecMul N N
2 eqid N Mat R = N Mat R
3 eqid Base R = Base R
4 eqid R = R
5 simpr N = R V R V
6 0fin Fin
7 eleq1 N = N Fin Fin
8 6 7 mpbiri N = N Fin
9 8 adantr N = R V N Fin
10 0ex V
11 snidg V
12 10 11 mp1i N = R V
13 oveq1 N = N Mat R = Mat R
14 13 adantr N = R V N Mat R = Mat R
15 14 fveq2d N = R V Base N Mat R = Base Mat R
16 mat0dimbas0 R V Base Mat R =
17 16 adantl N = R V Base Mat R =
18 15 17 eqtrd N = R V Base N Mat R =
19 12 18 eleqtrrd N = R V Base N Mat R
20 eqidd N = =
21 el1o 1 𝑜 =
22 20 21 sylibr N = 1 𝑜
23 oveq2 N = Base R N = Base R
24 fvex Base R V
25 map0e Base R V Base R = 1 𝑜
26 24 25 mp1i N = Base R = 1 𝑜
27 23 26 eqtrd N = Base R N = 1 𝑜
28 22 27 eleqtrrd N = Base R N
29 28 adantr N = R V Base R N
30 2 1 3 4 5 9 19 29 mavmulval N = R V · ˙ = i N R j N i j R j
31 mpteq1 N = i N R j N i j R j = i R j N i j R j
32 31 adantr N = R V i N R j N i j R j = i R j N i j R j
33 mpt0 i R j N i j R j =
34 32 33 eqtrdi N = R V i N R j N i j R j =
35 30 34 eqtrd N = R V · ˙ =