Metamath Proof Explorer

Theorem smatlem

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

Ref Expression
Hypotheses smat.s ⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
smat.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
smat.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
smat.k ⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑀 ) )
smat.l ⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
smat.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
smatlem.i ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
smatlem.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
smatlem.1 ⊢ ( 𝜑 → if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) = 𝑋 )
smatlem.2 ⊢ ( 𝜑 → if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) = 𝑌 )
Assertion smatlem ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝑋 𝐴 𝑌 ) )

Proof

Step Hyp Ref Expression
1 smat.s ⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
2 smat.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 smat.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 smat.k ⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑀 ) )
5 smat.l ⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
6 smat.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
7 smatlem.i ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
8 smatlem.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
9 smatlem.1 ⊢ ( 𝜑 → if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) = 𝑋 )
10 smatlem.2 ⊢ ( 𝜑 → if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) = 𝑌 )
11 fz1ssnn ⊢ ( 1 ... 𝑀 ) ⊆ ℕ
12 11 4 sselid ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
13 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
14 13 5 sselid ⊢ ( 𝜑 → 𝐿 ∈ ℕ )
15 smatfval ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝐴 ∈ ( 𝐵 ↑m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) ) → ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 ) = ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )
16 12 14 6 15 syl3anc ⊢ ( 𝜑 → ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 ) = ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )
17 1 16 syl5eq ⊢ ( 𝜑 → 𝑆 = ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )
18 17 oveqd ⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝐼 ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) 𝐽 ) )
19 df-ov ⊢ ( 𝐼 ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) 𝐽 ) = ( ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ‘ ⟨ 𝐼 , 𝐽 ⟩ )
20 18 19 eqtrdi ⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) )
21 7 8 jca ⊢ ( 𝜑 → ( 𝐼 ∈ ℕ ∧ 𝐽 ∈ ℕ ) )
22 opelxp ⊢ ( ⟨ 𝐼 , 𝐽 ⟩ ∈ ( ℕ × ℕ ) ↔ ( 𝐼 ∈ ℕ ∧ 𝐽 ∈ ℕ ) )
23 21 22 sylibr ⊢ ( 𝜑 → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( ℕ × ℕ ) )
24 eqid ⊢ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) = ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ )
25 opex ⊢ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ∈ V
26 24 25 dmmpo ⊢ dom ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) = ( ℕ × ℕ )
27 23 26 eleqtrrdi ⊢ ( 𝜑 → ⟨ 𝐼 , 𝐽 ⟩ ∈ dom ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) )
28 24 mpofun ⊢ Fun ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ )
29 fvco ⊢ ( ( Fun ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ∧ ⟨ 𝐼 , 𝐽 ⟩ ∈ dom ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) → ( ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐴 ‘ ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) ) )
30 28 29 mpan ⊢ ( ⟨ 𝐼 , 𝐽 ⟩ ∈ dom ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) → ( ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐴 ‘ ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) ) )
31 27 30 syl ⊢ ( 𝜑 → ( ( 𝐴 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ( 𝐴 ‘ ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) ) )
32 20 31 eqtrd ⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝐴 ‘ ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) ) )
33 df-ov ⊢ ( 𝐼 ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) 𝐽 ) = ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ )
34 breq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 < 𝐾 ↔ 𝐼 < 𝐾 ) )
35 id ⊢ ( 𝑖 = 𝐼 → 𝑖 = 𝐼 )
36 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 + 1 ) = ( 𝐼 + 1 ) )
37 34 35 36 ifbieq12d ⊢ ( 𝑖 = 𝐼 → if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) )
38 37 opeq1d ⊢ ( 𝑖 = 𝐼 → ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ = ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ )
39 breq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 < 𝐿 ↔ 𝐽 < 𝐿 ) )
40 id ⊢ ( 𝑗 = 𝐽 → 𝑗 = 𝐽 )
41 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 + 1 ) = ( 𝐽 + 1 ) )
42 39 40 41 ifbieq12d ⊢ ( 𝑗 = 𝐽 → if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) = if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) )
43 42 opeq2d ⊢ ( 𝑗 = 𝐽 → ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ = ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) ⟩ )
44 opex ⊢ ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) ⟩ ∈ V
45 38 43 24 44 ovmpo ⊢ ( ( 𝐼 ∈ ℕ ∧ 𝐽 ∈ ℕ ) → ( 𝐼 ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) 𝐽 ) = ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) ⟩ )
46 21 45 syl ⊢ ( 𝜑 → ( 𝐼 ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) 𝐽 ) = ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) ⟩ )
47 9 10 opeq12d ⊢ ( 𝜑 → ⟨ if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) , if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
48 46 47 eqtrd ⊢ ( 𝜑 → ( 𝐼 ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) 𝐽 ) = ⟨ 𝑋 , 𝑌 ⟩ )
49 33 48 eqtr3id ⊢ ( 𝜑 → ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ⟨ 𝑋 , 𝑌 ⟩ )
50 49 fveq2d ⊢ ( 𝜑 → ( 𝐴 ‘ ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) ) = ( 𝐴 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
51 df-ov ⊢ ( 𝑋 𝐴 𝑌 ) = ( 𝐴 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
52 50 51 eqtr4di ⊢ ( 𝜑 → ( 𝐴 ‘ ( ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ‘ ⟨ 𝐼 , 𝐽 ⟩ ) ) = ( 𝑋 𝐴 𝑌 ) )
53 32 52 eqtrd ⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝑋 𝐴 𝑌 ) )