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 22696

Description: Lemma 4 for mp2pm2mp 22698. (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 22695	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)))
10		eqid 2729	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘𝑃)
11		eqid 2729	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
12	8	ply1ring 22132	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
13	12	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring)
14		ringcmn 20191	. . . . . . . . . . . 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 2729	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
23		eqid 2729	. . . . . . . . . . . 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 2729	. . . . . . . . . . . . . 14 ⊢ (coe₁‘𝑂) = (coe₁‘𝑂)
30	29, 3, 2, 23	coe1fvalcl 22097	. . . . . . . . . . . . 13 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
31	28, 30	sylan 580	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
32	1, 22, 23, 24, 25, 31	matecld 22313	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
33		simpr 484	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
34		eqid 2729	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 22158	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
36	21, 32, 33, 35	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
37	36	ralrimiva 3125	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
38		simp1lr 1238	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ₀)
39		oveq 7393	. . . . . . . . . . . . . . . . 17 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → (𝑖((coe₁‘𝑂)‘𝑥)𝑗) = (𝑖(0_g‘𝐴)𝑗))
40	39	oveq1d 7402	. . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
44	1, 43	mat0op 22306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
45	42, 44	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
46		eqidd 2730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0_g‘𝑅) = (0_g‘𝑅))
47		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁)
48		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁)
49		fvexd 6873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝑅) ∈ V)
50	45, 46, 47, 48, 49	ovmpod 7541	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
51	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
52	51	oveq1d 7402	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0_g‘𝑅) · (𝑥𝐸𝑌)))
53	18	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 ∈ Ring)
54	8	ply1sca 22137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 = (Scalar‘𝑃))
56	55	fveq2d 6862	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
57	56	oveq1d 7402	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘𝑅) · (𝑥𝐸𝑌)) = ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)))
58	8	ply1lmod 22136	. . . . . . . . . . . . . . . . . . . . 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 22157	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
63	53, 61, 62	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
64		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
65		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
66	10, 64, 4, 65, 11	lmod0vs 20801	. . . . . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
69	68	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
70	40, 69	sylan9eqr 2786	. . . . . . . . . . . . . . 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 3145	. . . . . . . . . . . 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 5111	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥))
77		fveq2 6858	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝑥))
78	77	oveqd 7404	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝑥)𝑗))
79		oveq1 7394	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌))
80	78, 79	oveq12d 7405	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)))
81	80	eqeq1d 2731	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃) ↔ ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
82	76, 81	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
83	82	cbvralvw 3215	. . . . . . . . . 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 19916	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))
86	85	fveq2d 6862	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
87	86	fveq1d 6860	. . . . . 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 13581	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ₀)
92	90, 91	syl11 33	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
93	92	ralrimiv 3124	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
94		fzfid 13938	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin)
95	8, 10, 20, 89, 93, 94	coe1fzgsumd 22191	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
96	87, 95	eqtrd 2764	. . . . 5 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
97	96	mpoeq3dva 7466	. . . 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 22313	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
105	91	adantl 481	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ₀)
106	43, 22, 8, 6, 4, 34, 5	coe1tm 22159	. . . . . . . . . 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 2733	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘))
109	108	ifbid 4512	. . . . . . . . . 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 7420	. . . . . . . . . . 11 ⊢ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ V
113		fvex 6871	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) ∈ V
114	112, 113	ifex 4539	. . . . . . . . . 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 6975	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
117	116	mpteq2dva 5200	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
118	117	oveq2d 7403	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))))
119	118	mpoeq3dva 7466	. . . . 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 5111	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾))
122		fveqeq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) ↔ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
123	121, 122	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))))
124	123	rspcva 3586	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
125	1, 43	mat0op 22306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
126	125	eqcomd 2735	. . . . . . . . . . . . . . . . . . . 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 13579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠))
130		nn0re 12451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
131	130	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑘 ∈ ℝ)
132		nn0re 12451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ ℕ₀ → 𝑠 ∈ ℝ)
133	132	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑠 ∈ ℝ)
134		nn0re 12451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℝ)
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝐾 ∈ ℝ)
136		lelttr 11264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
137	131, 133, 135, 136	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
138		animorr 980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))
139		df-ne 2926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘)
140	130	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → 𝑘 ∈ ℝ)
141		lttri2 11256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = (0_g‘𝑅))
162	161	mpteq2dva 5200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅)))
163	162	oveq2d 7403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))))
164		ringmnd 20152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
165	164	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd)
166		ovex 7420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑠) ∈ V
167	43	gsumz 18763	. . . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (0_g‘𝑅))
172	171	mpoeq3dva 7466	. . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . 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 7422	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V)
191		lenlt 11252	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
192	134, 132, 191	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
193		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ ℕ₀)
194		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ₀)
195		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠)
196		elfz2nn0 13579	. . . . . . . . . . . . . . 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 2736	. . . . . . . . . . 11 ⊢ (𝐾 = 𝑘 ↔ 𝑘 = 𝐾)
204		ifbi 4511	. . . . . . . . . . 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 5203	. . . . . . . . 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 22313	. . . . . . . . . . 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 3125	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
215	43, 189, 190, 202, 206, 214	gsummpt1n0 19895	. . . . . . . 8 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))
216	215	mpoeq3dva 7466	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)))
217		csbov 7432	. . . . . . . . . . . . . . 15 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗)
218		csbfv 6908	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾)
219	218	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾))
220	219	oveqd 7404	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ₀ → (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
221	217, 220	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
222	221	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
223	222	mpoeq3dv 7468	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe₁‘𝑂)‘𝐾)𝑗)))
224		oveq12 7396	. . . . . . . . . . . . 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 7422	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe₁‘𝑂)‘𝐾)𝑏) ∈ V)
229	223, 225, 226, 227, 228	ovmpod 7541	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
230	229	ralrimivva 3180	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
231		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑁 ∈ Fin)
232	218	oveqi 7400	. . . . . . . . . . . . . 14 ⊢ (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
233	217, 232	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
234		simp2 1137	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
235		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
236	29, 3, 2, 23	coe1fvalcl 22097	. . . . . . . . . . . . . . . 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 22313	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅))
240	233, 239	eqeltrid 2832	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
241	1, 22, 23, 231, 18, 240	matbas2d 22310	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴))
242	1, 23	eqmat 22311	. . . . . . . . . . 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 2764	. . . . . 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 2768	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
251		eqid 2729	. . . . . 6 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
252	29, 3, 2, 251	coe1sfi 22098	. . . . 5 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) finSupp (0_g‘𝐴))
253	26, 252	syl 17	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) finSupp (0_g‘𝐴))
254	29, 3, 2, 251, 23	coe1fsupp 22099	. . . . . 6 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)})
255		elrabi 3654	. . . . . 6 ⊢ ((coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)} → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
256	26, 254, 255	3syl 18	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
257		fvex 6871	. . . . 5 ⊢ (0_g‘𝐴) ∈ V
258		fsuppmapnn0ub 13960	. . . . 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 3141	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
262	9, 261	eqtrd 2764	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 2925 ∀wral 3044 ∃wrex 3053 {crab 3405 Vcvv 3447 ⦋csb 3862 ifcif 4488 class class class wbr 5107 ↦ cmpt 5188 ‘cfv 6511 (class class class)co 7387 ∈ cmpo 7389 ↑_m cmap 8799 Fincfn 8918 finSupp cfsupp 9312 ℝcr 11067 0cc0 11068 < clt 11208 ≤ cle 11209 ℕ₀cn0 12442 ...cfz 13468 Basecbs 17179 Scalarcsca 17223 ·_𝑠 cvsca 17224 0_gc0g 17402 Σ_g cgsu 17403 Mndcmnd 18661 ._gcmg 18999 CMndccmn 19710 mulGrpcmgp 20049 Ringcrg 20142 LModclmod 20766 var₁cv1 22060 Poly₁cpl1 22061 coe₁cco1 22062 Mat cmat 22294 decompPMat cdecpmat 22649

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 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-ot 4598 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-ofr 7654 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-sup 9393 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-fz 13469 df-fzo 13616 df-seq 13967 df-hash 14296 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18710 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-mulg 19000 df-subg 19055 df-ghm 19145 df-cntz 19249 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-ring 20144 df-subrng 20455 df-subrg 20479 df-lmod 20768 df-lss 20838 df-sra 21080 df-rgmod 21081 df-dsmm 21641 df-frlm 21656 df-psr 21818 df-mvr 21819 df-mpl 21820 df-opsr 21822 df-psr1 22064 df-vr1 22065 df-ply1 22066 df-coe1 22067 df-mat 22295 df-decpmat 22650

This theorem is referenced by: mp2pm2mplem5 22697 mp2pm2mp 22698

W3C validator