Metamath Proof Explorer

Theorem smatfval

Description: Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Assertion smatfval 
|- ( ( K e. NN /\ L e. NN /\ M e. V ) -> ( K ( subMat1 ` M ) L ) = ( M o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( M e. V -> M e. _V )
2 1 3ad2ant3 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> M e. _V )
3 coeq1 
 |-  ( m = M -> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) = ( M o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) )
4 3 mpoeq3dv 
 |-  ( m = M -> ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) = ( k e. NN , l e. NN |-> ( M o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )
5 df-smat 
 |-  subMat1 = ( m e. _V |-> ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )
6 nnex 
 |-  NN e. _V
7 6 6 mpoex 
 |-  ( k e. NN , l e. NN |-> ( M o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) e. _V
8 4 5 7 fvmpt 
 |-  ( M e. _V -> ( subMat1 ` M ) = ( k e. NN , l e. NN |-> ( M o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )
9 2 8 syl 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> ( subMat1 ` M ) = ( k e. NN , l e. NN |-> ( M o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )
10 breq2 
 |-  ( k = K -> ( i < k <-> i < K ) )
11 10 ifbid 
 |-  ( k = K -> if ( i < k , i , ( i + 1 ) ) = if ( i < K , i , ( i + 1 ) ) )
12 11 opeq1d 
 |-  ( k = K -> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. = <. if ( i < K , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. )
13 12 mpoeq3dv 
 |-  ( k = K -> ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) = ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) )
14 breq2 
 |-  ( l = L -> ( j < l <-> j < L ) )
15 14 ifbid 
 |-  ( l = L -> if ( j < l , j , ( j + 1 ) ) = if ( j < L , j , ( j + 1 ) ) )
16 15 opeq2d 
 |-  ( l = L -> <. if ( i < K , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. = <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. )
17 16 mpoeq3dv 
 |-  ( l = L -> ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) = ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) )
18 13 17 sylan9eq 
 |-  ( ( k = K /\ l = L ) -> ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) = ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) )
19 18 adantl 
 |-  ( ( ( K e. NN /\ L e. NN /\ M e. V ) /\ ( k = K /\ l = L ) ) -> ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) = ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) )
20 19 coeq2d 
 |-  ( ( ( K e. NN /\ L e. NN /\ M e. V ) /\ ( k = K /\ l = L ) ) -> ( M o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) = ( M o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )
21 simp1 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> K e. NN )
22 simp2 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> L e. NN )
23 simp3 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> M e. V )
24 6 6 mpoex 
 |-  ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) e. _V
25 24 a1i 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) e. _V )
26 coexg 
 |-  ( ( M e. V /\ ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) e. _V ) -> ( M o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) e. _V )
27 23 25 26 syl2anc 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> ( M o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) e. _V )
28 9 20 21 22 27 ovmpod 
 |-  ( ( K e. NN /\ L e. NN /\ M e. V ) -> ( K ( subMat1 ` M ) L ) = ( M o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )