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