Step | Hyp | Ref
| Expression |
1 | | nn0ex 12424 |
. . 3
β’
β0 β V |
2 | 1 | a1i 11 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β β0 β
V) |
3 | | mp2pm2mp.a |
. . . . 5
β’ π΄ = (π Mat π
) |
4 | 3 | matring 21808 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
5 | | mp2pm2mp.q |
. . . . 5
β’ π = (Poly1βπ΄) |
6 | 5 | ply1lmod 21639 |
. . . 4
β’ (π΄ β Ring β π β LMod) |
7 | 4, 6 | syl 17 |
. . 3
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
8 | 7 | 3adant3 1133 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β π β LMod) |
9 | 4 | 3adant3 1133 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β π΄ β Ring) |
10 | 5 | ply1sca 21640 |
. . 3
β’ (π΄ β Ring β π΄ = (Scalarβπ)) |
11 | 9, 10 | syl 17 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β π΄ = (Scalarβπ)) |
12 | | mp2pm2mp.l |
. 2
β’ πΏ = (Baseβπ) |
13 | | simpl2 1193 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β πΏ) β§ π β β0) β π
β Ring) |
14 | | mp2pm2mplem2.p |
. . . . 5
β’ π = (Poly1βπ
) |
15 | | mp2pm2mp.m |
. . . . 5
β’ Β· = (
Β·π βπ) |
16 | | mp2pm2mp.e |
. . . . 5
β’ πΈ =
(.gβ(mulGrpβπ)) |
17 | | mp2pm2mp.y |
. . . . 5
β’ π = (var1βπ
) |
18 | | mp2pm2mp.i |
. . . . 5
β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) |
19 | | eqid 2733 |
. . . . 5
β’ (π Mat π) = (π Mat π) |
20 | | eqid 2733 |
. . . . 5
β’
(Baseβ(π Mat
π)) = (Baseβ(π Mat π)) |
21 | 3, 5, 12, 14, 15, 16, 17, 18, 19, 20 | mply1topmatcl 22170 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β (πΌβπ) β (Baseβ(π Mat π))) |
22 | 21 | adantr 482 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β πΏ) β§ π β β0) β (πΌβπ) β (Baseβ(π Mat π))) |
23 | | simpr 486 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β πΏ) β§ π β β0) β π β
β0) |
24 | | eqid 2733 |
. . . 4
β’
(Baseβπ΄) =
(Baseβπ΄) |
25 | 14, 19, 20, 3, 24 | decpmatcl 22132 |
. . 3
β’ ((π
β Ring β§ (πΌβπ) β (Baseβ(π Mat π)) β§ π β β0) β ((πΌβπ) decompPMat π) β (Baseβπ΄)) |
26 | 13, 22, 23, 25 | syl3anc 1372 |
. 2
β’ (((π β Fin β§ π
β Ring β§ π β πΏ) β§ π β β0) β ((πΌβπ) decompPMat π) β (Baseβπ΄)) |
27 | | mp2pm2mplem5.x |
. . . 4
β’ π = (var1βπ΄) |
28 | | eqid 2733 |
. . . 4
β’
(mulGrpβπ) =
(mulGrpβπ) |
29 | | mp2pm2mplem5.e |
. . . 4
β’ β =
(.gβ(mulGrpβπ)) |
30 | 5, 27, 28, 29, 12 | ply1moncl 21658 |
. . 3
β’ ((π΄ β Ring β§ π β β0)
β (π β π) β πΏ) |
31 | 9, 30 | sylan 581 |
. 2
β’ (((π β Fin β§ π
β Ring β§ π β πΏ) β§ π β β0) β (π β π) β πΏ) |
32 | | eqid 2733 |
. 2
β’
(0gβπ) = (0gβπ) |
33 | | eqid 2733 |
. 2
β’
(0gβπ΄) = (0gβπ΄) |
34 | | mp2pm2mplem5.m |
. 2
β’ β = (
Β·π βπ) |
35 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = π β ((coe1βπ)βπ) = ((coe1βπ)βπ)) |
36 | 35 | oveqd 7375 |
. . . . . . . . . . . 12
β’ (π = π β (π((coe1βπ)βπ)π) = (π((coe1βπ)βπ)π)) |
37 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π = π β (ππΈπ) = (ππΈπ)) |
38 | 36, 37 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (π = π β ((π((coe1βπ)βπ)π) Β· (ππΈπ)) = ((π((coe1βπ)βπ)π) Β· (ππΈπ))) |
39 | 38 | cbvmptv 5219 |
. . . . . . . . . 10
β’ (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))) = (π β β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))) |
40 | 39 | oveq2i 7369 |
. . . . . . . . 9
β’ (π Ξ£g
(π β
β0 β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))) = (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))) |
41 | 40 | a1i 11 |
. . . . . . . 8
β’ ((π β π β§ π β π) β (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))) = (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))))) |
42 | 41 | mpoeq3ia 7436 |
. . . . . . 7
β’ (π β π, π β π β¦ (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))))) = (π β π, π β π β¦ (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ))))) |
43 | 42 | mpteq2i 5211 |
. . . . . 6
β’ (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) |
44 | 18, 43 | eqtri 2761 |
. . . . 5
β’ πΌ = (π β πΏ β¦ (π β π, π β π β¦ (π Ξ£g (π β β0
β¦ ((π((coe1βπ)βπ)π) Β· (ππΈπ)))))) |
45 | 3, 5, 12, 15, 16, 17, 44, 14 | mp2pm2mplem4 22174 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β πΏ) β§ π β β0) β ((πΌβπ) decompPMat π) = ((coe1βπ)βπ)) |
46 | 45 | mpteq2dva 5206 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β (π β β0 β¦ ((πΌβπ) decompPMat π)) = (π β β0 β¦
((coe1βπ)βπ))) |
47 | 5, 12, 33 | mptcoe1fsupp 21602 |
. . . 4
β’ ((π΄ β Ring β§ π β πΏ) β (π β β0 β¦
((coe1βπ)βπ)) finSupp (0gβπ΄)) |
48 | 4, 47 | stoic3 1779 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β (π β β0 β¦
((coe1βπ)βπ)) finSupp (0gβπ΄)) |
49 | 46, 48 | eqbrtrd 5128 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β (π β β0 β¦ ((πΌβπ) decompPMat π)) finSupp (0gβπ΄)) |
50 | 2, 8, 11, 12, 26, 31, 32, 33, 34, 49 | mptscmfsupp0 20402 |
1
β’ ((π β Fin β§ π
β Ring β§ π β πΏ) β (π β β0 β¦ (((πΌβπ) decompPMat π) β (π β π))) finSupp (0gβπ)) |