Theorem smatfval

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

	Ref	Expression
Assertion	smatfval	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → ( 𝐾 ( subMat1 ‘ 𝑀 ) 𝐿 ) = ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
2	1	3ad2ant3	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → 𝑀 ∈ V )
3		coeq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) = ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )
4	3	mpoeq3dv	⊢ ( 𝑚 = 𝑀 → ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) = ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )
5		df-smat	⊢ subMat1 = ( 𝑚 ∈ V ↦ ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )
6		nnex	⊢ ℕ ∈ V
7	6 6	mpoex	⊢ ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) ∈ V
8	4 5 7	fvmpt	⊢ ( 𝑀 ∈ V → ( subMat1 ‘ 𝑀 ) = ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )
9	2 8	syl	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → ( subMat1 ‘ 𝑀 ) = ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )
10		breq2	⊢ ( 𝑘 = 𝐾 → ( 𝑖 < 𝑘 ↔ 𝑖 < 𝐾 ) )
11	10	ifbid	⊢ ( 𝑘 = 𝐾 → if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) )
12	11	opeq1d	⊢ ( 𝑘 = 𝐾 → ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ = ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ )
13	12	mpoeq3dv	⊢ ( 𝑘 = 𝐾 → ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) = ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) )
14		breq2	⊢ ( 𝑙 = 𝐿 → ( 𝑗 < 𝑙 ↔ 𝑗 < 𝐿 ) )
15	14	ifbid	⊢ ( 𝑙 = 𝐿 → if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) = if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) )
16	15	opeq2d	⊢ ( 𝑙 = 𝐿 → ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ = ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ )
17	16	mpoeq3dv	⊢ ( 𝑙 = 𝐿 → ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) = ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) )
18	13 17	sylan9eq	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) → ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) = ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) )
19	18	adantl	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) = ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) )
20	19	coeq2d	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) ∧ ( 𝑘 = 𝐾 ∧ 𝑙 = 𝐿 ) ) → ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) = ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )
21		simp1	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → 𝐾 ∈ ℕ )
22		simp2	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → 𝐿 ∈ ℕ )
23		simp3	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → 𝑀 ∈ 𝑉 )
24	6 6	mpoex	⊢ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ∈ V
25	24	a1i	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ∈ V )
26		coexg	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ∈ V ) → ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ∈ V )
27	23 25 26	syl2anc	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ∈ V )
28	9 20 21 22 27	ovmpod	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉 ) → ( 𝐾 ( subMat1 ‘ 𝑀 ) 𝐿 ) = ( 𝑀 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝐾 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝐿 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )