submateq - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > submateq		Structured version Visualization version GIF version

Theorem submateq 29203

Description: Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.)

**Hypotheses**
Ref	Expression
submateq.a	⊢ 𝐴 = ((1...𝑁) Mat 𝑅)
submateq.b	⊢ 𝐵 = (Base‘𝐴)
submateq.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
submateq.i	⊢ (𝜑 → 𝐼 ∈ (1...𝑁))
submateq.j	⊢ (𝜑 → 𝐽 ∈ (1...𝑁))
submateq.e	⊢ (𝜑 → 𝐸 ∈ 𝐵)
submateq.f	⊢ (𝜑 → 𝐹 ∈ 𝐵)
submateq.1	⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗))

**Assertion**
Ref	Expression
submateq	⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽))

Distinct variable groups: 𝑖,𝐸,𝑗 𝑖,𝐹,𝑗 𝑖,𝐼,𝑗 𝑖,𝐽,𝑗 𝑖,𝑁,𝑗 𝜑,𝑖,𝑗 Allowed substitution hints: 𝐴(𝑖,𝑗) 𝐵(𝑖,𝑗) 𝑅(𝑖,𝑗)

Proof of Theorem submateq Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝑥 ∈ (1...(𝑁 − 1)))
2		submateq.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → 𝑁 ∈ ℕ)
4		submateq.i	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))
5	4	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → 𝐼 ∈ (1...𝑁))
6		simplr 788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → 𝑥 ∈ (1...(𝑁 − 1)))
7		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → 𝐼 ≤ 𝑥)
8	3, 5, 6, 7	submateqlem1 29201	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → (𝑥 ∈ (𝐼...𝑁) ∧ (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼})))
9	8	simprd 478	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}))
10	1, 9	syldanl 731	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) → (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}))
11	10	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}))
12		simprr 792	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝑦 ∈ (1...(𝑁 − 1)))
13	2	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → 𝑁 ∈ ℕ)
14		submateq.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))
15	14	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → 𝐽 ∈ (1...𝑁))
16		simplr 788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → 𝑦 ∈ (1...(𝑁 − 1)))
17		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → 𝐽 ≤ 𝑦)
18	13, 15, 16, 17	submateqlem1 29201	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → (𝑦 ∈ (𝐽...𝑁) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})))
19	18	simprd 478	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽}))
20	12, 19	syldanl 731	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐽 ≤ 𝑦) → (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽}))
21	20	adantlr 747	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽}))
22	11, 21	jca 553	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → ((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})))
23		ovex 6577	. . . . . . . . . 10 ⊢ (𝑥 + 1) ∈ V
24	23	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 + 1) ∈ V)
25		ovex 6577	. . . . . . . . . 10 ⊢ (𝑦 + 1) ∈ V
26	25	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 + 1) ∈ V)
27		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → 𝑖 = (𝑥 + 1))
28	27	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → (𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ↔ (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼})))
29		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → 𝑗 = (𝑦 + 1))
30	29	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → (𝑗 ∈ ((1...𝑁) ∖ {𝐽}) ↔ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})))
31	28, 30	anbi12d 743	. . . . . . . . . 10 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → ((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) ↔ ((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽}))))
32		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → (𝑖𝐸𝑗) = ((𝑥 + 1)𝐸(𝑦 + 1)))
33		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → (𝑖𝐹𝑗) = ((𝑥 + 1)𝐹(𝑦 + 1)))
34	32, 33	eqeq12d 2625	. . . . . . . . . 10 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → ((𝑖𝐸𝑗) = (𝑖𝐹𝑗) ↔ ((𝑥 + 1)𝐸(𝑦 + 1)) = ((𝑥 + 1)𝐹(𝑦 + 1))))
35	31, 34	imbi12d 333	. . . . . . . . 9 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = (𝑦 + 1)) → (((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)) ↔ (((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})) → ((𝑥 + 1)𝐸(𝑦 + 1)) = ((𝑥 + 1)𝐹(𝑦 + 1)))))
36		submateq.1	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗))
37	36	3expib 1260	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)))
38	24, 26, 35, 37	vtocl2d 28699	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})) → ((𝑥 + 1)𝐸(𝑦 + 1)) = ((𝑥 + 1)𝐹(𝑦 + 1))))
39	38	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → (((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})) → ((𝑥 + 1)𝐸(𝑦 + 1)) = ((𝑥 + 1)𝐹(𝑦 + 1))))
40	22, 39	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → ((𝑥 + 1)𝐸(𝑦 + 1)) = ((𝑥 + 1)𝐹(𝑦 + 1)))
41		eqid 2610	. . . . . . 7 ⊢ (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐸)𝐽)
42	2	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝑁 ∈ ℕ)
43	4	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝐼 ∈ (1...𝑁))
44	14	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝐽 ∈ (1...𝑁))
45		submateq.e	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ 𝐵)
46		submateq.a	. . . . . . . . . 10 ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)
47		eqid 2610	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
48		submateq.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐴)
49	46, 47, 48	matbas2i 20047	. . . . . . . . 9 ⊢ (𝐸 ∈ 𝐵 → 𝐸 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
50	45, 49	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
51	50	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝐸 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
52	8	simpld 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≤ 𝑥) → 𝑥 ∈ (𝐼...𝑁))
53	1, 52	syldanl 731	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) → 𝑥 ∈ (𝐼...𝑁))
54	53	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝑥 ∈ (𝐼...𝑁))
55	18	simpld 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝐽 ≤ 𝑦) → 𝑦 ∈ (𝐽...𝑁))
56	12, 55	syldanl 731	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐽 ≤ 𝑦) → 𝑦 ∈ (𝐽...𝑁))
57	56	adantlr 747	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝑦 ∈ (𝐽...𝑁))
58	41, 42, 42, 43, 44, 51, 54, 57	smatbr 29195	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = ((𝑥 + 1)𝐸(𝑦 + 1)))
59		eqid 2610	. . . . . . 7 ⊢ (𝐼(subMat1‘𝐹)𝐽) = (𝐼(subMat1‘𝐹)𝐽)
60		submateq.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
61	46, 47, 48	matbas2i 20047	. . . . . . . . 9 ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
62	60, 61	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
63	62	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → 𝐹 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
64	59, 42, 42, 43, 44, 63, 54, 57	smatbr 29195	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦) = ((𝑥 + 1)𝐹(𝑦 + 1)))
65	40, 58, 64	3eqtr4d 2654	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝐽 ≤ 𝑦) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
66	10	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}))
67	2	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → 𝑁 ∈ ℕ)
68	14	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → 𝐽 ∈ (1...𝑁))
69		simplr 788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → 𝑦 ∈ (1...(𝑁 − 1)))
70		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → 𝑦 < 𝐽)
71	67, 68, 69, 70	submateqlem2 29202	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → (𝑦 ∈ (1..^𝐽) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})))
72	71	simprd 478	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → 𝑦 ∈ ((1...𝑁) ∖ {𝐽}))
73	12, 72	syldanl 731	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑦 < 𝐽) → 𝑦 ∈ ((1...𝑁) ∖ {𝐽}))
74	73	adantlr 747	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝑦 ∈ ((1...𝑁) ∖ {𝐽}))
75	66, 74	jca 553	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → ((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})))
76		vex 3176	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
77	76	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑦 ∈ V)
78		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → 𝑖 = (𝑥 + 1))
79	78	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → (𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ↔ (𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼})))
80		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → 𝑗 = 𝑦)
81		eqidd 2611	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → ((1...𝑁) ∖ {𝐽}) = ((1...𝑁) ∖ {𝐽}))
82	80, 81	eleq12d 2682	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → (𝑗 ∈ ((1...𝑁) ∖ {𝐽}) ↔ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})))
83	79, 82	anbi12d 743	. . . . . . . . . 10 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → ((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) ↔ ((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽}))))
84		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → (𝑖𝐸𝑗) = ((𝑥 + 1)𝐸𝑦))
85		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → (𝑖𝐹𝑗) = ((𝑥 + 1)𝐹𝑦))
86	84, 85	eqeq12d 2625	. . . . . . . . . 10 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → ((𝑖𝐸𝑗) = (𝑖𝐹𝑗) ↔ ((𝑥 + 1)𝐸𝑦) = ((𝑥 + 1)𝐹𝑦)))
87	83, 86	imbi12d 333	. . . . . . . . 9 ⊢ ((𝑖 = (𝑥 + 1) ∧ 𝑗 = 𝑦) → (((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)) ↔ (((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})) → ((𝑥 + 1)𝐸𝑦) = ((𝑥 + 1)𝐹𝑦))))
88	24, 77, 87, 37	vtocl2d 28699	. . . . . . . 8 ⊢ (𝜑 → (((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})) → ((𝑥 + 1)𝐸𝑦) = ((𝑥 + 1)𝐹𝑦)))
89	88	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → (((𝑥 + 1) ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})) → ((𝑥 + 1)𝐸𝑦) = ((𝑥 + 1)𝐹𝑦)))
90	75, 89	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → ((𝑥 + 1)𝐸𝑦) = ((𝑥 + 1)𝐹𝑦))
91	2	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝑁 ∈ ℕ)
92	4	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝐼 ∈ (1...𝑁))
93	14	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝐽 ∈ (1...𝑁))
94	50	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝐸 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
95	53	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝑥 ∈ (𝐼...𝑁))
96	71	simpld 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) ∧ 𝑦 < 𝐽) → 𝑦 ∈ (1..^𝐽))
97	12, 96	syldanl 731	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑦 < 𝐽) → 𝑦 ∈ (1..^𝐽))
98	97	adantlr 747	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝑦 ∈ (1..^𝐽))
99	41, 91, 91, 92, 93, 94, 95, 98	smattr 29193	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = ((𝑥 + 1)𝐸𝑦))
100	62	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → 𝐹 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
101	59, 91, 91, 92, 93, 100, 95, 98	smattr 29193	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦) = ((𝑥 + 1)𝐹𝑦))
102	90, 99, 101	3eqtr4d 2654	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) ∧ 𝑦 < 𝐽) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
103		fz1ssnn 12243	. . . . . . . . . 10 ⊢ (1...𝑁) ⊆ ℕ
104	103, 14	sseldi 3566	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℕ)
105	104	nnred 10912	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ ℝ)
106	105	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝐽 ∈ ℝ)
107		fz1ssnn 12243	. . . . . . . . 9 ⊢ (1...(𝑁 − 1)) ⊆ ℕ
108	107, 12	sseldi 3566	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝑦 ∈ ℕ)
109	108	nnred 10912	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝑦 ∈ ℝ)
110		lelttric 10023	. . . . . . 7 ⊢ ((𝐽 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐽 ≤ 𝑦 ∨ 𝑦 < 𝐽))
111	106, 109, 110	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → (𝐽 ≤ 𝑦 ∨ 𝑦 < 𝐽))
112	111	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) → (𝐽 ≤ 𝑦 ∨ 𝑦 < 𝐽))
113	65, 102, 112	mpjaodan 823	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝐼 ≤ 𝑥) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
114	2	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → 𝑁 ∈ ℕ)
115	4	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → 𝐼 ∈ (1...𝑁))
116		simplr 788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → 𝑥 ∈ (1...(𝑁 − 1)))
117		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → 𝑥 < 𝐼)
118	114, 115, 116, 117	submateqlem2 29202	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → (𝑥 ∈ (1..^𝐼) ∧ 𝑥 ∈ ((1...𝑁) ∖ {𝐼})))
119	118	simprd 478	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → 𝑥 ∈ ((1...𝑁) ∖ {𝐼}))
120	1, 119	syldanl 731	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) → 𝑥 ∈ ((1...𝑁) ∖ {𝐼}))
121	120	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝑥 ∈ ((1...𝑁) ∖ {𝐼}))
122	20	adantlr 747	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽}))
123	121, 122	jca 553	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → (𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})))
124		vex 3176	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
125	124	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑥 ∈ V)
126		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → 𝑖 = 𝑥)
127	126	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → (𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ↔ 𝑥 ∈ ((1...𝑁) ∖ {𝐼})))
128		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → 𝑗 = (𝑦 + 1))
129	128	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → (𝑗 ∈ ((1...𝑁) ∖ {𝐽}) ↔ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})))
130	127, 129	anbi12d 743	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → ((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) ↔ (𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽}))))
131		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → (𝑖𝐸𝑗) = (𝑥𝐸(𝑦 + 1)))
132		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → (𝑖𝐹𝑗) = (𝑥𝐹(𝑦 + 1)))
133	131, 132	eqeq12d 2625	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → ((𝑖𝐸𝑗) = (𝑖𝐹𝑗) ↔ (𝑥𝐸(𝑦 + 1)) = (𝑥𝐹(𝑦 + 1))))
134	130, 133	imbi12d 333	. . . . . . . . 9 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = (𝑦 + 1)) → (((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)) ↔ ((𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})) → (𝑥𝐸(𝑦 + 1)) = (𝑥𝐹(𝑦 + 1)))))
135	125, 26, 134, 37	vtocl2d 28699	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})) → (𝑥𝐸(𝑦 + 1)) = (𝑥𝐹(𝑦 + 1))))
136	135	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → ((𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ (𝑦 + 1) ∈ ((1...𝑁) ∖ {𝐽})) → (𝑥𝐸(𝑦 + 1)) = (𝑥𝐹(𝑦 + 1))))
137	123, 136	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → (𝑥𝐸(𝑦 + 1)) = (𝑥𝐹(𝑦 + 1)))
138	2	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝑁 ∈ ℕ)
139	4	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝐼 ∈ (1...𝑁))
140	14	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝐽 ∈ (1...𝑁))
141	50	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝐸 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
142	118	simpld 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...(𝑁 − 1))) ∧ 𝑥 < 𝐼) → 𝑥 ∈ (1..^𝐼))
143	1, 142	syldanl 731	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) → 𝑥 ∈ (1..^𝐼))
144	143	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝑥 ∈ (1..^𝐼))
145	56	adantlr 747	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝑦 ∈ (𝐽...𝑁))
146	41, 138, 138, 139, 140, 141, 144, 145	smatbl 29194	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥𝐸(𝑦 + 1)))
147	62	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → 𝐹 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
148	59, 138, 138, 139, 140, 147, 144, 145	smatbl 29194	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦) = (𝑥𝐹(𝑦 + 1)))
149	137, 146, 148	3eqtr4d 2654	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝐽 ≤ 𝑦) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
150	120	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝑥 ∈ ((1...𝑁) ∖ {𝐼}))
151	73	adantlr 747	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝑦 ∈ ((1...𝑁) ∖ {𝐽}))
152	150, 151	jca 553	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → (𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})))
153		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → 𝑖 = 𝑥)
154	153	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ↔ 𝑥 ∈ ((1...𝑁) ∖ {𝐼})))
155		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → 𝑗 = 𝑦)
156	155	eleq1d 2672	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑗 ∈ ((1...𝑁) ∖ {𝐽}) ↔ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})))
157	154, 156	anbi12d 743	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → ((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) ↔ (𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽}))))
158		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑖𝐸𝑗) = (𝑥𝐸𝑦))
159		oveq12 6558	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑖𝐹𝑗) = (𝑥𝐹𝑦))
160	158, 159	eqeq12d 2625	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → ((𝑖𝐸𝑗) = (𝑖𝐹𝑗) ↔ (𝑥𝐸𝑦) = (𝑥𝐹𝑦)))
161	157, 160	imbi12d 333	. . . . . . . . 9 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (((𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)) ↔ ((𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑥𝐸𝑦) = (𝑥𝐹𝑦))))
162	125, 77, 161, 37	vtocl2d 28699	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑥𝐸𝑦) = (𝑥𝐹𝑦)))
163	162	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → ((𝑥 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑦 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑥𝐸𝑦) = (𝑥𝐹𝑦)))
164	152, 163	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → (𝑥𝐸𝑦) = (𝑥𝐹𝑦))
165	2	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝑁 ∈ ℕ)
166	4	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝐼 ∈ (1...𝑁))
167	14	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝐽 ∈ (1...𝑁))
168	50	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝐸 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
169	143	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝑥 ∈ (1..^𝐼))
170	97	adantlr 747	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝑦 ∈ (1..^𝐽))
171	41, 165, 165, 166, 167, 168, 169, 170	smattl 29192	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥𝐸𝑦))
172	62	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → 𝐹 ∈ ((Base‘𝑅) ↑_𝑚 ((1...𝑁) × (1...𝑁))))
173	59, 165, 165, 166, 167, 172, 169, 170	smattl 29192	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦) = (𝑥𝐹𝑦))
174	164, 171, 173	3eqtr4d 2654	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) ∧ 𝑦 < 𝐽) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
175	111	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) → (𝐽 ≤ 𝑦 ∨ 𝑦 < 𝐽))
176	149, 174, 175	mpjaodan 823	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) ∧ 𝑥 < 𝐼) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
177	103, 4	sseldi 3566	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ ℕ)
178	177	nnred 10912	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℝ)
179	178	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝐼 ∈ ℝ)
180	107, 1	sseldi 3566	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝑥 ∈ ℕ)
181	180	nnred 10912	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → 𝑥 ∈ ℝ)
182		lelttric 10023	. . . . 5 ⊢ ((𝐼 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐼 ≤ 𝑥 ∨ 𝑥 < 𝐼))
183	179, 181, 182	syl2anc 691	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → (𝐼 ≤ 𝑥 ∨ 𝑥 < 𝐼))
184	113, 176, 183	mpjaodan 823	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝑁 − 1)) ∧ 𝑦 ∈ (1...(𝑁 − 1)))) → (𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
185	184	ralrimivva 2954	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (1...(𝑁 − 1))∀𝑦 ∈ (1...(𝑁 − 1))(𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦))
186		eqid 2610	. . . 4 ⊢ (Base‘((1...(𝑁 − 1)) Mat 𝑅)) = (Base‘((1...(𝑁 − 1)) Mat 𝑅))
187	46, 48, 186, 41, 2, 4, 14, 45	smatcl 29196	. . 3 ⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
188	46, 48, 186, 59, 2, 4, 14, 60	smatcl 29196	. . 3 ⊢ (𝜑 → (𝐼(subMat1‘𝐹)𝐽) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
189		eqid 2610	. . . 4 ⊢ ((1...(𝑁 − 1)) Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅)
190	189, 186	eqmat 20049	. . 3 ⊢ (((𝐼(subMat1‘𝐸)𝐽) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)) ∧ (𝐼(subMat1‘𝐹)𝐽) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → ((𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽) ↔ ∀𝑥 ∈ (1...(𝑁 − 1))∀𝑦 ∈ (1...(𝑁 − 1))(𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦)))
191	187, 188, 190	syl2anc 691	. 2 ⊢ (𝜑 → ((𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽) ↔ ∀𝑥 ∈ (1...(𝑁 − 1))∀𝑦 ∈ (1...(𝑁 − 1))(𝑥(𝐼(subMat1‘𝐸)𝐽)𝑦) = (𝑥(𝐼(subMat1‘𝐹)𝐽)𝑦)))
192	185, 191	mpbird 246	1 ⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ∖ cdif 3537 {csn 4125 class class class wbr 4583 × cxp 5036 ‘cfv 5804 (class class class)co 6549 ↑_𝑚 cmap 7744 ℝcr 9814 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 ...cfz 12197 ..^cfzo 12334 Basecbs 15695 Mat cmat 20032 subMat1csmat 29187

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-ot 4134 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-fz 12198 df-fzo 12335 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-hom 15793 df-cco 15794 df-0g 15925 df-prds 15931 df-pws 15933 df-sra 18993 df-rgmod 18994 df-dsmm 19895 df-frlm 19910 df-mat 20033 df-smat 29188

This theorem is referenced by: submatminr1 29204

W3C validator