Theorem mp2pm2mplem4

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

	Ref	Expression
Hypotheses	mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mp2pm2mp.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	mp2pm2mp.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mp2pm2mp.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mp2pm2mp.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
	mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
	mp2pm2mplem2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion	mp2pm2mplem4	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mp2pm2mp.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3		mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mp2pm2mp.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		mp2pm2mp.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		mp2pm2mp.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
7		mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
8		mp2pm2mplem2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
9	1 2 3 4 5 6 7 8	mp2pm2mplem3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) )
10		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
12	8	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13	12	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ Ring )
14		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
15	13 14	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ CMnd )
16	15	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → 𝑃 ∈ CMnd )
17	16	3ad2ant1	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ CMnd )
18		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ Ring )
19	18	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → 𝑅 ∈ Ring )
20	19	3ad2ant1	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
21	20	adantr	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
22		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
24		simpl2	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑖 ∈ 𝑁 )
25		simpl3	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑗 ∈ 𝑁 )
26		simpl3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑂 ∈ 𝐿 )
27	26	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → 𝑂 ∈ 𝐿 )
28	27	3ad2ant1	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑂 ∈ 𝐿 )
29		eqid	⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
30	29 3 2 23	coe1fvalcl	⊢ ( ( 𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
31	28 30	sylan	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
32	1 22 23 24 25 31	matecld	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
33		simpr	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
34		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
35	22 8 6 4 34 5 10	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
36	21 32 33 35	syl3anc	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
37	36	ralrimiva	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
38		simp1lr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑠 ∈ ℕ0 )
39		oveq	⊢ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) = ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) )
40	39	oveq1d	⊢ ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) )
41		3simpa	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
42	41	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
43		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
44	1 43	mat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
45	42 44	syl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0g ‘ 𝐴 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
46		eqidd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑎 = 𝑖 ∧ 𝑏 = 𝑗 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
47		simprl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
48		simprr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
49		fvexd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
50	45 46 47 48 49	ovmpod	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) = ( 0g ‘ 𝑅 ) )
51	50	adantr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) = ( 0g ‘ 𝑅 ) )
52	51	oveq1d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( ( 0g ‘ 𝑅 ) · ( 𝑥 𝐸 𝑌 ) ) )
53	18	ad3antrrr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → 𝑅 ∈ Ring )
54	8	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
55	53 54	syl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
56	55	fveq2d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
57	56	oveq1d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 0g ‘ 𝑅 ) · ( 𝑥 𝐸 𝑌 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑥 𝐸 𝑌 ) ) )
58	8	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
59	58	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ LMod )
60	59	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → 𝑃 ∈ LMod )
61		simpr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
62	8 6 34 5 10	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
63	53 61 62	syl2anc	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
64		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
65		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
66	10 64 4 65 11	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) )
67	60 63 66	syl2anc	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) )
68	52 57 67	3eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) )
69	68	adantr	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) → ( ( 𝑖 ( 0g ‘ 𝐴 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) )
70	40 69	sylan9eqr	⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑠 < 𝑥 ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) )
71	70	exp31	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑠 < 𝑥 → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ) )
72	71	a2d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ) )
73	72	ralimdva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ) )
74	73	impancom	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ) )
75	74	3impib	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) )
76		breq2	⊢ ( 𝑘 = 𝑥 → ( 𝑠 < 𝑘 ↔ 𝑠 < 𝑥 ) )
77		fveq2	⊢ ( 𝑘 = 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) )
78	77	oveqd	⊢ ( 𝑘 = 𝑥 → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) )
79		oveq1	⊢ ( 𝑘 = 𝑥 → ( 𝑘 𝐸 𝑌 ) = ( 𝑥 𝐸 𝑌 ) )
80	78 79	oveq12d	⊢ ( 𝑘 = 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) )
81	80	eqeq1d	⊢ ( 𝑘 = 𝑥 → ( ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ↔ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) )
82	76 81	imbi12d	⊢ ( 𝑘 = 𝑥 → ( ( 𝑠 < 𝑘 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ( 𝑠 < 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ) )
83	82	cbvralvw	⊢ ( ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) 𝑗 ) · ( 𝑥 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) )
84	75 83	sylibr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( 0g ‘ 𝑃 ) ) )
85	10 11 17 37 38 84	gsummptnn0fz	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
86	85	fveq2d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
87	86	fveq1d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) )
88		simpllr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → 𝐾 ∈ ℕ0 )
89	88	3ad2ant1	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐾 ∈ ℕ0 )
90	36	expcom	⊢ ( 𝑘 ∈ ℕ0 → ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) ) )
91		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝑘 ∈ ℕ0 )
92	90 91	syl11	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) ) )
93	92	ralrimiv	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
94		fzfid	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 0 ... 𝑠 ) ∈ Fin )
95	8 10 20 89 93 94	coe1fzgsumd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) ) )
96	87 95	eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) ) )
97	96	mpoeq3dva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) ) ) )
98	18	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
99	98	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
100		simpl2	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑖 ∈ 𝑁 )
101		simpl3	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑗 ∈ 𝑁 )
102	26	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑂 ∈ 𝐿 )
103	102 91 30	syl2an	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
104	1 22 23 100 101 103	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
105	91	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑘 ∈ ℕ0 )
106	43 22 8 6 4 34 5	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) )
107	99 104 105 106	syl3anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) )
108		eqeq1	⊢ ( 𝑙 = 𝐾 → ( 𝑙 = 𝑘 ↔ 𝐾 = 𝑘 ) )
109	108	ifbid	⊢ ( 𝑙 = 𝐾 → if ( 𝑙 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
110	109	adantl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) ∧ 𝑙 = 𝐾 ) → if ( 𝑙 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
111		simpl1r	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐾 ∈ ℕ0 )
112		ovex	⊢ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ V
113		fvex	⊢ ( 0g ‘ 𝑅 ) ∈ V
114	112 113	ifex	⊢ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ∈ V
115	114	a1i	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
116	107 110 111 115	fvmptd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) = if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
117	116	mpteq2dva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) )
118	117	oveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) )
119	118	mpoeq3dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) )
120	119	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ‘ 𝐾 ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) )
121		breq2	⊢ ( 𝑥 = 𝐾 → ( 𝑠 < 𝑥 ↔ 𝑠 < 𝐾 ) )
122		fveqeq2	⊢ ( 𝑥 = 𝐾 → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ↔ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) )
123	121 122	imbi12d	⊢ ( 𝑥 = 𝐾 → ( ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ↔ ( 𝑠 < 𝐾 → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ) )
124	123	rspcva	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑠 < 𝐾 → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) )
125	1 43	mat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
126	125	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝐴 ) )
127	126	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝐴 ) )
128	127	ad3antlr	⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝐴 ) )
129		elfz2nn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) )
130		nn0re	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
131	130	ad2antrr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
132		nn0re	⊢ ( 𝑠 ∈ ℕ0 → 𝑠 ∈ ℝ )
133	132	ad2antlr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑠 ∈ ℝ )
134		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
135	134	adantl	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℝ )
136		lelttr	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾 ) → 𝑘 < 𝐾 ) )
137	131 133 135 136	syl3anc	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾 ) → 𝑘 < 𝐾 ) )
138		animorr	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 < 𝐾 ) → ( 𝐾 < 𝑘 ∨ 𝑘 < 𝐾 ) )
139		df-ne	⊢ ( 𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘 )
140	130	adantr	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
141		lttri2	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐾 ≠ 𝑘 ↔ ( 𝐾 < 𝑘 ∨ 𝑘 < 𝐾 ) ) )
142	134 140 141	syl2anr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ≠ 𝑘 ↔ ( 𝐾 < 𝑘 ∨ 𝑘 < 𝐾 ) ) )
143	142	adantr	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 < 𝐾 ) → ( 𝐾 ≠ 𝑘 ↔ ( 𝐾 < 𝑘 ∨ 𝑘 < 𝐾 ) ) )
144	139 143	bitr3id	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 < 𝐾 ) → ( ¬ 𝐾 = 𝑘 ↔ ( 𝐾 < 𝑘 ∨ 𝑘 < 𝐾 ) ) )
145	138 144	mpbird	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 < 𝐾 ) → ¬ 𝐾 = 𝑘 )
146	145	ex	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑘 < 𝐾 → ¬ 𝐾 = 𝑘 ) )
147	137 146	syld	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾 ) → ¬ 𝐾 = 𝑘 ) )
148	147	exp4b	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐾 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐾 → ¬ 𝐾 = 𝑘 ) ) ) )
149	148	com24	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑠 < 𝐾 → ( 𝑘 ≤ 𝑠 → ( 𝐾 ∈ ℕ0 → ¬ 𝐾 = 𝑘 ) ) ) )
150	149	expimpd	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝑘 ≤ 𝑠 → ( 𝐾 ∈ ℕ0 → ¬ 𝐾 = 𝑘 ) ) ) )
151	150	com23	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝐾 ∈ ℕ0 → ¬ 𝐾 = 𝑘 ) ) ) )
152	151	imp	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝐾 ∈ ℕ0 → ¬ 𝐾 = 𝑘 ) ) )
153	152	3adant2	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝐾 ∈ ℕ0 → ¬ 𝐾 = 𝑘 ) ) )
154	129 153	sylbi	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝐾 ∈ ℕ0 → ¬ 𝐾 = 𝑘 ) ) )
155	154	com13	⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐾 = 𝑘 ) ) )
156	155	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐾 = 𝑘 ) ) )
157	156	imp	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐾 = 𝑘 ) )
158	157	adantr	⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐾 = 𝑘 ) )
159	158	3ad2ant1	⊢ ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐾 = 𝑘 ) )
160	159	imp	⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ¬ 𝐾 = 𝑘 )
161	160	iffalsed	⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
162	161	mpteq2dva	⊢ ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 0g ‘ 𝑅 ) ) )
163	162	oveq2d	⊢ ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 0g ‘ 𝑅 ) ) ) )
164		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
165	164	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑅 ∈ Mnd )
166		ovex	⊢ ( 0 ... 𝑠 ) ∈ V
167	43	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑠 ) ∈ V ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
168	165 166 167	sylancl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
169	168	ad3antlr	⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
170	169	3ad2ant1	⊢ ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
171	163 170	eqtrd	⊢ ( ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝑅 ) )
172	171	mpoeq3dva	⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
173		simpr	⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) )
174	128 172 173	3eqtr4d	⊢ ( ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
175	174	ex	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾 ) ) → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) )
176	175	expr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ 𝑠 ∈ ℕ0 ) → ( 𝑠 < 𝐾 → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) )
177	176	a2d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ) ∧ 𝑠 ∈ ℕ0 ) → ( ( 𝑠 < 𝐾 → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) )
178	177	exp31	⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑠 ∈ ℕ0 → ( ( 𝑠 < 𝐾 → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) ) )
179	178	com14	⊢ ( ( 𝑠 < 𝐾 → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) = ( 0g ‘ 𝐴 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑠 ∈ ℕ0 → ( 𝐾 ∈ ℕ0 → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) ) )
180	124 179	syl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑠 ∈ ℕ0 → ( 𝐾 ∈ ℕ0 → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) ) )
181	180	ex	⊢ ( 𝐾 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑠 ∈ ℕ0 → ( 𝐾 ∈ ℕ0 → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) ) ) )
182	181	com25	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ∈ ℕ0 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) ) ) )
183	182	pm2.43i	⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) ) )
184	183	impcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) ) ) )
185	184	imp31	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑠 < 𝐾 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) )
186	185	com12	⊢ ( 𝑠 < 𝐾 → ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) )
187	165	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → 𝑅 ∈ Mnd )
188	187	adantl	⊢ ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) → 𝑅 ∈ Mnd )
189	188	3ad2ant1	⊢ ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Mnd )
190		ovexd	⊢ ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 0 ... 𝑠 ) ∈ V )
191		lenlt	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾 ) )
192	134 132 191	syl2an	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾 ) )
193		simpll	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑠 ) → 𝐾 ∈ ℕ0 )
194		simplr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑠 ) → 𝑠 ∈ ℕ0 )
195		simpr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑠 ) → 𝐾 ≤ 𝑠 )
196		elfz2nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑠 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝐾 ≤ 𝑠 ) )
197	193 194 195 196	syl3anbrc	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑠 ) → 𝐾 ∈ ( 0 ... 𝑠 ) )
198	197	ex	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑠 → 𝐾 ∈ ( 0 ... 𝑠 ) ) )
199	192 198	sylbird	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐾 → 𝐾 ∈ ( 0 ... 𝑠 ) ) )
200	199	ad4ant23	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( ¬ 𝑠 < 𝐾 → 𝐾 ∈ ( 0 ... 𝑠 ) ) )
201	200	impcom	⊢ ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) → 𝐾 ∈ ( 0 ... 𝑠 ) )
202	201	3ad2ant1	⊢ ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐾 ∈ ( 0 ... 𝑠 ) )
203		eqcom	⊢ ( 𝐾 = 𝑘 ↔ 𝑘 = 𝐾 )
204		ifbi	⊢ ( ( 𝐾 = 𝑘 ↔ 𝑘 = 𝐾 ) → if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑘 = 𝐾 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
205	203 204	ax-mp	⊢ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑘 = 𝐾 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) )
206	205	mpteq2i	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝑘 = 𝐾 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) )
207		simpl2	⊢ ( ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑖 ∈ 𝑁 )
208		simpl3	⊢ ( ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑗 ∈ 𝑁 )
209	27	adantl	⊢ ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) → 𝑂 ∈ 𝐿 )
210	209	3ad2ant1	⊢ ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑂 ∈ 𝐿 )
211	210 30	sylan	⊢ ( ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
212	1 22 23 207 208 211	matecld	⊢ ( ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
213	91 212	sylan2	⊢ ( ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
214	213	ralrimiva	⊢ ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
215	43 189 190 202 206 214	gsummpt1n0	⊢ ( ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) = ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) )
216	215	mpoeq3dva	⊢ ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) )
217		csbov	⊢ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ⦋ 𝐾 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 )
218		csbfv	⊢ ⦋ 𝐾 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 )
219	218	a1i	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
220	219	oveqd	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑖 ⦋ 𝐾 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) )
221	217 220	eqtrid	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) )
222	221	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) )
223	222	mpoeq3dv	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) ) )
224		oveq12	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) = ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) )
225	224	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) = ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) )
226		simprl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
227		simprr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
228		ovexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) ∈ V )
229	223 225 226 227 228	ovmpod	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) 𝑏 ) = ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) )
230	229	ralrimivva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) 𝑏 ) = ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) )
231		simpl1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ Fin )
232	218	oveqi	⊢ ( 𝑖 ⦋ 𝐾 / 𝑘 ⦌ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 )
233	217 232	eqtri	⊢ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 )
234		simp2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
235		simp3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
236	29 3 2 23	coe1fvalcl	⊢ ( ( 𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
237	236	3ad2antl3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
238	237	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝐴 ) )
239	1 22 23 234 235 238	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
240	233 239	eqeltrid	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
241	1 22 23 231 18 240	matbas2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) ∈ ( Base ‘ 𝐴 ) )
242	1 23	eqmat	⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) 𝑏 ) = ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) ) )
243	241 237 242	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) 𝑏 ) = ( 𝑎 ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) 𝑏 ) ) )
244	230 243	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
245	244	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
246	245	adantl	⊢ ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ⦋ 𝐾 / 𝑘 ⦌ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
247	216 246	eqtrd	⊢ ( ( ¬ 𝑠 < 𝐾 ∧ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
248	247	ex	⊢ ( ¬ 𝑠 < 𝐾 → ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) ) )
249	186 248	pm2.61i	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐾 = 𝑘 , ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
250	97 120 249	3eqtrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
251		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
252	29 3 2 251	coe1sfi	⊢ ( 𝑂 ∈ 𝐿 → ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) )
253	26 252	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) )
254	29 3 2 251 23	coe1fsupp	⊢ ( 𝑂 ∈ 𝐿 → ( coe1 ‘ 𝑂 ) ∈ { 𝑥 ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∣ 𝑥 finSupp ( 0g ‘ 𝐴 ) } )
255		elrabi	⊢ ( ( coe1 ‘ 𝑂 ) ∈ { 𝑥 ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∣ 𝑥 finSupp ( 0g ‘ 𝐴 ) } → ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) )
256	26 254 255	3syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) )
257		fvex	⊢ ( 0g ‘ 𝐴 ) ∈ V
258		fsuppmapnn0ub	⊢ ( ( ( coe1 ‘ 𝑂 ) ∈ ( ( Base ‘ 𝐴 ) ↑m ℕ0 ) ∧ ( 0g ‘ 𝐴 ) ∈ V ) → ( ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
259	256 257 258	sylancl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
260	253 259	mpd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( coe1 ‘ 𝑂 ) ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) )
261	250 260	r19.29a	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )
262	9 261	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝐾 ) )