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 22038

Description: Lemma 4 for mp2pm2mp 22040. (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 22037	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)))
10		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘𝑃)
11		eqid 2736	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
12	8	ply1ring 21499	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
13	12	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring)
14		ringcmn 19892	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ CMnd)
16	15	ad3antrrr 727	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑃 ∈ CMnd)
17	16	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ CMnd)
18		simpl2 1191	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑅 ∈ Ring)
19	18	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Ring)
20	19	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
21	20	adantr 481	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑅 ∈ Ring)
22		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
23		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘𝐴) = (Base‘𝐴)
24		simpl2 1191	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
25		simpl3 1192	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
26		simpl3 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑂 ∈ 𝐿)
27	26	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑂 ∈ 𝐿)
28	27	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
29		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (coe₁‘𝑂) = (coe₁‘𝑂)
30	29, 3, 2, 23	coe1fvalcl 21463	. . . . . . . . . . . . 13 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
31	28, 30	sylan 580	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
32	1, 22, 23, 24, 25, 31	matecld 21655	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
33		simpr 485	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
34		eqid 2736	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
35	22, 8, 6, 4, 34, 5, 10	ply1tmcl 21523	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
36	21, 32, 33, 35	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
37	36	ralrimiva 3139	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
38		simp1lr 1236	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ₀)
39		oveq 7322	. . . . . . . . . . . . . . . . 17 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → (𝑖((coe₁‘𝑂)‘𝑥)𝑗) = (𝑖(0_g‘𝐴)𝑗))
40	39	oveq1d 7331	. . . . . . . . . . . . . . . 16 ⊢ (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)))
41		3simpa 1147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
42	41	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
43		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
44	1, 43	mat0op 21648	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
45	42, 44	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0_g‘𝑅)))
46		eqidd 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0_g‘𝑅) = (0_g‘𝑅))
47		simprl 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁)
48		simprr 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁)
49		fvexd 6826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0_g‘𝑅) ∈ V)
50	45, 46, 47, 48, 49	ovmpod 7466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
51	50	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑖(0_g‘𝐴)𝑗) = (0_g‘𝑅))
52	51	oveq1d 7331	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0_g‘𝑅) · (𝑥𝐸𝑌)))
53	18	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 ∈ Ring)
54	8	ply1sca 21504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑅 = (Scalar‘𝑃))
56	55	fveq2d 6815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
57	56	oveq1d 7331	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((0_g‘𝑅) · (𝑥𝐸𝑌)) = ((0_g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)))
58	8	ply1lmod 21503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
59	58	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ LMod)
60	59	ad4antr 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑃 ∈ LMod)
61		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62	8, 6, 34, 5, 10	ply1moncl 21522	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
63	53, 61, 62	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → (𝑥𝐸𝑌) ∈ (Base‘𝑃))
64		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
65		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
66	10, 64, 4, 65, 11	lmod0vs 20236	. . . . . . . . . . . . . . . . . . 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 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
69	68	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) → ((𝑖(0_g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
70	40, 69	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ₀) ∧ 𝑠 < 𝑥) ∧ ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))
71	70	exp31 420	. . . . . . . . . . . . . 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 3160	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
74	73	impancom 452	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
75	74	3impib 1115	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
76		breq2 5090	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥))
77		fveq2 6811	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝑥))
78	77	oveqd 7333	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝑥)𝑗))
79		oveq1 7323	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌))
80	78, 79	oveq12d 7334	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)))
81	80	eqeq1d 2738	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → (((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃) ↔ ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
82	76, 81	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃))))
83	82	cbvralvw 3221	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ₀ (𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)) ↔ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((𝑖((coe₁‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0_g‘𝑃)))
84	75, 83	sylibr 233	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ₀ (𝑠 < 𝑘 → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0_g‘𝑃)))
85	10, 11, 17, 37, 38, 84	gsummptnn0fz 19659	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))
86	85	fveq2d 6815	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))))
87	86	fveq1d 6813	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))
88		simpllr 773	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝐾 ∈ ℕ₀)
89	88	3ad2ant1 1132	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ ℕ₀)
90	36	expcom 414	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ₀ → ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
91		elfznn0 13428	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ₀)
92	90, 91	syl11 33	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)))
93	92	ralrimiv 3138	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))
94		fzfid 13772	. . . . . . 7 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin)
95	8, 10, 20, 89, 93, 94	coe1fzgsumd 21553	. . . . . 6 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
96	87, 95	eqtrd 2776	. . . . 5 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))
97	96	mpoeq3dva 7393	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))))
98	18	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
99	98	adantr 481	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
100		simpl2 1191	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑖 ∈ 𝑁)
101		simpl3 1192	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑗 ∈ 𝑁)
102	26	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿)
103	102, 91, 30	syl2an 596	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘𝑂)‘𝑘) ∈ (Base‘𝐴))
104	1, 22, 23, 100, 101, 103	matecld 21655	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
105	91	adantl 482	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ₀)
106	43, 22, 8, 6, 4, 34, 5	coe1tm 21524	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ₀) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
107	99, 104, 105, 106	syl3anc 1370	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
108		eqeq1 2740	. . . . . . . . . . 11 ⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘))
109	108	ifbid 4493	. . . . . . . . . 10 ⊢ (𝑙 = 𝐾 → if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
110	109	adantl 482	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑙 = 𝐾) → if(𝑙 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
111		simpl1r 1224	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝐾 ∈ ℕ₀)
112		ovex 7349	. . . . . . . . . . 11 ⊢ (𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ V
113		fvex 6824	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) ∈ V
114	112, 113	ifex 4520	. . . . . . . . . 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 6921	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
117	116	mpteq2dva 5186	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))
118	117	oveq2d 7332	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))))
119	118	mpoeq3dva 7393	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
120	119	ad2antrr 723	. . . 4 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ ((coe₁‘((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))))
121		breq2 5090	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾))
122		fveqeq2 6820	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐾 → (((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴) ↔ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
123	121, 122	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))))
124	123	rspcva 3567	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑠 < 𝐾 → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)))
125	1, 43	mat0op 21648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
126	125	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
127	126	3adant3 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
128	127	ad3antlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)) = (0_g‘𝐴))
129		elfz2nn0 13426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠))
130		nn0re 12321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
131	130	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑘 ∈ ℝ)
132		nn0re 12321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ ℕ₀ → 𝑠 ∈ ℝ)
133	132	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝑠 ∈ ℝ)
134		nn0re 12321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℝ)
135	134	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → 𝐾 ∈ ℝ)
136		lelttr 11144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
137	131, 133, 135, 136	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾))
138		animorr 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))
139		df-ne 2941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘)
140	130	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → 𝑘 ∈ ℝ)
141		lttri2 11136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
142	134, 140, 141	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
143	142	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
144	139, 143	bitr3id 284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → (¬ 𝐾 = 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)))
145	138, 144	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑘 < 𝐾) → ¬ 𝐾 = 𝑘)
146	145	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → (𝑘 < 𝐾 → ¬ 𝐾 = 𝑘))
147	137, 146	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ∈ ℕ₀) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → ¬ 𝐾 = 𝑘))
148	147	exp4b 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ∈ ℕ₀ → (𝑘 ≤ 𝑠 → (𝑠 < 𝐾 → ¬ 𝐾 = 𝑘))))
149	148	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝑠 < 𝐾 → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
150	149	expimpd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ ℕ₀ → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
151	150	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘))))
152	151	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
153	152	3adant2 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
154	129, 153	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ₀ → ¬ 𝐾 = 𝑘)))
155	154	com13 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐾 ∈ ℕ₀ → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)))
156	155	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) → ((𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)))
157	156	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
158	157	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
159	158	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))
160	159	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐾 = 𝑘)
161	160	iffalsed 4481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)) = (0_g‘𝑅))
162	161	mpteq2dva 5186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅)))
163	162	oveq2d 7332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))))
164		ringmnd 19865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
165	164	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd)
166		ovex 7349	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑠) ∈ V
167	43	gsumz 18548	. . . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
170	169	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ (0_g‘𝑅))) = (0_g‘𝑅))
171	163, 170	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = (0_g‘𝑅))
172	171	mpoeq3dva 7393	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0_g‘𝑅)))
173		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴))
174	128, 172, 173	3eqtr4d 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) ∧ ((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
175	174	ex 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ₀ ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ₀ ∧ 𝑠 < 𝐾)) → (((coe₁‘𝑂)‘𝐾) = (0_g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))
176	175	expr 457	. . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . 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 413	. . . . . . . . . 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 408	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑠 ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾)))))
185	184	imp31 418	. . . . . 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 727	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → 𝑅 ∈ Mnd)
188	187	adantl 482	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑅 ∈ Mnd)
189	188	3ad2ant1 1132	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Mnd)
190		ovexd 7351	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V)
191		lenlt 11132	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
192	134, 132, 191	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾))
193		simpll 764	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ ℕ₀)
194		simplr 766	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ₀)
195		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠)
196		elfz2nn0 13426	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (0...𝑠) ↔ (𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑠))
197	193, 194, 195, 196	syl3anbrc 1342	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ (0...𝑠))
198	197	ex 413	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (𝐾 ≤ 𝑠 → 𝐾 ∈ (0...𝑠)))
199	192, 198	sylbird 259	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑠 ∈ ℕ₀) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
200	199	ad4ant23 750	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠)))
201	200	impcom 408	. . . . . . . . . 10 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝐾 ∈ (0...𝑠))
202	201	3ad2ant1 1132	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ (0...𝑠))
203		eqcom 2743	. . . . . . . . . . 11 ⊢ (𝐾 = 𝑘 ↔ 𝑘 = 𝐾)
204		ifbi 4492	. . . . . . . . . . 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 5191	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐾, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))
207		simpl2 1191	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑖 ∈ 𝑁)
208		simpl3 1192	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ₀) → 𝑗 ∈ 𝑁)
209	27	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → 𝑂 ∈ 𝐿)
210	209	3ad2ant1 1132	. . . . . . . . . . . . 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 21655	. . . . . . . . . . 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 3139	. . . . . . . . 9 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
215	43, 189, 190, 202, 206, 214	gsummpt1n0 19638	. . . . . . . 8 ⊢ (((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅)))) = ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))
216	215	mpoeq3dva 7393	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)))
217		csbov 7359	. . . . . . . . . . . . . . 15 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗)
218		csbfv 6858	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾)
219	218	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘) = ((coe₁‘𝑂)‘𝐾))
220	219	oveqd 7333	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ₀ → (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
221	217, 220	eqtrid 2788	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ₀ → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
222	221	ad2antlr 724	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗))
223	222	mpoeq3dv 7395	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe₁‘𝑂)‘𝐾)𝑗)))
224		oveq12 7325	. . . . . . . . . . . . 13 ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
225	224	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
226		simprl 768	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁)
227		simprr 770	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁)
228		ovexd 7351	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe₁‘𝑂)‘𝐾)𝑏) ∈ V)
229	223, 225, 226, 227, 228	ovmpod 7466	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
230	229	ralrimivva 3193	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe₁‘𝑂)‘𝐾)𝑏))
231		simpl1 1190	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → 𝑁 ∈ Fin)
232	218	oveqi 7329	. . . . . . . . . . . . . 14 ⊢ (𝑖⦋𝐾 / 𝑘⦌((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
233	217, 232	eqtri 2764	. . . . . . . . . . . . 13 ⊢ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) = (𝑖((coe₁‘𝑂)‘𝐾)𝑗)
234		simp2 1136	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
235		simp3 1137	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
236	29, 3, 2, 23	coe1fvalcl 21463	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
237	236	3ad2antl3 1186	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
238	237	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe₁‘𝑂)‘𝐾) ∈ (Base‘𝐴))
239	1, 22, 23, 234, 235, 238	matecld 21655	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe₁‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅))
240	233, 239	eqeltrid 2841	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅))
241	1, 22, 23, 231, 18, 240	matbas2d 21652	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴))
242	1, 23	eqmat 21653	. . . . . . . . . . 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 256	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
245	244	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
246	245	adantl 482	. . . . . . 7 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe₁‘𝑂)‘𝑘)𝑗)) = ((coe₁‘𝑂)‘𝐾))
247	216, 246	eqtrd 2776	. . . . . 6 ⊢ ((¬ 𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σ_g (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe₁‘𝑂)‘𝑘)𝑗), (0_g‘𝑅))))) = ((coe₁‘𝑂)‘𝐾))
248	247	ex 413	. . . . 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 2780	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) ∧ 𝑠 ∈ ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ (𝑠 < 𝑥 → ((coe₁‘𝑂)‘𝑥) = (0_g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
251		eqid 2736	. . . . . 6 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
252	29, 3, 2, 251	coe1sfi 21464	. . . . 5 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) finSupp (0_g‘𝐴))
253	26, 252	syl 17	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) finSupp (0_g‘𝐴))
254	29, 3, 2, 251, 23	coe1fsupp 21465	. . . . . 6 ⊢ (𝑂 ∈ 𝐿 → (coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)})
255		elrabi 3627	. . . . . 6 ⊢ ((coe₁‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑_m ℕ₀) ∣ 𝑥 finSupp (0_g‘𝐴)} → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
256	26, 254, 255	3syl 18	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (coe₁‘𝑂) ∈ ((Base‘𝐴) ↑_m ℕ₀))
257		fvex 6824	. . . . 5 ⊢ (0_g‘𝐴) ∈ V
258		fsuppmapnn0ub 13794	. . . . 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 3155	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe₁‘(𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑖((coe₁‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe₁‘𝑂)‘𝐾))
262	9, 261	eqtrd 2776	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ₀) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe₁‘𝑂)‘𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3403 Vcvv 3440 ⦋csb 3841 ifcif 4470 class class class wbr 5086 ↦ cmpt 5169 ‘cfv 6465 (class class class)co 7316 ∈ cmpo 7318 ↑_m cmap 8664 Fincfn 8782 finSupp cfsupp 9204 ℝcr 10949 0cc0 10950 < clt 11088 ≤ cle 11089 ℕ₀cn0 12312 ...cfz 13318 Basecbs 16986 Scalarcsca 17039 ·_𝑠 cvsca 17040 0_gc0g 17224 Σ_g cgsu 17225 Mndcmnd 18459 ._gcmg 18773 CMndccmn 19458 mulGrpcmgp 19792 Ringcrg 19855 LModclmod 20203 var₁cv1 21427 Poly₁cpl1 21428 coe₁cco1 21429 Mat cmat 21634 decompPMat cdecpmat 21991

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5223 ax-sep 5237 ax-nul 5244 ax-pow 5302 ax-pr 5366 ax-un 7629 ax-cnex 11006 ax-resscn 11007 ax-1cn 11008 ax-icn 11009 ax-addcl 11010 ax-addrcl 11011 ax-mulcl 11012 ax-mulrcl 11013 ax-mulcom 11014 ax-addass 11015 ax-mulass 11016 ax-distr 11017 ax-i2m1 11018 ax-1ne0 11019 ax-1rid 11020 ax-rnegex 11021 ax-rrecex 11022 ax-cnre 11023 ax-pre-lttri 11024 ax-pre-lttrn 11025 ax-pre-ltadd 11026 ax-pre-mulgt0 11027

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3442 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4471 df-pw 4546 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-ot 4579 df-uni 4850 df-int 4892 df-iun 4938 df-iin 4939 df-br 5087 df-opab 5149 df-mpt 5170 df-tr 5204 df-id 5506 df-eprel 5512 df-po 5520 df-so 5521 df-fr 5562 df-se 5563 df-we 5564 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-pred 6224 df-ord 6291 df-on 6292 df-lim 6293 df-suc 6294 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-f1 6470 df-fo 6471 df-f1o 6472 df-fv 6473 df-isom 6474 df-riota 7273 df-ov 7319 df-oprab 7320 df-mpo 7321 df-of 7574 df-ofr 7575 df-om 7759 df-1st 7877 df-2nd 7878 df-supp 8026 df-frecs 8145 df-wrecs 8176 df-recs 8250 df-rdg 8289 df-1o 8345 df-er 8547 df-map 8666 df-pm 8667 df-ixp 8735 df-en 8783 df-dom 8784 df-sdom 8785 df-fin 8786 df-fsupp 9205 df-sup 9277 df-oi 9345 df-card 9774 df-pnf 11090 df-mnf 11091 df-xr 11092 df-ltxr 11093 df-le 11094 df-sub 11286 df-neg 11287 df-nn 12053 df-2 12115 df-3 12116 df-4 12117 df-5 12118 df-6 12119 df-7 12120 df-8 12121 df-9 12122 df-n0 12313 df-z 12399 df-dec 12517 df-uz 12662 df-fz 13319 df-fzo 13462 df-seq 13801 df-hash 14124 df-struct 16922 df-sets 16939 df-slot 16957 df-ndx 16969 df-base 16987 df-ress 17016 df-plusg 17049 df-mulr 17050 df-sca 17052 df-vsca 17053 df-ip 17054 df-tset 17055 df-ple 17056 df-ds 17058 df-hom 17060 df-cco 17061 df-0g 17226 df-gsum 17227 df-prds 17232 df-pws 17234 df-mre 17369 df-mrc 17370 df-acs 17372 df-mgm 18400 df-sgrp 18449 df-mnd 18460 df-mhm 18504 df-submnd 18505 df-grp 18653 df-minusg 18654 df-sbg 18655 df-mulg 18774 df-subg 18825 df-ghm 18905 df-cntz 18996 df-cmn 19460 df-abl 19461 df-mgp 19793 df-ur 19810 df-ring 19857 df-subrg 20101 df-lmod 20205 df-lss 20274 df-sra 20514 df-rgmod 20515 df-dsmm 21019 df-frlm 21034 df-psr 21192 df-mvr 21193 df-mpl 21194 df-opsr 21196 df-psr1 21431 df-vr1 21432 df-ply1 21433 df-coe1 21434 df-mat 21635 df-decpmat 21992

This theorem is referenced by: mp2pm2mplem5 22039 mp2pm2mp 22040

W3C validator