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 e. V -> ( litMat ` M ) = ( i e. ( 1 ... ( # ` M ) ) , j e. ( 1 ... ( # ` ( M ` 0 ) ) ) |-> ( ( M ` ( i - 1 ) ) ` ( j - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( M e. V -> M e. _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 e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) ) = ( i e. ( 1 ... ( # ` M ) ) , j e. ( 1 ... ( # ` ( M ` 0 ) ) ) |-> ( ( M ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
10 df-lmat 
 |-  litMat = ( m e. _V |-> ( i e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
11 ovex 
 |-  ( 1 ... ( # ` M ) ) e. _V
12 ovex 
 |-  ( 1 ... ( # ` ( M ` 0 ) ) ) e. _V
13 11 12 mpoex 
 |-  ( i e. ( 1 ... ( # ` M ) ) , j e. ( 1 ... ( # ` ( M ` 0 ) ) ) |-> ( ( M ` ( i - 1 ) ) ` ( j - 1 ) ) ) e. _V
14 9 10 13 fvmpt 
 |-  ( M e. _V -> ( litMat ` M ) = ( i e. ( 1 ... ( # ` M ) ) , j e. ( 1 ... ( # ` ( M ` 0 ) ) ) |-> ( ( M ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
15 1 14 syl 
 |-  ( M e. V -> ( litMat ` M ) = ( i e. ( 1 ... ( # ` M ) ) , j e. ( 1 ... ( # ` ( M ` 0 ) ) ) |-> ( ( M ` ( i - 1 ) ) ` ( j - 1 ) ) ) )