Metamath Proof Explorer


Theorem lmatval

Description: Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020)

Ref Expression
Assertion lmatval M V litMat M = i 1 M , j 1 M 0 M i 1 j 1

Proof

Step Hyp Ref Expression
1 elex M V M V
2 fveq2 m = M m = M
3 2 oveq2d m = M 1 m = 1 M
4 fveq1 m = M m 0 = M 0
5 4 fveq2d m = M m 0 = M 0
6 5 oveq2d m = M 1 m 0 = 1 M 0
7 fveq1 m = M m i 1 = M i 1
8 7 fveq1d m = M m i 1 j 1 = M i 1 j 1
9 3 6 8 mpoeq123dv m = M i 1 m , j 1 m 0 m i 1 j 1 = i 1 M , j 1 M 0 M i 1 j 1
10 df-lmat litMat = m V i 1 m , j 1 m 0 m i 1 j 1
11 ovex 1 M V
12 ovex 1 M 0 V
13 11 12 mpoex i 1 M , j 1 M 0 M i 1 j 1 V
14 9 10 13 fvmpt M V litMat M = i 1 M , j 1 M 0 M i 1 j 1
15 1 14 syl M V litMat M = i 1 M , j 1 M 0 M i 1 j 1