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