smatlem

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

	Ref	Expression
Hypotheses	smat.s	$⊢ S = K {subMat}_{1} (A) L$
	smat.m	$⊢ φ \to M \in ℕ$
	smat.n	$⊢ φ \to N \in ℕ$
	smat.k	$⊢ φ \to K \in (1 \dots M)$
	smat.l	$⊢ φ \to L \in (1 \dots N)$
	smat.a	$⊢ φ \to A \in (B^{((1 \dots M) \times (1 \dots N))})$
	smatlem.i	$⊢ φ \to I \in ℕ$
	smatlem.j	$⊢ φ \to J \in ℕ$
	smatlem.1	$⊢ φ \to if (I < K, I, I + 1) = X$
	smatlem.2	$⊢ φ \to if (J < L, J, J + 1) = Y$
Assertion	smatlem	$⊢ φ \to I S J = X A Y$

Proof

Step	Hyp	Ref	Expression
1		smat.s	$⊢ S = K {subMat}_{1} (A) L$
2		smat.m	$⊢ φ \to M \in ℕ$
3		smat.n	$⊢ φ \to N \in ℕ$
4		smat.k	$⊢ φ \to K \in (1 \dots M)$
5		smat.l	$⊢ φ \to L \in (1 \dots N)$
6		smat.a	$⊢ φ \to A \in (B^{((1 \dots M) \times (1 \dots N))})$
7		smatlem.i	$⊢ φ \to I \in ℕ$
8		smatlem.j	$⊢ φ \to J \in ℕ$
9		smatlem.1	$⊢ φ \to if (I < K, I, I + 1) = X$
10		smatlem.2	$⊢ φ \to if (J < L, J, J + 1) = Y$
11		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
12	11 4	sselid	$⊢ φ \to K \in ℕ$
13		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
14	13 5	sselid	$⊢ φ \to L \in ℕ$
15		smatfval	$⊢ (K \in ℕ \land L \in ℕ \land A \in (B^{((1 \dots M) \times (1 \dots N))})) \to K {subMat}_{1} (A) L = A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
16	12 14 6 15	syl3anc	$⊢ φ \to K {subMat}_{1} (A) L = A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
17	1 16	eqtrid	$⊢ φ \to S = A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
18	17	oveqd	$⊢ φ \to I S J = I (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) J$
19		df-ov	$⊢ I (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) J = (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) (⟨I, J⟩)$
20	18 19	eqtrdi	$⊢ φ \to I S J = (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) (⟨I, J⟩)$
21	7 8	jca	$⊢ φ \to (I \in ℕ \land J \in ℕ)$
22		opelxp	$⊢ ⟨I, J⟩ \in (ℕ \times ℕ) \leftrightarrow (I \in ℕ \land J \in ℕ)$
23	21 22	sylibr	$⊢ φ \to ⟨I, J⟩ \in (ℕ \times ℕ)$
24		eqid	$⊢ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) = (i \in ℕ, j \in ℕ ⟼ ⟨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)⟩ \in V$
26	24 25	dmmpo	$⊢ dom (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) = ℕ \times ℕ$
27	23 26	eleqtrrdi	$⊢ φ \to ⟨I, J⟩ \in dom (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
28	24	mpofun	$⊢ Fun (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)$
29		fvco	$⊢ (Fun (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) \land ⟨I, J⟩ \in dom (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) \to (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) (⟨I, J⟩) = A ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩))$
30	28 29	mpan	$⊢ ⟨I, J⟩ \in dom (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) \to (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) (⟨I, J⟩) = A ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩))$
31	27 30	syl	$⊢ φ \to (A \circ (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩)) (⟨I, J⟩) = A ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩))$
32	20 31	eqtrd	$⊢ φ \to I S J = A ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩))$
33		df-ov	$⊢ I (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) J = (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩)$
34		breq1	$⊢ i = I \to (i < K \leftrightarrow I < K)$
35		id	$⊢ i = I \to i = I$
36		oveq1	$⊢ i = I \to i + 1 = I + 1$
37	34 35 36	ifbieq12d	$⊢ i = I \to if (i < K, i, i + 1) = if (I < K, I, I + 1)$
38	37	opeq1d	$⊢ i = I \to ⟨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 \to (j < L \leftrightarrow J < L)$
40		id	$⊢ j = J \to j = J$
41		oveq1	$⊢ j = J \to j + 1 = J + 1$
42	39 40 41	ifbieq12d	$⊢ j = J \to if (j < L, j, j + 1) = if (J < L, J, J + 1)$
43	42	opeq2d	$⊢ j = J \to ⟨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)⟩ \in V$
45	38 43 24 44	ovmpo	$⊢ (I \in ℕ \land J \in ℕ) \to I (i \in ℕ, j \in ℕ ⟼ ⟨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	$⊢ φ \to I (i \in ℕ, j \in ℕ ⟼ ⟨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	$⊢ φ \to ⟨if (I < K, I, I + 1), if (J < L, J, J + 1)⟩ = ⟨X, Y⟩$
48	46 47	eqtrd	$⊢ φ \to I (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) J = ⟨X, Y⟩$
49	33 48	eqtr3id	$⊢ φ \to (i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩) = ⟨X, Y⟩$
50	49	fveq2d	$⊢ φ \to A ((i \in ℕ, j \in ℕ ⟼ ⟨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	$⊢ φ \to A ((i \in ℕ, j \in ℕ ⟼ ⟨if (i < K, i, i + 1), if (j < L, j, j + 1)⟩) (⟨I, J⟩)) = X A Y$
53	32 52	eqtrd	$⊢ φ \to I S J = X A Y$

Metamath Proof Explorer

Theorem smatlem

Proof