Metamath Proof Explorer

Theorem mp2pm2mplem1

Description: Lemma 1 for mp2pm2mp . (Contributed by AV, 9-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₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
	Assertion	mp2pm2mplem1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_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		fveq2	⊢ ( 𝑝 = 𝑂 → ( coe₁ ‘ 𝑝 ) = ( coe₁ ‘ 𝑂 ) )
9	8	fveq1d	⊢ ( 𝑝 = 𝑂 → ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) = ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) )
10	9	oveqd	⊢ ( 𝑝 = 𝑂 → ( 𝑖 ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) )
11	10	oveq1d	⊢ ( 𝑝 = 𝑂 → ( ( 𝑖 ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) )
12	11	mpteq2dv	⊢ ( 𝑝 = 𝑂 → ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) )
13	12	oveq2d	⊢ ( 𝑝 = 𝑂 → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) )
14	13	mpoeq3dv	⊢ ( 𝑝 = 𝑂 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
15		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑂 ∈ 𝐿 )
16		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑁 ∈ Fin )
17		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ V )
18	16 16 17	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ V )
19	7 14 15 18	fvmptd3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑖 ( ( coe₁ ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )