| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mp2pm2mp.a | . . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 2 |  | mp2pm2mp.q | . . . 4
⊢ 𝑄 = (Poly1‘𝐴) | 
| 3 |  | mp2pm2mp.l | . . . 4
⊢ 𝐿 = (Base‘𝑄) | 
| 4 |  | mp2pm2mplem2.p | . . . 4
⊢ 𝑃 = (Poly1‘𝑅) | 
| 5 |  | mp2pm2mp.m | . . . 4
⊢  · = (
·𝑠 ‘𝑃) | 
| 6 |  | mp2pm2mp.e | . . . 4
⊢ 𝐸 =
(.g‘(mulGrp‘𝑃)) | 
| 7 |  | mp2pm2mp.y | . . . 4
⊢ 𝑌 = (var1‘𝑅) | 
| 8 |  | mp2pm2mp.i | . . . 4
⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) | 
| 9 |  | eqid 2736 | . . . 4
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃) | 
| 10 |  | eqid 2736 | . . . 4
⊢
(Base‘(𝑁 Mat
𝑃)) = (Base‘(𝑁 Mat 𝑃)) | 
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mply1topmatcl 22812 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) | 
| 12 |  | eqid 2736 | . . . 4
⊢ (
·𝑠 ‘𝑄) = ( ·𝑠
‘𝑄) | 
| 13 |  | eqid 2736 | . . . 4
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) | 
| 14 |  | eqid 2736 | . . . 4
⊢
(var1‘𝐴) = (var1‘𝐴) | 
| 15 |  | mp2pm2mp.t | . . . 4
⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) | 
| 16 | 4, 9, 10, 12, 13, 14, 1, 2, 15 | pm2mpfval 22803 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) → (𝑇‘(𝐼‘𝑂)) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) | 
| 17 | 11, 16 | syld3an3 1410 | . 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑇‘(𝐼‘𝑂)) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) | 
| 18 | 1 | matring 22450 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) | 
| 19 | 18 | 3adant3 1132 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝐴 ∈ Ring) | 
| 20 |  | eqid 2736 | . . . . 5
⊢
(0g‘𝑄) = (0g‘𝑄) | 
| 21 | 2 | ply1ring 22250 | . . . . . . 7
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) | 
| 22 |  | ringcmn 20280 | . . . . . . 7
⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) | 
| 23 | 18, 21, 22 | 3syl 18 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) | 
| 24 | 23 | 3adant3 1132 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑄 ∈ CMnd) | 
| 25 |  | nn0ex 12534 | . . . . . 6
⊢
ℕ0 ∈ V | 
| 26 | 25 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → ℕ0 ∈
V) | 
| 27 | 19 | adantr 480 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring) | 
| 28 |  | simpl2 1192 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) | 
| 29 | 11 | adantr 480 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) | 
| 30 |  | simpr 484 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) | 
| 31 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘𝐴) | 
| 32 | 4, 9, 10, 1, 31 | decpmatcl 22774 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃)) ∧ 𝑛 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑛) ∈ (Base‘𝐴)) | 
| 33 | 28, 29, 30, 32 | syl3anc 1372 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑛) ∈ (Base‘𝐴)) | 
| 34 |  | eqid 2736 | . . . . . . . 8
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) | 
| 35 | 31, 2, 14, 12, 34, 13, 3 | ply1tmcl 22276 | . . . . . . 7
⊢ ((𝐴 ∈ Ring ∧ ((𝐼‘𝑂) decompPMat 𝑛) ∈ (Base‘𝐴) ∧ 𝑛 ∈ ℕ0) → (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ 𝐿) | 
| 36 | 27, 33, 30, 35 | syl3anc 1372 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ 𝐿) | 
| 37 | 36 | fmpttd 7134 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶𝐿) | 
| 38 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((coe1‘𝑝)‘𝑘) = ((coe1‘𝑝)‘𝑛)) | 
| 39 | 38 | oveqd 7449 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑖((coe1‘𝑝)‘𝑘)𝑗) = (𝑖((coe1‘𝑝)‘𝑛)𝑗)) | 
| 40 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑘𝐸𝑌) = (𝑛𝐸𝑌)) | 
| 41 | 39, 40 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))) | 
| 42 | 41 | cbvmptv 5254 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑛 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))) | 
| 43 | 42 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑛 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌)))) | 
| 44 | 43 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))))) | 
| 45 | 44 | mpoeq3ia 7512 | . . . . . . . 8
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))))) | 
| 46 | 45 | mpteq2i 5246 | . . . . . . 7
⊢ (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌)))))) | 
| 47 | 8, 46 | eqtri 2764 | . . . . . 6
⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌)))))) | 
| 48 | 1, 2, 3, 5, 6, 7, 47, 4, 12, 13, 14 | mp2pm2mplem5 22817 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) | 
| 49 | 3, 20, 24, 26, 37, 48 | gsumcl 19934 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ 𝐿) | 
| 50 |  | simp3 1138 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑂 ∈ 𝐿) | 
| 51 | 19, 49, 50 | 3jca 1128 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐴 ∈ Ring ∧ (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ 𝐿 ∧ 𝑂 ∈ 𝐿)) | 
| 52 | 1, 2, 3, 5, 6, 7, 8, 4 | mp2pm2mplem4 22816 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑛) = ((coe1‘𝑂)‘𝑛)) | 
| 53 | 52 | oveq1d 7447 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) =
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) | 
| 54 | 53 | adantlr 715 | . . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) =
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) | 
| 55 | 54 | mpteq2dva 5241 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) | 
| 56 | 55 | oveq2d 7448 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) | 
| 57 | 56 | fveq2d 6909 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) | 
| 58 | 57 | fveq1d 6907 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘(𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)) | 
| 59 | 19, 50 | jca 511 | . . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿)) | 
| 60 | 59 | adantr 480 | . . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿)) | 
| 61 |  | eqid 2736 | . . . . . . . . . 10
⊢
(coe1‘𝑂) = (coe1‘𝑂) | 
| 62 | 2, 14, 3, 12, 34, 13, 61 | ply1coe 22303 | . . . . . . . . 9
⊢ ((𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑂 = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) | 
| 63 | 60, 62 | syl 17 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → 𝑂 = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) | 
| 64 | 63 | eqcomd 2742 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = 𝑂) | 
| 65 | 64 | fveq2d 6909 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘𝑂)) | 
| 66 | 65 | fveq1d 6907 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙)) | 
| 67 | 58, 66 | eqtrd 2776 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙)) | 
| 68 | 67 | ralrimiva 3145 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → ∀𝑙 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙)) | 
| 69 |  | eqid 2736 | . . . 4
⊢
(coe1‘(𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) | 
| 70 | 2, 3, 69, 61 | eqcoe1ply1eq 22304 | . . 3
⊢ ((𝐴 ∈ Ring ∧ (𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ 𝐿 ∧ 𝑂 ∈ 𝐿) → (∀𝑙 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = 𝑂)) | 
| 71 | 51, 68, 70 | sylc 65 | . 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = 𝑂) | 
| 72 | 17, 71 | eqtrd 2776 | 1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑇‘(𝐼‘𝑂)) = 𝑂) |