Step | Hyp | Ref
| Expression |
1 | | coe1pwmul.z |
. . 3
β’ 0 =
(0gβπ
) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | coe1pwmul.p |
. . 3
β’ π = (Poly1βπ
) |
4 | | coe1pwmul.x |
. . 3
β’ π = (var1βπ
) |
5 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
6 | | coe1pwmul.n |
. . 3
β’ π = (mulGrpβπ) |
7 | | coe1pwmul.e |
. . 3
β’ β =
(.gβπ) |
8 | | coe1pwmul.b |
. . 3
β’ π΅ = (Baseβπ) |
9 | | coe1pwmul.t |
. . 3
β’ Β· =
(.rβπ) |
10 | | eqid 2733 |
. . 3
β’
(.rβπ
) = (.rβπ
) |
11 | | coe1pwmul.a |
. . 3
β’ (π β π΄ β π΅) |
12 | | coe1pwmul.r |
. . 3
β’ (π β π
β Ring) |
13 | | eqid 2733 |
. . . . 5
β’
(1rβπ
) = (1rβπ
) |
14 | 2, 13 | ringidcl 19994 |
. . . 4
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
15 | 12, 14 | syl 17 |
. . 3
β’ (π β (1rβπ
) β (Baseβπ
)) |
16 | | coe1pwmul.d |
. . 3
β’ (π β π· β
β0) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 15, 16 | coe1tmmul 21664 |
. 2
β’ (π β
(coe1β(((1rβπ
)( Β·π
βπ)(π· β π)) Β· π΄)) = (π₯ β β0 β¦ if(π· β€ π₯, ((1rβπ
)(.rβπ
)((coe1βπ΄)β(π₯ β π·))), 0 ))) |
18 | 3 | ply1sca 21640 |
. . . . . . 7
β’ (π
β Ring β π
= (Scalarβπ)) |
19 | 12, 18 | syl 17 |
. . . . . 6
β’ (π β π
= (Scalarβπ)) |
20 | 19 | fveq2d 6847 |
. . . . 5
β’ (π β (1rβπ
) =
(1rβ(Scalarβπ))) |
21 | 20 | oveq1d 7373 |
. . . 4
β’ (π β
((1rβπ
)(
Β·π βπ)(π· β π)) =
((1rβ(Scalarβπ))( Β·π
βπ)(π· β π))) |
22 | 3 | ply1lmod 21639 |
. . . . . 6
β’ (π
β Ring β π β LMod) |
23 | 12, 22 | syl 17 |
. . . . 5
β’ (π β π β LMod) |
24 | 6, 8 | mgpbas 19907 |
. . . . . 6
β’ π΅ = (Baseβπ) |
25 | 3 | ply1ring 21635 |
. . . . . . 7
β’ (π
β Ring β π β Ring) |
26 | 6 | ringmgp 19975 |
. . . . . . 7
β’ (π β Ring β π β Mnd) |
27 | 12, 25, 26 | 3syl 18 |
. . . . . 6
β’ (π β π β Mnd) |
28 | 4, 3, 8 | vr1cl 21604 |
. . . . . . 7
β’ (π
β Ring β π β π΅) |
29 | 12, 28 | syl 17 |
. . . . . 6
β’ (π β π β π΅) |
30 | 24, 7, 27, 16, 29 | mulgnn0cld 18902 |
. . . . 5
β’ (π β (π· β π) β π΅) |
31 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
32 | | eqid 2733 |
. . . . . 6
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
33 | 8, 31, 5, 32 | lmodvs1 20365 |
. . . . 5
β’ ((π β LMod β§ (π· β π) β π΅) β
((1rβ(Scalarβπ))( Β·π
βπ)(π· β π)) = (π· β π)) |
34 | 23, 30, 33 | syl2anc 585 |
. . . 4
β’ (π β
((1rβ(Scalarβπ))( Β·π
βπ)(π· β π)) = (π· β π)) |
35 | 21, 34 | eqtrd 2773 |
. . 3
β’ (π β
((1rβπ
)(
Β·π βπ)(π· β π)) = (π· β π)) |
36 | 35 | fvoveq1d 7380 |
. 2
β’ (π β
(coe1β(((1rβπ
)( Β·π
βπ)(π· β π)) Β· π΄)) = (coe1β((π· β π) Β· π΄))) |
37 | 12 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β π
β Ring) |
38 | | eqid 2733 |
. . . . . . . . 9
β’
(coe1βπ΄) = (coe1βπ΄) |
39 | 38, 8, 3, 2 | coe1f 21598 |
. . . . . . . 8
β’ (π΄ β π΅ β (coe1βπ΄):β0βΆ(Baseβπ
)) |
40 | 11, 39 | syl 17 |
. . . . . . 7
β’ (π β
(coe1βπ΄):β0βΆ(Baseβπ
)) |
41 | 40 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β (coe1βπ΄):β0βΆ(Baseβπ
)) |
42 | 16 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β π· β
β0) |
43 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β π₯ β β0) |
44 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β π· β€ π₯) |
45 | | nn0sub2 12569 |
. . . . . . 7
β’ ((π· β β0
β§ π₯ β
β0 β§ π·
β€ π₯) β (π₯ β π·) β
β0) |
46 | 42, 43, 44, 45 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β (π₯ β π·) β
β0) |
47 | 41, 46 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β ((coe1βπ΄)β(π₯ β π·)) β (Baseβπ
)) |
48 | 2, 10, 13 | ringlidm 19997 |
. . . . 5
β’ ((π
β Ring β§
((coe1βπ΄)β(π₯ β π·)) β (Baseβπ
)) β ((1rβπ
)(.rβπ
)((coe1βπ΄)β(π₯ β π·))) = ((coe1βπ΄)β(π₯ β π·))) |
49 | 37, 47, 48 | syl2anc 585 |
. . . 4
β’ (((π β§ π₯ β β0) β§ π· β€ π₯) β ((1rβπ
)(.rβπ
)((coe1βπ΄)β(π₯ β π·))) = ((coe1βπ΄)β(π₯ β π·))) |
50 | 49 | ifeq1da 4518 |
. . 3
β’ ((π β§ π₯ β β0) β if(π· β€ π₯, ((1rβπ
)(.rβπ
)((coe1βπ΄)β(π₯ β π·))), 0 ) = if(π· β€ π₯, ((coe1βπ΄)β(π₯ β π·)), 0 )) |
51 | 50 | mpteq2dva 5206 |
. 2
β’ (π β (π₯ β β0 β¦ if(π· β€ π₯, ((1rβπ
)(.rβπ
)((coe1βπ΄)β(π₯ β π·))), 0 )) = (π₯ β β0 β¦ if(π· β€ π₯, ((coe1βπ΄)β(π₯ β π·)), 0 ))) |
52 | 17, 36, 51 | 3eqtr3d 2781 |
1
β’ (π β
(coe1β((π·
β
π) Β· π΄)) = (π₯ β β0 β¦ if(π· β€ π₯, ((coe1βπ΄)β(π₯ β π·)), 0 ))) |