Metamath Proof Explorer

Theorem smatlem

Description: Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Hypotheses smat.s 
|- S = ( K ( subMat1 ` A ) L )
smat.m 
|- ( ph -> M e. NN )
smat.n 
|- ( ph -> N e. NN )
smat.k 
|- ( ph -> K e. ( 1 ... M ) )
smat.l 
|- ( ph -> L e. ( 1 ... N ) )
smat.a 
|- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
smatlem.i 
|- ( ph -> I e. NN )
smatlem.j 
|- ( ph -> J e. NN )
smatlem.1 
|- ( ph -> if ( I < K , I , ( I + 1 ) ) = X )
smatlem.2 
|- ( ph -> if ( J < L , J , ( J + 1 ) ) = Y )
Assertion smatlem 
|- ( ph -> ( I S J ) = ( X A Y ) )

Proof

Step Hyp Ref Expression
1 smat.s 
 |-  S = ( K ( subMat1 ` A ) L )
2 smat.m 
 |-  ( ph -> M e. NN )
3 smat.n 
 |-  ( ph -> N e. NN )
4 smat.k 
 |-  ( ph -> K e. ( 1 ... M ) )
5 smat.l 
 |-  ( ph -> L e. ( 1 ... N ) )
6 smat.a 
 |-  ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
7 smatlem.i 
 |-  ( ph -> I e. NN )
8 smatlem.j 
 |-  ( ph -> J e. NN )
9 smatlem.1 
 |-  ( ph -> if ( I < K , I , ( I + 1 ) ) = X )
10 smatlem.2 
 |-  ( ph -> if ( J < L , J , ( J + 1 ) ) = Y )
11 fz1ssnn 
 |-  ( 1 ... M ) C_ NN
12 11 4 sselid 
 |-  ( ph -> K e. NN )
13 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
14 13 5 sselid 
 |-  ( ph -> L e. NN )
15 smatfval 
 |-  ( ( K e. NN /\ L e. NN /\ A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) ) -> ( K ( subMat1 ` A ) L ) = ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )
16 12 14 6 15 syl3anc 
 |-  ( ph -> ( K ( subMat1 ` A ) L ) = ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )
17 1 16 eqtrid 
 |-  ( ph -> S = ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )
18 17 oveqd 
 |-  ( ph -> ( I S J ) = ( I ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) J ) )
19 df-ov 
 |-  ( I ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) J ) = ( ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) ` <. I , J >. )
20 18 19 eqtrdi 
 |-  ( ph -> ( I S J ) = ( ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) ` <. I , J >. ) )
21 7 8 jca 
 |-  ( ph -> ( I e. NN /\ J e. NN ) )
22 opelxp 
 |-  ( <. I , J >. e. ( NN X. NN ) <-> ( I e. NN /\ J e. NN ) )
23 21 22 sylibr 
 |-  ( ph -> <. I , J >. e. ( NN X. NN ) )
24 eqid 
 |-  ( 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 ) ) >. )
25 opex 
 |-  <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. e. _V
26 24 25 dmmpo 
 |-  dom ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) = ( NN X. NN )
27 23 26 eleqtrrdi 
 |-  ( ph -> <. I , J >. e. dom ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) )
28 24 mpofun 
 |-  Fun ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. )
29 fvco 
 |-  ( ( Fun ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) /\ <. I , J >. e. dom ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) -> ( ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) ` <. I , J >. ) = ( A ` ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) ) )
30 28 29 mpan 
 |-  ( <. I , J >. e. dom ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) -> ( ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) ` <. I , J >. ) = ( A ` ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) ) )
31 27 30 syl 
 |-  ( ph -> ( ( A o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) ` <. I , J >. ) = ( A ` ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) ) )
32 20 31 eqtrd 
 |-  ( ph -> ( I S J ) = ( A ` ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) ) )
33 df-ov 
 |-  ( I ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) J ) = ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. )
34 breq1 
 |-  ( i = I -> ( i < K <-> I < K ) )
35 id 
 |-  ( i = I -> i = I )
36 oveq1 
 |-  ( i = I -> ( i + 1 ) = ( I + 1 ) )
37 34 35 36 ifbieq12d 
 |-  ( i = I -> if ( i < K , i , ( i + 1 ) ) = if ( I < K , I , ( I + 1 ) ) )
38 37 opeq1d 
 |-  ( i = I -> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. = <. if ( I < K , I , ( I + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. )
39 breq1 
 |-  ( j = J -> ( j < L <-> J < L ) )
40 id 
 |-  ( j = J -> j = J )
41 oveq1 
 |-  ( j = J -> ( j + 1 ) = ( J + 1 ) )
42 39 40 41 ifbieq12d 
 |-  ( j = J -> if ( j < L , j , ( j + 1 ) ) = if ( J < L , J , ( J + 1 ) ) )
43 42 opeq2d 
 |-  ( j = J -> <. if ( I < K , I , ( I + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. = <. if ( I < K , I , ( I + 1 ) ) , if ( J < L , J , ( J + 1 ) ) >. )
44 opex 
 |-  <. if ( I < K , I , ( I + 1 ) ) , if ( J < L , J , ( J + 1 ) ) >. e. _V
45 38 43 24 44 ovmpo 
 |-  ( ( I e. NN /\ J e. NN ) -> ( I ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) J ) = <. if ( I < K , I , ( I + 1 ) ) , if ( J < L , J , ( J + 1 ) ) >. )
46 21 45 syl 
 |-  ( ph -> ( I ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) J ) = <. if ( I < K , I , ( I + 1 ) ) , if ( J < L , J , ( J + 1 ) ) >. )
47 9 10 opeq12d 
 |-  ( ph -> <. if ( I < K , I , ( I + 1 ) ) , if ( J < L , J , ( J + 1 ) ) >. = <. X , Y >. )
48 46 47 eqtrd 
 |-  ( ph -> ( I ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) J ) = <. X , Y >. )
49 33 48 eqtr3id 
 |-  ( ph -> ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) = <. X , Y >. )
50 49 fveq2d 
 |-  ( ph -> ( A ` ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) ) = ( A ` <. X , Y >. ) )
51 df-ov 
 |-  ( X A Y ) = ( A ` <. X , Y >. )
52 50 51 eqtr4di 
 |-  ( ph -> ( A ` ( ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ` <. I , J >. ) ) = ( X A Y ) )
53 32 52 eqtrd 
 |-  ( ph -> ( I S J ) = ( X A Y ) )