mp2pm2mplem3

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

	Ref	Expression
Hypotheses	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	mp2pm2mplem3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mp2pm2mp.q	⊢ 𝑄 = ( Poly₁ ‘ 𝐴 )
3		mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mp2pm2mp.m	⊢ · = ( ·_𝑠 ‘ 𝑃 )
5		mp2pm2mp.e	⊢ 𝐸 = ( ._g ‘ ( mulGrp ‘ 𝑃 ) )
6		mp2pm2mp.y	⊢ 𝑌 = ( var₁ ‘ 𝑅 )
7		mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
8		mp2pm2mplem2.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
9	1 2 3 4 5 6 7	mp2pm2mplem1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
10	9	oveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) decompPMat 𝐾 ) )
11	10	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) decompPMat 𝐾 ) )
12		eqid	⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
13		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
14	1 2 3 4 5 6 7 8 12 13	mp2pm2mplem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
15	12 13	decpmatval	⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ∧ 𝐾 ∈ ℕ₀ ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) decompPMat 𝐾 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) ) ‘ 𝐾 ) ) )
16	14 15	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) decompPMat 𝐾 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) ) ‘ 𝐾 ) ) )
17		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
18		oveq12	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) )
19	18	oveq1d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) )
20	19	mpteq2dv	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) )
21	20	oveq2d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
22	21	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
23		simp2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
24		simp3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
25		ovexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ∈ V )
26	17 22 23 24 25	ovmpod	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
27	26	fveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( coe₁ ‘ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
28	27	fveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe₁ ‘ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) )
29	28	mpoeq3dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) ) ‘ 𝐾 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) )
30		oveq1	⊢ ( 𝑎 = 𝑖 → ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) = ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) )
31	30	oveq1d	⊢ ( 𝑎 = 𝑖 → ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) )
32	31	mpteq2dv	⊢ ( 𝑎 = 𝑖 → ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) )
33	32	oveq2d	⊢ ( 𝑎 = 𝑖 → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
34	33	fveq2d	⊢ ( 𝑎 = 𝑖 → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
35	34	fveq1d	⊢ ( 𝑎 = 𝑖 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) )
36		simpl	⊢ ( ( 𝑏 = 𝑗 ∧ 𝑘 ∈ ℕ₀ ) → 𝑏 = 𝑗 )
37	36	oveq2d	⊢ ( ( 𝑏 = 𝑗 ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) = ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) )
38	37	oveq1d	⊢ ( ( 𝑏 = 𝑗 ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) )
39	38	mpteq2dva	⊢ ( 𝑏 = 𝑗 → ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) )
40	39	oveq2d	⊢ ( 𝑏 = 𝑗 → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
41	40	fveq2d	⊢ ( 𝑏 = 𝑗 → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
42	41	fveq1d	⊢ ( 𝑏 = 𝑗 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) )
43	35 42	cbvmpov	⊢ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑎 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑏 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) )
44	29 43	eqtrdi	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) 𝑏 ) ) ‘ 𝐾 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) )
45	11 16 44	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐾 ∈ ℕ₀ ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ‘ 𝐾 ) ) )

Metamath Proof Explorer

Theorem mp2pm2mplem3

Proof