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 ⊢ A = N Mat R
mp2pm2mp.q ⊢ Q = Poly 1 ⁡ A
mp2pm2mp.l ⊢ L = Base Q
mp2pm2mp.m ⊢ · ˙ = ⋅ P
mp2pm2mp.e ⊢ E = ⋅ mulGrp P
mp2pm2mp.y ⊢ Y = var 1 ⁡ R
mp2pm2mp.i ⊢ I = p ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y
Assertion mp2pm2mplem1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ O ∈ L → I ⁡ O = i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y

Proof

Step Hyp Ref Expression
1 mp2pm2mp.a ⊢ A = N Mat R
2 mp2pm2mp.q ⊢ Q = Poly 1 ⁡ A
3 mp2pm2mp.l ⊢ L = Base Q
4 mp2pm2mp.m ⊢ · ˙ = ⋅ P
5 mp2pm2mp.e ⊢ E = ⋅ mulGrp P
6 mp2pm2mp.y ⊢ Y = var 1 ⁡ R
7 mp2pm2mp.i ⊢ I = p ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y
8 fveq2 ⊢ p = O → coe 1 ⁡ p = coe 1 ⁡ O
9 8 fveq1d ⊢ p = O → coe 1 ⁡ p ⁡ k = coe 1 ⁡ O ⁡ k
10 9 oveqd ⊢ p = O → i coe 1 ⁡ p ⁡ k j = i coe 1 ⁡ O ⁡ k j
11 10 oveq1d ⊢ p = O → i coe 1 ⁡ p ⁡ k j · ˙ k E Y = i coe 1 ⁡ O ⁡ k j · ˙ k E Y
12 11 mpteq2dv ⊢ p = O → k ∈ ℕ 0 ⟼ i coe 1 ⁡ p ⁡ k j · ˙ k E Y = k ∈ ℕ 0 ⟼ i coe 1 ⁡ O ⁡ k j · ˙ k E Y
13 12 oveq2d ⊢ p = O → ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y = ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y
14 13 mpoeq3dv ⊢ p = O → i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y = i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y
15 simp3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ O ∈ L → O ∈ L
16 simp1 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ O ∈ L → N ∈ Fin
17 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y ∈ V
18 16 16 17 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring ∧ O ∈ L → i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y ∈ V
19 7 14 15 18 fvmptd3 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ O ∈ L → I ⁡ O = i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y