Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β π β Fin) |
2 | | simplr 768 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β π
β CRing) |
3 | | elrabi 3644 |
. . . . . 6
β’ (π β {π β (Baseβπ΄) β£ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))} β π β (Baseβπ΄)) |
4 | | chpscmat.d |
. . . . . 6
β’ π· = {π β (Baseβπ΄) β£ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))} |
5 | 3, 4 | eleq2s 2856 |
. . . . 5
β’ (π β π· β π β (Baseβπ΄)) |
6 | 5 | 3ad2ant1 1134 |
. . . 4
β’ ((π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ) β π β (Baseβπ΄)) |
7 | 6 | adantl 483 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β π β (Baseβπ΄)) |
8 | | oveq 7368 |
. . . . . . . . . . 11
β’ (π = π β (πππ) = (πππ)) |
9 | 8 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π = π β ((πππ) = if(π = π, π, (0gβπ
)) β (πππ) = if(π = π, π, (0gβπ
)))) |
10 | 9 | 2ralbidv 3213 |
. . . . . . . . 9
β’ (π = π β (βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)) β βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)))) |
11 | 10 | rexbidv 3176 |
. . . . . . . 8
β’ (π = π β (βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)) β βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)))) |
12 | 11 | elrab 3650 |
. . . . . . 7
β’ (π β {π β (Baseβπ΄) β£ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))} β (π β (Baseβπ΄) β§ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)))) |
13 | | ifnefalse 4503 |
. . . . . . . . . . . . . . . 16
β’ (π β π β if(π = π, π, (0gβπ
)) = (0gβπ
)) |
14 | 13 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
β’ (π β π β ((πππ) = if(π = π, π, (0gβπ
)) β (πππ) = (0gβπ
))) |
15 | 14 | biimpcd 249 |
. . . . . . . . . . . . . 14
β’ ((πππ) = if(π = π, π, (0gβπ
)) β (π β π β (πππ) = (0gβπ
))) |
16 | 15 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((((π β
(Baseβπ΄) β§ π β (Baseβπ
)) β§ (π β Fin β§ π
β CRing)) β§ π β π) β§ π β π) β ((πππ) = if(π = π, π, (0gβπ
)) β (π β π β (πππ) = (0gβπ
)))) |
17 | 16 | ralimdva 3165 |
. . . . . . . . . . . 12
β’ ((((π β (Baseβπ΄) β§ π β (Baseβπ
)) β§ (π β Fin β§ π
β CRing)) β§ π β π) β (βπ β π (πππ) = if(π = π, π, (0gβπ
)) β βπ β π (π β π β (πππ) = (0gβπ
)))) |
18 | 17 | ralimdva 3165 |
. . . . . . . . . . 11
β’ (((π β (Baseβπ΄) β§ π β (Baseβπ
)) β§ (π β Fin β§ π
β CRing)) β (βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
)))) |
19 | 18 | ex 414 |
. . . . . . . . . 10
β’ ((π β (Baseβπ΄) β§ π β (Baseβπ
)) β ((π β Fin β§ π
β CRing) β (βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
))))) |
20 | 19 | com23 86 |
. . . . . . . . 9
β’ ((π β (Baseβπ΄) β§ π β (Baseβπ
)) β (βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)) β ((π β Fin β§ π
β CRing) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
))))) |
21 | 20 | rexlimdva 3153 |
. . . . . . . 8
β’ (π β (Baseβπ΄) β (βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
)) β ((π β Fin β§ π
β CRing) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
))))) |
22 | 21 | imp 408 |
. . . . . . 7
β’ ((π β (Baseβπ΄) β§ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))) β ((π β Fin β§ π
β CRing) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
)))) |
23 | 12, 22 | sylbi 216 |
. . . . . 6
β’ (π β {π β (Baseβπ΄) β£ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))} β ((π β Fin β§ π
β CRing) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
)))) |
24 | 23, 4 | eleq2s 2856 |
. . . . 5
β’ (π β π· β ((π β Fin β§ π
β CRing) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
)))) |
25 | 24 | 3ad2ant1 1134 |
. . . 4
β’ ((π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ) β ((π β Fin β§ π
β CRing) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
)))) |
26 | 25 | impcom 409 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β βπ β π βπ β π (π β π β (πππ) = (0gβπ
))) |
27 | | chp0mat.c |
. . . 4
β’ πΆ = (π CharPlyMat π
) |
28 | | chp0mat.p |
. . . 4
β’ π = (Poly1βπ
) |
29 | | chp0mat.a |
. . . 4
β’ π΄ = (π Mat π
) |
30 | | chpscmat.s |
. . . 4
β’ π = (algScβπ) |
31 | | eqid 2737 |
. . . 4
β’
(Baseβπ΄) =
(Baseβπ΄) |
32 | | chp0mat.x |
. . . 4
β’ π = (var1βπ
) |
33 | | eqid 2737 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
34 | | chp0mat.g |
. . . 4
β’ πΊ = (mulGrpβπ) |
35 | | chpscmat.m |
. . . 4
β’ β =
(-gβπ) |
36 | 27, 28, 29, 30, 31, 32, 33, 34, 35 | chpdmat 22206 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β (Baseβπ΄)) β§ βπ β π βπ β π (π β π β (πππ) = (0gβπ
))) β (πΆβπ) = (πΊ Ξ£g (π β π β¦ (π β (πβ(πππ)))))) |
37 | 1, 2, 7, 26, 36 | syl31anc 1374 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (πΆβπ) = (πΊ Ξ£g (π β π β¦ (π β (πβ(πππ)))))) |
38 | | id 22 |
. . . . . . . . . . . 12
β’ (π = π β π = π) |
39 | 38, 38 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β (πππ) = (πππ)) |
40 | 39 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π = π β ((πππ) = πΈ β (πππ) = πΈ)) |
41 | 40 | rspccv 3581 |
. . . . . . . . 9
β’
(βπ β
π (πππ) = πΈ β (π β π β (πππ) = πΈ)) |
42 | 41 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ) β (π β π β (πππ) = πΈ)) |
43 | 42 | adantl 483 |
. . . . . . 7
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (π β π β (πππ) = πΈ)) |
44 | 43 | imp 408 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β§ π β π) β (πππ) = πΈ) |
45 | 44 | fveq2d 6851 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β§ π β π) β (πβ(πππ)) = (πβπΈ)) |
46 | 45 | oveq2d 7378 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β§ π β π) β (π β (πβ(πππ))) = (π β (πβπΈ))) |
47 | 46 | mpteq2dva 5210 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (π β π β¦ (π β (πβ(πππ)))) = (π β π β¦ (π β (πβπΈ)))) |
48 | 47 | oveq2d 7378 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (πΊ Ξ£g (π β π β¦ (π β (πβ(πππ))))) = (πΊ Ξ£g (π β π β¦ (π β (πβπΈ))))) |
49 | 28 | ply1crng 21585 |
. . . . 5
β’ (π
β CRing β π β CRing) |
50 | 34 | crngmgp 19979 |
. . . . 5
β’ (π β CRing β πΊ β CMnd) |
51 | | cmnmnd 19586 |
. . . . 5
β’ (πΊ β CMnd β πΊ β Mnd) |
52 | 49, 50, 51 | 3syl 18 |
. . . 4
β’ (π
β CRing β πΊ β Mnd) |
53 | 52 | ad2antlr 726 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β πΊ β Mnd) |
54 | | crngring 19983 |
. . . . . . . 8
β’ (π
β CRing β π
β Ring) |
55 | 28 | ply1ring 21635 |
. . . . . . . 8
β’ (π
β Ring β π β Ring) |
56 | 54, 55 | syl 17 |
. . . . . . 7
β’ (π
β CRing β π β Ring) |
57 | | ringgrp 19976 |
. . . . . . 7
β’ (π β Ring β π β Grp) |
58 | 56, 57 | syl 17 |
. . . . . 6
β’ (π
β CRing β π β Grp) |
59 | 58 | ad2antlr 726 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β π β Grp) |
60 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
61 | 32, 28, 60 | vr1cl 21604 |
. . . . . . 7
β’ (π
β Ring β π β (Baseβπ)) |
62 | 54, 61 | syl 17 |
. . . . . 6
β’ (π
β CRing β π β (Baseβπ)) |
63 | 62 | ad2antlr 726 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β π β (Baseβπ)) |
64 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β πΌ β π) |
65 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(Scalarβπ) =
(Scalarβπ) |
66 | 56 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π· β§ (π β Fin β§ π
β CRing)) β π β Ring) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β π β Ring) |
68 | 28 | ply1lmod 21639 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β Ring β π β LMod) |
69 | 54, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β CRing β π β LMod) |
70 | 69 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π· β§ (π β Fin β§ π
β CRing)) β π β LMod) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β π β LMod) |
72 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
73 | 30, 65, 67, 71, 72, 60 | asclf 21301 |
. . . . . . . . . . . . . . . 16
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β π:(Baseβ(Scalarβπ))βΆ(Baseβπ)) |
74 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π· β§ (π β Fin β§ π
β CRing)) β π β (Baseβπ΄)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β π β (Baseβπ΄)) |
76 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβπ
) =
(Baseβπ
) |
77 | 29, 76 | matecl 21790 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ πΌ β π β§ π β (Baseβπ΄)) β (πΌππΌ) β (Baseβπ
)) |
78 | 64, 64, 75, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β (πΌππΌ) β (Baseβπ
)) |
79 | 28 | ply1sca 21640 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β CRing β π
= (Scalarβπ)) |
80 | 79 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π· β§ (π β Fin β§ π
β CRing)) β π
= (Scalarβπ)) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β π
= (Scalarβπ)) |
82 | 81 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β (Scalarβπ) = π
) |
83 | 82 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β (Baseβ(Scalarβπ)) = (Baseβπ
)) |
84 | 78, 83 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . 16
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β (πΌππΌ) β (Baseβ(Scalarβπ))) |
85 | 73, 84 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β (πβ(πΌππΌ)) β (Baseβπ)) |
86 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (πΈ = (πΌππΌ) β (πβπΈ) = (πβ(πΌππΌ))) |
87 | 86 | eqcoms 2745 |
. . . . . . . . . . . . . . . 16
β’ ((πΌππΌ) = πΈ β (πβπΈ) = (πβ(πΌππΌ))) |
88 | 87 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ ((πΌππΌ) = πΈ β ((πβπΈ) β (Baseβπ) β (πβ(πΌππΌ)) β (Baseβπ))) |
89 | 85, 88 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β ((πΌππΌ) = πΈ β (πβπΈ) β (Baseβπ))) |
90 | 89 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β§ π = πΌ) β ((πΌππΌ) = πΈ β (πβπΈ) β (Baseβπ))) |
91 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΌ β π = πΌ) |
92 | 91, 91 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = πΌ β (πππ) = (πΌππΌ)) |
93 | 92 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
β’ (π = πΌ β ((πππ) = πΈ β (πΌππΌ) = πΈ)) |
94 | 93 | imbi1d 342 |
. . . . . . . . . . . . . 14
β’ (π = πΌ β (((πππ) = πΈ β (πβπΈ) β (Baseβπ)) β ((πΌππΌ) = πΈ β (πβπΈ) β (Baseβπ)))) |
95 | 94 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β§ π = πΌ) β (((πππ) = πΈ β (πβπΈ) β (Baseβπ)) β ((πΌππΌ) = πΈ β (πβπΈ) β (Baseβπ)))) |
96 | 90, 95 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β§ π = πΌ) β ((πππ) = πΈ β (πβπΈ) β (Baseβπ))) |
97 | 64, 96 | rspcimdv 3574 |
. . . . . . . . . . 11
β’ (((π β π· β§ (π β Fin β§ π
β CRing)) β§ πΌ β π) β (βπ β π (πππ) = πΈ β (πβπΈ) β (Baseβπ))) |
98 | 97 | ex 414 |
. . . . . . . . . 10
β’ ((π β π· β§ (π β Fin β§ π
β CRing)) β (πΌ β π β (βπ β π (πππ) = πΈ β (πβπΈ) β (Baseβπ)))) |
99 | 98 | com23 86 |
. . . . . . . . 9
β’ ((π β π· β§ (π β Fin β§ π
β CRing)) β (βπ β π (πππ) = πΈ β (πΌ β π β (πβπΈ) β (Baseβπ)))) |
100 | 99 | ex 414 |
. . . . . . . 8
β’ (π β π· β ((π β Fin β§ π
β CRing) β (βπ β π (πππ) = πΈ β (πΌ β π β (πβπΈ) β (Baseβπ))))) |
101 | 100 | com24 95 |
. . . . . . 7
β’ (π β π· β (πΌ β π β (βπ β π (πππ) = πΈ β ((π β Fin β§ π
β CRing) β (πβπΈ) β (Baseβπ))))) |
102 | 101 | 3imp 1112 |
. . . . . 6
β’ ((π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ) β ((π β Fin β§ π
β CRing) β (πβπΈ) β (Baseβπ))) |
103 | 102 | impcom 409 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (πβπΈ) β (Baseβπ)) |
104 | 60, 35 | grpsubcl 18834 |
. . . . 5
β’ ((π β Grp β§ π β (Baseβπ) β§ (πβπΈ) β (Baseβπ)) β (π β (πβπΈ)) β (Baseβπ)) |
105 | 59, 63, 103, 104 | syl3anc 1372 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (π β (πβπΈ)) β (Baseβπ)) |
106 | 34, 60 | mgpbas 19909 |
. . . 4
β’
(Baseβπ) =
(BaseβπΊ) |
107 | 105, 106 | eleqtrdi 2848 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (π β (πβπΈ)) β (BaseβπΊ)) |
108 | | eqid 2737 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
109 | | chp0mat.m |
. . . 4
β’ β =
(.gβπΊ) |
110 | 108, 109 | gsumconst 19718 |
. . 3
β’ ((πΊ β Mnd β§ π β Fin β§ (π β (πβπΈ)) β (BaseβπΊ)) β (πΊ Ξ£g (π β π β¦ (π β (πβπΈ)))) = ((β―βπ) β (π β (πβπΈ)))) |
111 | 53, 1, 107, 110 | syl3anc 1372 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (πΊ Ξ£g (π β π β¦ (π β (πβπΈ)))) = ((β―βπ) β (π β (πβπΈ)))) |
112 | 37, 48, 111 | 3eqtrd 2781 |
1
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ πΌ β π β§ βπ β π (πππ) = πΈ)) β (πΆβπ) = ((β―βπ) β (π β (πβπΈ)))) |