Metamath Proof Explorer

Theorem lmatfvlem

Description: Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020)

Ref Expression
Hypotheses lmatfval.m 
|- M = ( litMat ` W )
lmatfval.n 
|- ( ph -> N e. NN )
lmatfval.w 
|- ( ph -> W e. Word Word V )
lmatfval.1 
|- ( ph -> ( # ` W ) = N )
lmatfval.2 
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( # ` ( W ` i ) ) = N )
lmatfvlem.1 
|- K e. NN0
lmatfvlem.2 
|- L e. NN0
lmatfvlem.3 
|- I <_ N
lmatfvlem.4 
|- J <_ N
lmatfvlem.5 
|- ( K + 1 ) = I
lmatfvlem.6 
|- ( L + 1 ) = J
lmatfvlem.7 
|- ( W ` K ) = X
lmatfvlem.8 
|- ( ph -> ( X ` L ) = Y )
Assertion lmatfvlem 
|- ( ph -> ( I M J ) = Y )

Proof

Step Hyp Ref Expression
1 lmatfval.m 
 |-  M = ( litMat ` W )
2 lmatfval.n 
 |-  ( ph -> N e. NN )
3 lmatfval.w 
 |-  ( ph -> W e. Word Word V )
4 lmatfval.1 
 |-  ( ph -> ( # ` W ) = N )
5 lmatfval.2 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( # ` ( W ` i ) ) = N )
6 lmatfvlem.1 
 |-  K e. NN0
7 lmatfvlem.2 
 |-  L e. NN0
8 lmatfvlem.3 
 |-  I <_ N
9 lmatfvlem.4 
 |-  J <_ N
10 lmatfvlem.5 
 |-  ( K + 1 ) = I
11 lmatfvlem.6 
 |-  ( L + 1 ) = J
12 lmatfvlem.7 
 |-  ( W ` K ) = X
13 lmatfvlem.8 
 |-  ( ph -> ( X ` L ) = Y )
14 nn0p1nn 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN )
15 6 14 ax-mp 
 |-  ( K + 1 ) e. NN
16 10 15 eqeltrri 
 |-  I e. NN
17 nnge1 
 |-  ( I e. NN -> 1 <_ I )
18 16 17 ax-mp 
 |-  1 <_ I
19 18 8 pm3.2i 
 |-  ( 1 <_ I /\ I <_ N )
20 19 a1i 
 |-  ( ph -> ( 1 <_ I /\ I <_ N ) )
21 nnz 
 |-  ( I e. NN -> I e. ZZ )
22 16 21 ax-mp 
 |-  I e. ZZ
23 22 a1i 
 |-  ( ph -> I e. ZZ )
24 1z 
 |-  1 e. ZZ
25 24 a1i 
 |-  ( ph -> 1 e. ZZ )
26 2 nnzd 
 |-  ( ph -> N e. ZZ )
27 elfz 
 |-  ( ( I e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( I e. ( 1 ... N ) <-> ( 1 <_ I /\ I <_ N ) ) )
28 23 25 26 27 syl3anc 
 |-  ( ph -> ( I e. ( 1 ... N ) <-> ( 1 <_ I /\ I <_ N ) ) )
29 20 28 mpbird 
 |-  ( ph -> I e. ( 1 ... N ) )
30 nn0p1nn 
 |-  ( L e. NN0 -> ( L + 1 ) e. NN )
31 7 30 ax-mp 
 |-  ( L + 1 ) e. NN
32 11 31 eqeltrri 
 |-  J e. NN
33 nnge1 
 |-  ( J e. NN -> 1 <_ J )
34 32 33 ax-mp 
 |-  1 <_ J
35 34 9 pm3.2i 
 |-  ( 1 <_ J /\ J <_ N )
36 35 a1i 
 |-  ( ph -> ( 1 <_ J /\ J <_ N ) )
37 nnz 
 |-  ( J e. NN -> J e. ZZ )
38 32 37 ax-mp 
 |-  J e. ZZ
39 38 a1i 
 |-  ( ph -> J e. ZZ )
40 elfz 
 |-  ( ( J e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( J e. ( 1 ... N ) <-> ( 1 <_ J /\ J <_ N ) ) )
41 39 25 26 40 syl3anc 
 |-  ( ph -> ( J e. ( 1 ... N ) <-> ( 1 <_ J /\ J <_ N ) ) )
42 36 41 mpbird 
 |-  ( ph -> J e. ( 1 ... N ) )
43 1 2 3 4 5 29 42 lmatfval 
 |-  ( ph -> ( I M J ) = ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) )
44 6 nn0cni 
 |-  K e. CC
45 ax-1cn 
 |-  1 e. CC
46 44 45 pncan3oi 
 |-  ( ( K + 1 ) - 1 ) = K
47 10 oveq1i 
 |-  ( ( K + 1 ) - 1 ) = ( I - 1 )
48 46 47 eqtr3i 
 |-  K = ( I - 1 )
49 48 fveq2i 
 |-  ( W ` K ) = ( W ` ( I - 1 ) )
50 49 12 eqtr3i 
 |-  ( W ` ( I - 1 ) ) = X
51 50 a1i 
 |-  ( ph -> ( W ` ( I - 1 ) ) = X )
52 51 fveq1d 
 |-  ( ph -> ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) = ( X ` ( J - 1 ) ) )
53 7 nn0cni 
 |-  L e. CC
54 53 45 pncan3oi 
 |-  ( ( L + 1 ) - 1 ) = L
55 11 oveq1i 
 |-  ( ( L + 1 ) - 1 ) = ( J - 1 )
56 54 55 eqtr3i 
 |-  L = ( J - 1 )
57 56 a1i 
 |-  ( ph -> L = ( J - 1 ) )
58 57 fveq2d 
 |-  ( ph -> ( X ` L ) = ( X ` ( J - 1 ) ) )
59 58 13 eqtr3d 
 |-  ( ph -> ( X ` ( J - 1 ) ) = Y )
60 43 52 59 3eqtrd 
 |-  ( ph -> ( I M J ) = Y )