mp2pm2mplem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mp2pm2mplem4		Structured version Visualization version GIF version

Theorem mp2pm2mplem4 22752

Description: Lemma 4 for mp2pm2mp 22754. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.)

**Hypotheses**
Ref	Expression
mp2pm2mp.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mp2pm2mp.q	⊢ 𝑄 = (Poly₁‘𝐴)
mp2pm2mp.l	⊢ 𝐿 = (Base‘𝑄)
mp2pm2mp.m	⊢ · = ( ·_𝑠 ‘𝑃)
mp2pm2mp.e	⊢ 𝐸 = (._g‘(mulGrp‘𝑃))
mp2pm2mp.y	⊢ 𝑌 = (var₁‘𝑅)
mp2pm2mp.i	⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
mp2pm2mplem2.p	⊢ 𝑃 = (Poly₁‘𝑅)

**Assertion**
Ref	Expression
mp2pm2mplem4	⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe₁‘𝑂)‘𝐾))

Distinct variable groups: 𝐸,𝑝 𝐿,𝑝 𝑖,𝑁,𝑗,𝑝 𝑖,𝑂,𝑗,𝑝,𝑘 𝑃,𝑝 𝑅,𝑝 𝑌,𝑝 · ,𝑝 𝑘,𝐿 𝑃,𝑖,𝑗,𝑘 𝑅,𝑘 · ,𝑘 𝑖,𝐸,𝑗 𝑖,𝐾,𝑗 𝑖,𝐿,𝑗 𝑘,𝑁 𝑅,𝑖,𝑗 𝑖,𝑌,𝑗 · ,𝑖,𝑗 𝐴,𝑖,𝑗,𝑘 𝑘,𝐸 𝑘,𝐾 𝑘,𝑌 Allowed substitution hints: 𝐴(𝑝) 𝑄(𝑖,𝑗,𝑘,𝑝) 𝐼(𝑖,𝑗,𝑘,𝑝) 𝐾(𝑝)

Proof of Theorem mp2pm2mplem4 Dummy variables 𝑎 𝑏 𝑠 𝑥 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	. . 3 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		mp2pm2mp.q	. . 3 ⊢ 𝑄 = (Poly₁‘𝐴)
3		mp2pm2mp.l	. . 3 ⊢ 𝐿 = (Base‘𝑄)
4		mp2pm2mp.m	. . 3 ⊢ · = ( ·_𝑠 ‘𝑃)
5		mp2pm2mp.e	. . 3 ⊢ 𝐸 = (._g‘(mulGrp‘𝑃))
6		mp2pm2mp.y	. . 3 ⊢ 𝑌 = (var₁‘𝑅)
7		mp2pm2mp.i	. . 3 ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
8		mp2pm2mplem2.p	. . 3 ⊢ 𝑃 = (Poly₁‘𝑅)
9	1, 2, 3, 4, 5, 6, 7, 8	mp2pm2mplem3 22751	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)))
10		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘𝑃)
11		eqid 2736	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
12	8	ply1ring 22188	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
13	12	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring)
14		ringcmn 20247	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ CMnd)
16	15	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑃 ∈ CMnd)
17	16	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ CMnd)
18		simpl2 1193	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑅 ∈ Ring)
19	18	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Ring)
20	19	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
21	20	adantr 480	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑅 ∈ Ring)
22		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
23		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘𝐴) = (Base‘𝐴)
24		simpl2 1193	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
25		simpl3 1194	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
26		simpl3 1194	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑂 ∈ 𝐿)
27	26	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑂 ∈ 𝐿)
28	27	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
29		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (coe₁‘𝑂) = (coe₁‘𝑂)
30	29, 3, 2, 23	coe1fvalcl 22153	. . . . . . . . . . . . 13 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
31	28, 30	sylan 580	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
32	1, 22, 23, 24, 25, 31	matecld 22369	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
33		simpr 484	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
34		eqid 2736	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 22214	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
36	21, 32, 33, 35	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
37	36	ralrimiva 3133	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
38		simp1lr 1238	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ₀)
39		oveq 7416	. . . . . . . . . . . . . . . . 17 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → (𝑖((coe₁‘𝑂)‘𝑥)𝑗) = (𝑖(0_g‘𝐴)𝑗))
40	39	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)))
41		3simpa 1148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
42	41	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
43		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
44	1, 43	mat0op 22362	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
45	42, 44	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
46		eqidd 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0_g‘𝑅) = (0_g‘𝑅))
47		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁)
48		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁)
49		fvexd 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝑅) ∈ V)
50	45, 46, 47, 48, 49	ovmpod 7564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
51	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
52	51	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0_g‘𝑅) · (𝑥𝐸𝑌)))
53	18	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 ∈ Ring)
54	8	ply1sca 22193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 = (Scalar‘𝑃))
56	55	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
57	56	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘𝑅) · (𝑥𝐸𝑌)) = ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)))
58	8	ply1lmod 22192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
59	58	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ LMod)
60	59	ad4antr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑃 ∈ LMod)
61		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62	8, 6, 34, 5, 10	ply1moncl 22213	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
63	53, 61, 62	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
64		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
65		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
66	10, 64, 4, 65, 11	lmod0vs 20857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
67	60, 63, 66	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
68	52, 57, 67	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
69	68	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
70	40, 69	sylan9eqr 2793	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) ∧ ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
71	70	exp31 419	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑠 < 𝑥 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
72	71	a2d 29	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
73	72	ralimdva 3153	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
74	73	impancom 451	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
75	74	3impib 1116	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
76		breq2 5128	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥))
77		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝑥))
78	77	oveqd 7427	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝑥)𝑗))
79		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌))
80	78, 79	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)))
81	80	eqeq1d 2738	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃) ↔ ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
82	76, 81	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
83	82	cbvralvw 3224	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ₀ (𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
84	75, 83	sylibr 234	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ (𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)))
85	10, 11, 17, 37, 38, 84	gsummptnn0fz 19972	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))
86	85	fveq2d 6885	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
87	86	fveq1d 6883	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))
88		simpllr 775	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝐾 ∈ ℕ₀)
89	88	3ad2ant1 1133	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ ℕ₀)
90	36	expcom 413	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ₀ → ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
91		elfznn0 13642	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ₀)
92	90, 91	syl11 33	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
93	92	ralrimiv 3132	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
94		fzfid 13996	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin)
95	8, 10, 20, 89, 93, 94	coe1fzgsumd 22247	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
96	87, 95	eqtrd 2771	. . . . 5 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
97	96	mpoeq3dva 7489	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))))
98	18	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
99	98	adantr 480	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
100		simpl2 1193	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑖 ∈ 𝑁)
101		simpl3 1194	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑗 ∈ 𝑁)
102	26	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
103	102, 91, 30	syl2an 596	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
104	1, 22, 23, 100, 101, 103	matecld 22369	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
105	91	adantl 481	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ₀)
106	43, 22, 8, 6, 4, 34, 5	coe1tm 22215	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
107	99, 104, 105, 106	syl3anc 1373	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
108		eqeq1 2740	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘))
109	108	ifbid 4529	. . . . . . . . . 10 ⊢ (𝑙 = 𝐾 → if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
110	109	adantl 481	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑙 = 𝐾) → if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
111		simpl1r 1226	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝐾 ∈ ℕ₀)
112		ovex 7443	. . . . . . . . . . 11 ⊢ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ V
113		fvex 6894	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) ∈ V
114	112, 113	ifex 4556	. . . . . . . . . 10 ⊢ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) ∈ V
115	114	a1i 11	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) ∈ V)
116	107, 110, 111, 115	fvmptd 6998	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
117	116	mpteq2dva 5219	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
118	117	oveq2d 7426	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))))
119	118	mpoeq3dva 7489	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
120	119	ad2antrr 726	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
121		breq2 5128	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾))
122		fveqeq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) ↔ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
123	121, 122	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))))
124	123	rspcva 3604	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
125	1, 43	mat0op 22362	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
126	125	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
127	126	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
128	127	ad3antlr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
129		elfz2nn0 13640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠))
130		nn0re 12515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
131	130	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑘 ∈ ℝ)
132		nn0re 12515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ ℕ₀ → 𝑠 ∈ ℝ)
133	132	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑠 ∈ ℝ)
134		nn0re 12515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℝ)
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝐾 ∈ ℝ)
136		lelttr 11330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
137	131, 133, 135, 136	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
138		animorr 980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))
139		df-ne 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘)
140	130	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → 𝑘 ∈ ℝ)
141		lttri2 11322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
142	134, 140, 141	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
143	142	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
144	139, 143	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (¬ 𝐾 = 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
145	138, 144	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → ¬ 𝐾 = 𝑘)
146	145	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → (𝑘 < 𝐾 → ¬ 𝐾 = 𝑘))
147	137, 146	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → ¬ 𝐾 = 𝑘))
148	147	exp4b 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ∈ ℕ₀ → (𝑘 ≤ 𝑠 → (𝑠 < 𝐾 → ¬ 𝐾 = 𝑘))))
149	148	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝑠 < 𝐾 → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
150	149	expimpd 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ ℕ₀ → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
151	150	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
152	151	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
153	152	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
154	129, 153	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
155	154	com13 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐾 ∈ ℕ₀ → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)))
156	155	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)))
157	156	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
158	157	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
159	158	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
160	159	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐾 = 𝑘)
161	160	iffalsed 4516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = (0_g‘𝑅))
162	161	mpteq2dva 5219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅)))
163	162	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))))
164		ringmnd 20208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
165	164	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd)
166		ovex 7443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑠) ∈ V
167	43	gsumz 18819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
168	165, 166, 167	sylancl 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
169	168	ad3antlr 731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
170	169	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
171	163, 170	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (0_g‘𝑅))
172	171	mpoeq3dva 7489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
173		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))
174	128, 172, 173	3eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
175	174	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) → (((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
176	175	expr 456	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ₀) → (𝑠 < 𝐾 → (((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))
177	176	a2d 29	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ₀) → ((𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))
178	177	exp31 419	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℕ₀ → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → ((𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
179	178	com14 96	. . . . . . . . . . . 12 ⊢ ((𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
180	124, 179	syl 17	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
181	180	ex 412	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))))
182	181	com25 99	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))))
183	182	pm2.43i 52	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ₀ → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
184	183	impcom 407	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))
185	184	imp31 417	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
186	185	com12 32	. . . . 5 ⊢ (𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
187	165	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Mnd)
188	187	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑅 ∈ Mnd)
189	188	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Mnd)
190		ovexd 7445	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V)
191		lenlt 11318	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
192	134, 132, 191	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
193		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ ℕ₀)
194		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ₀)
195		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠)
196		elfz2nn0 13640	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (0...𝑠) ↔ (𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑠))
197	193, 194, 195, 196	syl3anbrc 1344	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ (0...𝑠))
198	197	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 → 𝐾 ∈ (0...𝑠)))
199	192, 198	sylbird 260	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
200	199	ad4ant23 753	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
201	200	impcom 407	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝐾 ∈ (0...𝑠))
202	201	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ (0...𝑠))
203		eqcom 2743	. . . . . . . . . . 11 ⊢ (𝐾 = 𝑘 ↔ 𝑘 = 𝐾)
204		ifbi 4528	. . . . . . . . . . 11 ⊢ ((𝐾 = 𝑘 ↔ 𝑘 = 𝐾) → if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝑘 = 𝐾, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
205	203, 204	ax-mp 5	. . . . . . . . . 10 ⊢ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝑘 = 𝐾, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))
206	205	mpteq2i 5222	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐾, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
207		simpl2 1193	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
208		simpl3 1194	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
209	27	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑂 ∈ 𝐿)
210	209	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
211	210, 30	sylan 580	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
212	1, 22, 23, 207, 208, 211	matecld 22369	. . . . . . . . . . 11 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
213	91, 212	sylan2 593	. . . . . . . . . 10 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
214	213	ralrimiva 3133	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
215	43, 189, 190, 202, 206, 214	gsummpt1n0 19951	. . . . . . . 8 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))
216	215	mpoeq3dva 7489	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)))
217		csbov 7455	. . . . . . . . . . . . . . 15 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗)
218		csbfv 6931	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾)
219	218	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾))
220	219	oveqd 7427	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ₀ → (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
221	217, 220	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
222	221	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
223	222	mpoeq3dv 7491	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe₁‘𝑂)‘𝐾)𝑗)))
224		oveq12 7419	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
225	224	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
226		simprl 770	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁)
227		simprr 772	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁)
228		ovexd 7445	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe₁‘𝑂)‘𝐾)𝑏) ∈ V)
229	223, 225, 226, 227, 228	ovmpod 7564	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
230	229	ralrimivva 3188	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
231		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑁 ∈ Fin)
232	218	oveqi 7423	. . . . . . . . . . . . . 14 ⊢ (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
233	217, 232	eqtri 2759	. . . . . . . . . . . . 13 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
234		simp2 1137	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
235		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
236	29, 3, 2, 23	coe1fvalcl 22153	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
237	236	3ad2antl3 1188	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
238	237	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
239	1, 22, 23, 234, 235, 238	matecld 22369	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅))
240	233, 239	eqeltrid 2839	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
241	1, 22, 23, 231, 18, 240	matbas2d 22366	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴))
242	1, 23	eqmat 22367	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴) ∧ ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏)))
243	241, 237, 242	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏)))
244	230, 243	mpbird 257	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
245	244	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
246	245	adantl 481	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
247	216, 246	eqtrd 2771	. . . . . 6 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
248	247	ex 412	. . . . 5 ⊢ (¬ 𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
249	186, 248	pm2.61i 182	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
250	97, 120, 249	3eqtrd 2775	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
251		eqid 2736	. . . . . 6 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
252	29, 3, 2, 251	coe1sfi 22154	. . . . 5 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) finSupp (0_g‘𝐴))
253	26, 252	syl 17	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) finSupp (0_g‘𝐴))
254	29, 3, 2, 251, 23	coe1fsupp 22155	. . . . . 6 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)})
255		elrabi 3671	. . . . . 6 ⊢ ((coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)} → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
256	26, 254, 255	3syl 18	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
257		fvex 6894	. . . . 5 ⊢ (0_g‘𝐴) ∈ V
258		fsuppmapnn0ub 14018	. . . . 5 ⊢ (((coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀) ∧ (0_g‘𝐴) ∈ V) → ((coe₁‘𝑂) finSupp (0_g‘𝐴) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))))
259	256, 257, 258	sylancl 586	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂) finSupp (0_g‘𝐴) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))))
260	253, 259	mpd 15	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))
261	250, 260	r19.29a 3149	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
262	9, 261	eqtrd 2771	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe₁‘𝑂)‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3420 Vcvv 3464 ⦋csb 3879 ifcif 4505 class class class wbr 5124 ↦ cmpt 5206 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 ↑_m cmap 8845 Fincfn 8964 finSupp cfsupp 9378 ℝcr 11133 0cc0 11134 < clt 11274 ≤ cle 11275 ℕ₀cn0 12506 ...cfz 13529 Basecbs 17233 Scalarcsca 17279 ·_𝑠 cvsca 17280 0_gc0g 17458 Σ_g cgsu 17459 Mndcmnd 18717 ._gcmg 19055 CMndccmn 19766 mulGrpcmgp 20105 Ringcrg 20198 LModclmod 20822 var₁cv1 22116 Poly₁cpl1 22117 coe₁cco1 22118 Mat cmat 22350 decompPMat cdecpmat 22705

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-ot 4615 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-ofr 7677 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-sup 9459 df-oi 9529 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-fz 13530 df-fzo 13677 df-seq 14025 df-hash 14354 df-struct 17171 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-mulr 17290 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-hom 17300 df-cco 17301 df-0g 17460 df-gsum 17461 df-prds 17466 df-pws 17468 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-subg 19111 df-ghm 19201 df-cntz 19305 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-ring 20200 df-subrng 20511 df-subrg 20535 df-lmod 20824 df-lss 20894 df-sra 21136 df-rgmod 21137 df-dsmm 21697 df-frlm 21712 df-psr 21874 df-mvr 21875 df-mpl 21876 df-opsr 21878 df-psr1 22120 df-vr1 22121 df-ply1 22122 df-coe1 22123 df-mat 22351 df-decpmat 22706

This theorem is referenced by: mp2pm2mplem5 22753 mp2pm2mp 22754

W3C validator