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 22947

Description: Lemma 4 for mp2pm2mp 22949. (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 22946	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)))
10		eqid 2763	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘𝑃)
11		eqid 2763	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
12	8	ply1ring 22388	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
13	12	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring)
14		ringcmn 20366	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
15	13, 14	syl 18	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ CMnd)
16	15	ad3antrrr 742	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑃 ∈ CMnd)
17	16	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ CMnd)
18		simpl2 1211	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑅 ∈ Ring)
19	18	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Ring)
20	19	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
21	20	adantr 485	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑅 ∈ Ring)
22		eqid 2763	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
23		eqid 2763	. . . . . . . . . . . 12 ⊢ (Base‘𝐴) = (Base‘𝐴)
24		simpl2 1211	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
25		simpl3 1212	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
26		simpl3 1212	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑂 ∈ 𝐿)
27	26	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑂 ∈ 𝐿)
28	27	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
29		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (coe₁‘𝑂) = (coe₁‘𝑂)
30	29, 3, 2, 23	coe1fvalcl 22353	. . . . . . . . . . . . 13 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
31	28, 30	sylan 591	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
32	1, 22, 23, 24, 25, 31	matecld 22564	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
33		simpr 489	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
34		eqid 2763	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 22414	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
36	21, 32, 33, 35	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
37	36	ralrimiva 3157	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
38		simp1lr 1256	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ₀)
39		oveq 7418	. . . . . . . . . . . . . . . . 17 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → (𝑖((coe₁‘𝑂)‘𝑥)𝑗) = (𝑖(0_g‘𝐴)𝑗))
40	39	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)))
41		3simpa 1166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
42	41	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
43		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
44	1, 43	mat0op 22557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
45	42, 44	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
46		eqidd 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0_g‘𝑅) = (0_g‘𝑅))
47		simprl 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁)
48		simprr 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁)
49		fvexd 6898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝑅) ∈ V)
50	45, 46, 47, 48, 49	ovmpod 7564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
51	50	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
52	51	oveq1d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0_g‘𝑅) · (𝑥𝐸𝑌)))
53	18	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 ∈ Ring)
54	8	ply1sca 22393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 = (Scalar‘𝑃))
56	55	fveq2d 6887	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
57	56	oveq1d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘𝑅) · (𝑥𝐸𝑌)) = ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)))
58	8	ply1lmod 22392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
59	58	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ LMod)
60	59	ad4antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑃 ∈ LMod)
61		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62	8, 6, 34, 5, 10	ply1moncl 22413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
63	53, 61, 62	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
64		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
65		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
66	10, 64, 4, 65, 11	lmod0vs 20997	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
67	60, 63, 66	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
68	52, 57, 67	3eqtrd 2802	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
69	68	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
70	40, 69	sylan9eqr 2820	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) ∧ ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
71	70	exp31 424	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑠 < 𝑥 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
72	71	a2d 30	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
73	72	ralimdva 3177	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
74	73	impancom 456	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
75	74	3impib 1134	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
76		breq2 5114	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥))
77		fveq2 6883	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝑥))
78	77	oveqd 7429	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝑥)𝑗))
79		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌))
80	78, 79	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)))
81	80	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃) ↔ ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
82	76, 81	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
83	82	cbvralvw 3243	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ₀ (𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
84	75, 83	sylibr 237	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ (𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)))
85	10, 11, 17, 37, 38, 84	gsummptnn0fz 20057	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))
86	85	fveq2d 6887	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
87	86	fveq1d 6885	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))
88		simpllr 787	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝐾 ∈ ℕ₀)
89	88	3ad2ant1 1151	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ ℕ₀)
90	36	expcom 418	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ₀ → ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
91		elfznn0 13650	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ₀)
92	90, 91	syl11 34	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
93	92	ralrimiv 3156	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
94		fzfid 14011	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin)
95	8, 10, 20, 89, 93, 94	coe1fzgsumd 22445	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
96	87, 95	eqtrd 2798	. . . . 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 1151	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
99	98	adantr 485	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
100		simpl2 1211	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑖 ∈ 𝑁)
101		simpl3 1212	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑗 ∈ 𝑁)
102	26	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
103	102, 91, 30	syl2an 607	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
104	1, 22, 23, 100, 101, 103	matecld 22564	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
105	91	adantl 486	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ₀)
106	43, 22, 8, 6, 4, 34, 5	coe1tm 22415	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
107	99, 104, 105, 106	syl3anc 1398	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
108		eqeq1 2767	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘))
109	108	ifbid 4512	. . . . . . . . . 10 ⊢ (𝑙 = 𝐾 → if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
110	109	adantl 486	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑙 = 𝐾) → if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
111		simpl1r 1244	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝐾 ∈ ℕ₀)
112		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ V
113		fvex 6896	. . . . . . . . . . 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 6999	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
117	116	mpteq2dva 5205	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
118	117	oveq2d 7428	. . . . . 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 738	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
121		breq2 5114	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾))
122		fveqeq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) ↔ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
123	121, 122	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))))
124	123	rspcva 3580	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
125	1, 43	mat0op 22557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
126	125	eqcomd 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
127	126	3adant3 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
128	127	ad3antlr 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
129		elfz2nn0 13648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠))
130		nn0re 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
131	130	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑘 ∈ ℝ)
132		nn0re 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ ℕ₀ → 𝑠 ∈ ℝ)
133	132	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑠 ∈ ℝ)
134		nn0re 12514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℝ)
135	134	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝐾 ∈ ℝ)
136		lelttr 11301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
137	131, 133, 135, 136	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
138		animorr 994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))
139		df-ne 2959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘)
140	130	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → 𝑘 ∈ ℝ)
141		lttri2 11293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
142	134, 140, 141	syl2anr 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
143	142	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
144	139, 143	bitr3id 288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (¬ 𝐾 = 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
145	138, 144	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → ¬ 𝐾 = 𝑘)
146	145	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → (𝑘 < 𝐾 → ¬ 𝐾 = 𝑘))
147	137, 146	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → ¬ 𝐾 = 𝑘))
148	147	exp4b 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ∈ ℕ₀ → (𝑘 ≤ 𝑠 → (𝑠 < 𝐾 → ¬ 𝐾 = 𝑘))))
149	148	com24 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝑠 < 𝐾 → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
150	149	expimpd 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ ℕ₀ → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
151	150	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
152	151	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
153	152	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
154	129, 153	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
155	154	com13 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐾 ∈ ℕ₀ → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)))
156	155	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)))
157	156	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
158	157	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
159	158	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
160	159	imp 411	. . . . . . . . . . . . . . . . . . . . . . 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 5205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅)))
163	162	oveq2d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))))
164		ringmnd 20326	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
165	164	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd)
166		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑠) ∈ V
167	43	gsumz 18896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
168	165, 166, 167	sylancl 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
169	168	ad3antlr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
170	169	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
171	163, 170	eqtrd 2798	. . . . . . . . . . . . . . . . . . 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 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))
174	128, 172, 173	3eqtr4d 2808	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
175	174	ex 417	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) → (((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
176	175	expr 461	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ₀) → (𝑠 < 𝐾 → (((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))
177	176	a2d 30	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ₀) → ((𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))
178	177	exp31 424	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℕ₀ → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → ((𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
179	178	com14 97	. . . . . . . . . . . 12 ⊢ ((𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
180	124, 179	syl 18	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
181	180	ex 417	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))))
182	181	com25 100	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ₀ → (𝐾 ∈ ℕ₀ → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))))
183	182	pm2.43i 53	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ₀ → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))))))
184	183	impcom 412	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))
185	184	imp31 422	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
186	185	com12 33	. . . . 5 ⊢ (𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
187	165	ad3antrrr 742	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Mnd)
188	187	adantl 486	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑅 ∈ Mnd)
189	188	3ad2ant1 1151	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Mnd)
190		ovexd 7447	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V)
191		lenlt 11289	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
192	134, 132, 191	syl2an 607	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
193		simpll 778	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ ℕ₀)
194		simplr 780	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ₀)
195		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠)
196		elfz2nn0 13648	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (0...𝑠) ↔ (𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑠))
197	193, 194, 195, 196	syl3anbrc 1362	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ (0...𝑠))
198	197	ex 417	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 → 𝐾 ∈ (0...𝑠)))
199	192, 198	sylbird 263	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
200	199	ad4ant23 765	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
201	200	impcom 412	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝐾 ∈ (0...𝑠))
202	201	3ad2ant1 1151	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ (0...𝑠))
203		eqcom 2770	. . . . . . . . . . 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 5208	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐾, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
207		simpl2 1211	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
208		simpl3 1212	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
209	27	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑂 ∈ 𝐿)
210	209	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
211	210, 30	sylan 591	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
212	1, 22, 23, 207, 208, 211	matecld 22564	. . . . . . . . . . 11 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
213	91, 212	sylan2 604	. . . . . . . . . 10 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
214	213	ralrimiva 3157	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
215	43, 189, 190, 202, 206, 214	gsummpt1n0 20036	. . . . . . . 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 7457	. . . . . . . . . . . . . . 15 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗)
218		csbfv 6930	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾)
219	218	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾))
220	219	oveqd 7429	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ₀ → (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
221	217, 220	eqtrid 2810	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
222	221	ad2antlr 739	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
223	222	mpoeq3dv 7491	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe₁‘𝑂)‘𝐾)𝑗)))
224		oveq12 7421	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
225	224	adantl 486	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
226		simprl 782	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁)
227		simprr 784	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁)
228		ovexd 7447	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe₁‘𝑂)‘𝐾)𝑏) ∈ V)
229	223, 225, 226, 227, 228	ovmpod 7564	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
230	229	ralrimivva 3208	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
231		simpl1 1210	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑁 ∈ Fin)
232	218	oveqi 7425	. . . . . . . . . . . . . 14 ⊢ (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
233	217, 232	eqtri 2786	. . . . . . . . . . . . 13 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
234		simp2 1155	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
235		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
236	29, 3, 2, 23	coe1fvalcl 22353	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
237	236	3ad2antl3 1206	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
238	237	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
239	1, 22, 23, 234, 235, 238	matecld 22564	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅))
240	233, 239	eqeltrid 2867	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
241	1, 22, 23, 231, 18, 240	matbas2d 22561	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴))
242	1, 23	eqmat 22562	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴) ∧ ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏)))
243	241, 237, 242	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏)))
244	230, 243	mpbird 260	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
245	244	ad2antrr 738	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
246	245	adantl 486	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
247	216, 246	eqtrd 2798	. . . . . 6 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
248	247	ex 417	. . . . 5 ⊢ (¬ 𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
249	186, 248	pm2.61i 184	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
250	97, 120, 249	3eqtrd 2802	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
251		eqid 2763	. . . . . 6 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
252	29, 3, 2, 251	coe1sfi 22354	. . . . 5 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) finSupp (0_g‘𝐴))
253	26, 252	syl 18	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) finSupp (0_g‘𝐴))
254	29, 3, 2, 251, 23	coe1fsupp 22355	. . . . . 6 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)})
255		elrabi 3647	. . . . . 6 ⊢ ((coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)} → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
256	26, 254, 255	3syl 19	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
257		fvex 6896	. . . . 5 ⊢ (0_g‘𝐴) ∈ V
258		fsuppmapnn0ub 14033	. . . . 5 ⊢ (((coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀) ∧ (0_g‘𝐴) ∈ V) → ((coe₁‘𝑂) finSupp (0_g‘𝐴) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))))
259	256, 257, 258	sylancl 597	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂) finSupp (0_g‘𝐴) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))))
260	253, 259	mpd 16	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∃𝑠 ∈ ℕ₀ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))
261	250, 260	r19.29a 3173	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
262	9, 261	eqtrd 2798	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe₁‘𝑂)‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 {crab 3416 Vcvv 3455 ⦋csb 3854 ifcif 4488 class class class wbr 5110 ↦ cmpt 5193 ‘cfv 6538 (class class class)co 7412 ∈ cmpo 7414 ↑_m cmap 8825 Fincfn 8944 finSupp cfsupp 9322 ℝcr 11100 0cc0 11101 < clt 11244 ≤ cle 11245 ℕ₀cn0 12505 ...cfz 13536 Basecbs 17270 Scalarcsca 17314 ·_𝑠 cvsca 17315 0_gc0g 17493 Σ_g cgsu 17494 Mndcmnd 18793 ._gcmg 19134 CMndccmn 19851 mulGrpcmgp 20217 Ringcrg 20316 LModclmod 20962 var₁cv1 22317 Poly₁cpl1 22318 coe₁cco1 22319 Mat cmat 22545 decompPMat cdecpmat 22900

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-tp 4595 df-op 4597 df-ot 4599 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-ofr 7677 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8158 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-2o 8455 df-er 8695 df-map 8827 df-pm 8828 df-ixp 8897 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-fsupp 9323 df-sup 9403 df-oi 9473 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-5 12307 df-6 12308 df-7 12309 df-8 12310 df-9 12311 df-n0 12506 df-z 12593 df-dec 12713 df-uz 12864 df-fz 13537 df-fzo 13685 df-seq 14040 df-hash 14369 df-struct 17208 df-sets 17225 df-slot 17243 df-ndx 17255 df-base 17271 df-ress 17292 df-plusg 17324 df-mulr 17325 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-hom 17335 df-cco 17336 df-0g 17495 df-gsum 17496 df-prds 17501 df-pws 17503 df-mre 17639 df-mrc 17640 df-acs 17642 df-mgm 18699 df-sgrp 18778 df-mnd 18794 df-mhm 18842 df-submnd 18843 df-grp 19004 df-minusg 19005 df-sbg 19006 df-mulg 19135 df-subg 19190 df-ghm 19285 df-cntz 19388 df-cmn 19853 df-abl 19854 df-mgp 20218 df-rng 20232 df-ur 20265 df-ring 20318 df-subrng 20632 df-subrg 20656 df-lmod 20964 df-lss 21034 df-sra 21275 df-rgmod 21276 df-dsmm 21863 df-frlm 21878 df-psr 22040 df-mvr 22041 df-mpl 22042 df-opsr 22044 df-psr1 22321 df-vr1 22322 df-ply1 22323 df-coe1 22324 df-mat 22546 df-decpmat 22901

This theorem is referenced by: mp2pm2mplem5 22948 mp2pm2mp 22949

W3C validator