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 22783

Description: Lemma 4 for mp2pm2mp 22785. (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 22782	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)))
10		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘𝑃)
11		eqid 2737	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
12	8	ply1ring 22220	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
13	12	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring)
14		ringcmn 20252	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ CMnd)
16	15	ad3antrrr 731	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑃 ∈ CMnd)
17	16	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ CMnd)
18		simpl2 1194	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑅 ∈ Ring)
19	18	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Ring)
20	19	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
21	20	adantr 480	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑅 ∈ Ring)
22		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
23		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘𝐴) = (Base‘𝐴)
24		simpl2 1194	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
25		simpl3 1195	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
26		simpl3 1195	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑂 ∈ 𝐿)
27	26	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑂 ∈ 𝐿)
28	27	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
29		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (coe₁‘𝑂) = (coe₁‘𝑂)
30	29, 3, 2, 23	coe1fvalcl 22185	. . . . . . . . . . . . 13 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
31	28, 30	sylan 581	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
32	1, 22, 23, 24, 25, 31	matecld 22400	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
33		simpr 484	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
34		eqid 2737	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 22246	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
36	21, 32, 33, 35	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
37	36	ralrimiva 3130	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
38		simp1lr 1239	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ₀)
39		oveq 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → (𝑖((coe₁‘𝑂)‘𝑥)𝑗) = (𝑖(0_g‘𝐴)𝑗))
40	39	oveq1d 7373	. . . . . . . . . . . . . . . 16 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)))
41		3simpa 1149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
42	41	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
43		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
44	1, 43	mat0op 22393	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
45	42, 44	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
46		eqidd 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0_g‘𝑅) = (0_g‘𝑅))
47		simprl 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁)
48		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁)
49		fvexd 6847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝑅) ∈ V)
50	45, 46, 47, 48, 49	ovmpod 7510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
51	50	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
52	51	oveq1d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0_g‘𝑅) · (𝑥𝐸𝑌)))
53	18	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 ∈ Ring)
54	8	ply1sca 22225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 = (Scalar‘𝑃))
56	55	fveq2d 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
57	56	oveq1d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘𝑅) · (𝑥𝐸𝑌)) = ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)))
58	8	ply1lmod 22224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
59	58	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ LMod)
60	59	ad4antr 733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑃 ∈ LMod)
61		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62	8, 6, 34, 5, 10	ply1moncl 22245	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
63	53, 61, 62	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
64		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
65		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
66	10, 64, 4, 65, 11	lmod0vs 20879	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
67	60, 63, 66	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
68	52, 57, 67	3eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
69	68	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
70	40, 69	sylan9eqr 2794	. . . . . . . . . . . . . . 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 3150	. . . . . . . . . . . 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 1117	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
76		breq2 5090	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥))
77		fveq2 6832	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝑥))
78	77	oveqd 7375	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝑥)𝑗))
79		oveq1 7365	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌))
80	78, 79	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)))
81	80	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃) ↔ ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
82	76, 81	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
83	82	cbvralvw 3216	. . . . . . . . . 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 19950	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))
86	85	fveq2d 6836	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
87	86	fveq1d 6834	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))
88		simpllr 776	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝐾 ∈ ℕ₀)
89	88	3ad2ant1 1134	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ ℕ₀)
90	36	expcom 413	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ₀ → ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
91		elfznn0 13563	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ₀)
92	90, 91	syl11 33	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
93	92	ralrimiv 3129	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
94		fzfid 13924	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin)
95	8, 10, 20, 89, 93, 94	coe1fzgsumd 22278	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
96	87, 95	eqtrd 2772	. . . . 5 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
97	96	mpoeq3dva 7435	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))))
98	18	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
99	98	adantr 480	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
100		simpl2 1194	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑖 ∈ 𝑁)
101		simpl3 1195	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑗 ∈ 𝑁)
102	26	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
103	102, 91, 30	syl2an 597	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
104	1, 22, 23, 100, 101, 103	matecld 22400	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
105	91	adantl 481	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ₀)
106	43, 22, 8, 6, 4, 34, 5	coe1tm 22247	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
107	99, 104, 105, 106	syl3anc 1374	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
108		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘))
109	108	ifbid 4491	. . . . . . . . . 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 1227	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝐾 ∈ ℕ₀)
112		ovex 7391	. . . . . . . . . . 11 ⊢ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ V
113		fvex 6845	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) ∈ V
114	112, 113	ifex 4518	. . . . . . . . . 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 6947	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
117	116	mpteq2dva 5179	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
118	117	oveq2d 7374	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))))
119	118	mpoeq3dva 7435	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
120	119	ad2antrr 727	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
121		breq2 5090	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾))
122		fveqeq2 6841	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) ↔ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
123	121, 122	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))))
124	123	rspcva 3563	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
125	1, 43	mat0op 22393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
126	125	eqcomd 2743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
127	126	3adant3 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
128	127	ad3antlr 732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
129		elfz2nn0 13561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠))
130		nn0re 12435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
131	130	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑘 ∈ ℝ)
132		nn0re 12435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ ℕ₀ → 𝑠 ∈ ℝ)
133	132	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑠 ∈ ℝ)
134		nn0re 12435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℝ)
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝐾 ∈ ℝ)
136		lelttr 11225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
137	131, 133, 135, 136	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
138		animorr 981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))
139		df-ne 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘)
140	130	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → 𝑘 ∈ ℝ)
141		lttri2 11217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
142	134, 140, 141	syl2anr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
160	159	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐾 = 𝑘)
161	160	iffalsed 4478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = (0_g‘𝑅))
162	161	mpteq2dva 5179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅)))
163	162	oveq2d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))))
164		ringmnd 20213	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
165	164	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd)
166		ovex 7391	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑠) ∈ V
167	43	gsumz 18793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
168	165, 166, 167	sylancl 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
169	168	ad3antlr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
170	169	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
171	163, 170	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (0_g‘𝑅))
172	171	mpoeq3dva 7435	. . . . . . . . . . . . . . . . . 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 2782	. . . . . . . . . . . . . . . . 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 731	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Mnd)
188	187	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑅 ∈ Mnd)
189	188	3ad2ant1 1134	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Mnd)
190		ovexd 7393	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V)
191		lenlt 11213	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
192	134, 132, 191	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
193		simpll 767	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ ℕ₀)
194		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ₀)
195		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠)
196		elfz2nn0 13561	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (0...𝑠) ↔ (𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑠))
197	193, 194, 195, 196	syl3anbrc 1345	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ (0...𝑠))
198	197	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 → 𝐾 ∈ (0...𝑠)))
199	192, 198	sylbird 260	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
200	199	ad4ant23 754	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
201	200	impcom 407	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝐾 ∈ (0...𝑠))
202	201	3ad2ant1 1134	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ (0...𝑠))
203		eqcom 2744	. . . . . . . . . . 11 ⊢ (𝐾 = 𝑘 ↔ 𝑘 = 𝐾)
204		ifbi 4490	. . . . . . . . . . 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 5182	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐾, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
207		simpl2 1194	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
208		simpl3 1195	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
209	27	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑂 ∈ 𝐿)
210	209	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
211	210, 30	sylan 581	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
212	1, 22, 23, 207, 208, 211	matecld 22400	. . . . . . . . . . 11 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
213	91, 212	sylan2 594	. . . . . . . . . 10 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
214	213	ralrimiva 3130	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
215	43, 189, 190, 202, 206, 214	gsummpt1n0 19929	. . . . . . . 8 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))
216	215	mpoeq3dva 7435	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)))
217		csbov 7403	. . . . . . . . . . . . . . 15 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗)
218		csbfv 6879	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾)
219	218	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾))
220	219	oveqd 7375	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ₀ → (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
221	217, 220	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
222	221	ad2antlr 728	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
223	222	mpoeq3dv 7437	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe₁‘𝑂)‘𝐾)𝑗)))
224		oveq12 7367	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
225	224	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
226		simprl 771	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁)
227		simprr 773	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁)
228		ovexd 7393	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe₁‘𝑂)‘𝐾)𝑏) ∈ V)
229	223, 225, 226, 227, 228	ovmpod 7510	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
230	229	ralrimivva 3181	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
231		simpl1 1193	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑁 ∈ Fin)
232	218	oveqi 7371	. . . . . . . . . . . . . 14 ⊢ (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
233	217, 232	eqtri 2760	. . . . . . . . . . . . 13 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
234		simp2 1138	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
235		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
236	29, 3, 2, 23	coe1fvalcl 22185	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
237	236	3ad2antl3 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
238	237	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
239	1, 22, 23, 234, 235, 238	matecld 22400	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅))
240	233, 239	eqeltrid 2841	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
241	1, 22, 23, 231, 18, 240	matbas2d 22397	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴))
242	1, 23	eqmat 22398	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴) ∧ ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏)))
243	241, 237, 242	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏)))
244	230, 243	mpbird 257	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
245	244	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
246	245	adantl 481	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
247	216, 246	eqtrd 2772	. . . . . 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 2776	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
251		eqid 2737	. . . . . 6 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
252	29, 3, 2, 251	coe1sfi 22186	. . . . 5 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) finSupp (0_g‘𝐴))
253	26, 252	syl 17	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) finSupp (0_g‘𝐴))
254	29, 3, 2, 251, 23	coe1fsupp 22187	. . . . . 6 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)})
255		elrabi 3631	. . . . . 6 ⊢ ((coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)} → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
256	26, 254, 255	3syl 18	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
257		fvex 6845	. . . . 5 ⊢ (0_g‘𝐴) ∈ V
258		fsuppmapnn0ub 13946	. . . . 5 ⊢ (((coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀) ∧ (0_g‘𝐴) ∈ V) → ((coe₁‘𝑂) finSupp (0_g‘𝐴) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))))
259	256, 257, 258	sylancl 587	. . . 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 3146	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
262	9, 261	eqtrd 2772	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe₁‘𝑂)‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 Vcvv 3430 ⦋csb 3838 ifcif 4467 class class class wbr 5086 ↦ cmpt 5167 ‘cfv 6490 (class class class)co 7358 ∈ cmpo 7360 ↑_m cmap 8764 Fincfn 8884 finSupp cfsupp 9265 ℝcr 11026 0cc0 11027 < clt 11168 ≤ cle 11169 ℕ₀cn0 12426 ...cfz 13450 Basecbs 17168 Scalarcsca 17212 ·_𝑠 cvsca 17213 0_gc0g 17391 Σ_g cgsu 17392 Mndcmnd 18691 ._gcmg 19032 CMndccmn 19744 mulGrpcmgp 20110 Ringcrg 20203 LModclmod 20844 var₁cv1 22148 Poly₁cpl1 22149 coe₁cco1 22150 Mat cmat 22381 decompPMat cdecpmat 22736

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-ot 4577 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-ofr 7623 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8102 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-pm 8767 df-ixp 8837 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-sup 9346 df-oi 9416 df-card 9852 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-7 12238 df-8 12239 df-9 12240 df-n0 12427 df-z 12514 df-dec 12634 df-uz 12778 df-fz 13451 df-fzo 13598 df-seq 13953 df-hash 14282 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-sca 17225 df-vsca 17226 df-ip 17227 df-tset 17228 df-ple 17229 df-ds 17231 df-hom 17233 df-cco 17234 df-0g 17393 df-gsum 17394 df-prds 17399 df-pws 17401 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-mhm 18740 df-submnd 18741 df-grp 18901 df-minusg 18902 df-sbg 18903 df-mulg 19033 df-subg 19088 df-ghm 19177 df-cntz 19281 df-cmn 19746 df-abl 19747 df-mgp 20111 df-rng 20123 df-ur 20152 df-ring 20205 df-subrng 20512 df-subrg 20536 df-lmod 20846 df-lss 20916 df-sra 21158 df-rgmod 21159 df-dsmm 21720 df-frlm 21735 df-psr 21897 df-mvr 21898 df-mpl 21899 df-opsr 21901 df-psr1 22152 df-vr1 22153 df-ply1 22154 df-coe1 22155 df-mat 22382 df-decpmat 22737

This theorem is referenced by: mp2pm2mplem5 22784 mp2pm2mp 22785

W3C validator