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 2610 |
. . . 4
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃) |
10 | | eqid 2610 |
. . . 4
⊢
(Base‘(𝑁 Mat
𝑃)) = (Base‘(𝑁 Mat 𝑃)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mply1topmatcl 20429 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) |
12 | | eqid 2610 |
. . . 4
⊢ (
·𝑠 ‘𝑄) = ( ·𝑠
‘𝑄) |
13 | | eqid 2610 |
. . . 4
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) |
14 | | eqid 2610 |
. . . 4
⊢
(var1‘𝐴) = (var1‘𝐴) |
15 | | mp2pm2mp.t |
. . . 4
⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) |
16 | 4, 9, 10, 12, 13, 14, 1, 2, 15 | pm2mpfval 20420 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) → (𝑇‘(𝐼‘𝑂)) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
17 | 11, 16 | syld3an3 1363 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑇‘(𝐼‘𝑂)) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
18 | 1 | matring 20068 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
19 | 18 | 3adant3 1074 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝐴 ∈ Ring) |
20 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑄) = (0g‘𝑄) |
21 | 2 | ply1ring 19439 |
. . . . . . 7
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
22 | | ringcmn 18404 |
. . . . . . 7
⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) |
23 | 18, 21, 22 | 3syl 18 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) |
24 | 23 | 3adant3 1074 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑄 ∈ CMnd) |
25 | | nn0ex 11175 |
. . . . . 6
⊢
ℕ0 ∈ V |
26 | 25 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → ℕ0 ∈
V) |
27 | 19 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring) |
28 | | simpl2 1058 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) |
29 | 11 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) |
30 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘𝐴) |
32 | 4, 9, 10, 1, 31 | decpmatcl 20391 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃)) ∧ 𝑛 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑛) ∈ (Base‘𝐴)) |
33 | 28, 29, 30, 32 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑛) ∈ (Base‘𝐴)) |
34 | | eqid 2610 |
. . . . . . . 8
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
35 | 31, 2, 14, 12, 34, 13, 3 | ply1tmcl 19463 |
. . . . . . 7
⊢ ((𝐴 ∈ Ring ∧ ((𝐼‘𝑂) decompPMat 𝑛) ∈ (Base‘𝐴) ∧ 𝑛 ∈ ℕ0) → (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ 𝐿) |
36 | 27, 33, 30, 35 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ 𝐿) |
37 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
38 | 36, 37 | fmptd 6292 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶𝐿) |
39 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((coe1‘𝑝)‘𝑘) = ((coe1‘𝑝)‘𝑛)) |
40 | 39 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑖((coe1‘𝑝)‘𝑘)𝑗) = (𝑖((coe1‘𝑝)‘𝑛)𝑗)) |
41 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑘𝐸𝑌) = (𝑛𝐸𝑌)) |
42 | 40, 41 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))) |
43 | 42 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑛 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))) |
44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑛 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌)))) |
45 | 44 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))))) |
46 | 45 | mpt2eq3ia 6618 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌))))) |
47 | 46 | mpteq2i 4669 |
. . . . . . 7
⊢ (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌)))))) |
48 | 8, 47 | eqtri 2632 |
. . . . . 6
⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑛)𝑗) · (𝑛𝐸𝑌)))))) |
49 | 1, 2, 3, 5, 6, 7, 48, 4, 12, 13, 14 | mp2pm2mplem5 20434 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
50 | 3, 20, 24, 26, 38, 49 | gsumcl 18139 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ 𝐿) |
51 | | simp3 1056 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑂 ∈ 𝐿) |
52 | 19, 50, 51 | 3jca 1235 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐴 ∈ Ring ∧ (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ 𝐿 ∧ 𝑂 ∈ 𝐿)) |
53 | 1, 2, 3, 5, 6, 7, 8, 4 | mp2pm2mplem4 20433 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑛) = ((coe1‘𝑂)‘𝑛)) |
54 | 53 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑛 ∈ ℕ0) → (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) =
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
55 | 54 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))) =
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
56 | 55 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) |
57 | 56 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
58 | 57 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
59 | 58 | fveq1d 6105 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘(𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)) |
60 | 19, 51 | jca 553 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿)) |
61 | 60 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿)) |
62 | | eqid 2610 |
. . . . . . . . . 10
⊢
(coe1‘𝑂) = (coe1‘𝑂) |
63 | 2, 14, 3, 12, 34, 13, 62 | ply1coe 19487 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑂 = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
64 | 61, 63 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → 𝑂 = (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
65 | 64 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) → (𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = 𝑂) |
66 | 65 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘𝑂)) |
67 | 66 | fveq1d 6105 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦
(((coe1‘𝑂)‘𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙)) |
68 | 59, 67 | eqtrd 2644 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑙 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙)) |
69 | 68 | ralrimiva 2949 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → ∀𝑙 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙)) |
70 | | eqid 2610 |
. . . 4
⊢
(coe1‘(𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
71 | 2, 3, 70, 62 | eqcoe1ply1eq 19488 |
. . 3
⊢ ((𝐴 ∈ Ring ∧ (𝑄 Σg
(𝑛 ∈
ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ 𝐿 ∧ 𝑂 ∈ 𝐿) → (∀𝑙 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑛 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ((coe1‘𝑂)‘𝑙) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = 𝑂)) |
72 | 52, 69, 71 | sylc 63 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑄 Σg (𝑛 ∈ ℕ0
↦ (((𝐼‘𝑂) decompPMat 𝑛)( ·𝑠
‘𝑄)(𝑛(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = 𝑂) |
73 | 17, 72 | eqtrd 2644 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑇‘(𝐼‘𝑂)) = 𝑂) |