Step | Hyp | Ref
| Expression |
1 | | uc1pmon1p.p |
. . . . 5
β’ π = (Poly1βπ
) |
2 | 1 | ply1ring 22088 |
. . . 4
β’ (π
β Ring β π β Ring) |
3 | 2 | adantr 480 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β π β Ring) |
4 | | uc1pmon1p.a |
. . . . . 6
β’ π΄ = (algScβπ) |
5 | | eqid 2724 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
6 | | eqid 2724 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
7 | 1, 4, 5, 6 | ply1sclf 22125 |
. . . . 5
β’ (π
β Ring β π΄:(Baseβπ
)βΆ(Baseβπ)) |
8 | 7 | adantr 480 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β π΄:(Baseβπ
)βΆ(Baseβπ)) |
9 | | uc1pmon1p.d |
. . . . . 6
β’ π· = ( deg1
βπ
) |
10 | | eqid 2724 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
11 | | uc1pmon1p.c |
. . . . . 6
β’ πΆ =
(Unic1pβπ
) |
12 | 9, 10, 11 | uc1pldg 26005 |
. . . . 5
β’ (π β πΆ β ((coe1βπ)β(π·βπ)) β (Unitβπ
)) |
13 | | uc1pmon1p.i |
. . . . . 6
β’ πΌ = (invrβπ
) |
14 | 10, 13, 5 | ringinvcl 20283 |
. . . . 5
β’ ((π
β Ring β§
((coe1βπ)β(π·βπ)) β (Unitβπ
)) β (πΌβ((coe1βπ)β(π·βπ))) β (Baseβπ
)) |
15 | 12, 14 | sylan2 592 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β (πΌβ((coe1βπ)β(π·βπ))) β (Baseβπ
)) |
16 | 8, 15 | ffvelcdmd 7077 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β (π΄β(πΌβ((coe1βπ)β(π·βπ)))) β (Baseβπ)) |
17 | 1, 6, 11 | uc1pcl 26000 |
. . . 4
β’ (π β πΆ β π β (Baseβπ)) |
18 | 17 | adantl 481 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β π β (Baseβπ)) |
19 | | uc1pmon1p.t |
. . . 4
β’ Β· =
(.rβπ) |
20 | 6, 19 | ringcl 20144 |
. . 3
β’ ((π β Ring β§ (π΄β(πΌβ((coe1βπ)β(π·βπ)))) β (Baseβπ) β§ π β (Baseβπ)) β ((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (Baseβπ)) |
21 | 3, 16, 18, 20 | syl3anc 1368 |
. 2
β’ ((π
β Ring β§ π β πΆ) β ((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (Baseβπ)) |
22 | | simpl 482 |
. . . . 5
β’ ((π
β Ring β§ π β πΆ) β π
β Ring) |
23 | | eqid 2724 |
. . . . . . . 8
β’
(RLRegβπ
) =
(RLRegβπ
) |
24 | 23, 10 | unitrrg 21192 |
. . . . . . 7
β’ (π
β Ring β
(Unitβπ
) β
(RLRegβπ
)) |
25 | 24 | adantr 480 |
. . . . . 6
β’ ((π
β Ring β§ π β πΆ) β (Unitβπ
) β (RLRegβπ
)) |
26 | 10, 13 | unitinvcl 20281 |
. . . . . . 7
β’ ((π
β Ring β§
((coe1βπ)β(π·βπ)) β (Unitβπ
)) β (πΌβ((coe1βπ)β(π·βπ))) β (Unitβπ
)) |
27 | 12, 26 | sylan2 592 |
. . . . . 6
β’ ((π
β Ring β§ π β πΆ) β (πΌβ((coe1βπ)β(π·βπ))) β (Unitβπ
)) |
28 | 25, 27 | sseldd 3975 |
. . . . 5
β’ ((π
β Ring β§ π β πΆ) β (πΌβ((coe1βπ)β(π·βπ))) β (RLRegβπ
)) |
29 | 9, 1, 23, 6, 19, 4 | deg1mul3 25972 |
. . . . 5
β’ ((π
β Ring β§ (πΌβ((coe1βπ)β(π·βπ))) β (RLRegβπ
) β§ π β (Baseβπ)) β (π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) = (π·βπ)) |
30 | 22, 28, 18, 29 | syl3anc 1368 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β (π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) = (π·βπ)) |
31 | 9, 11 | uc1pdeg 26004 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β (π·βπ) β
β0) |
32 | 30, 31 | eqeltrd 2825 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β (π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) β
β0) |
33 | | eqid 2724 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
34 | 9, 1, 33, 6 | deg1nn0clb 25947 |
. . . 4
β’ ((π
β Ring β§ ((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (Baseβπ)) β (((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (0gβπ) β (π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) β
β0)) |
35 | 21, 34 | syldan 590 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β (((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (0gβπ) β (π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) β
β0)) |
36 | 32, 35 | mpbird 257 |
. 2
β’ ((π
β Ring β§ π β πΆ) β ((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (0gβπ)) |
37 | 30 | fveq2d 6885 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β ((coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))β(π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))) = ((coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))β(π·βπ))) |
38 | | eqid 2724 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
39 | 1, 6, 5, 4, 19, 38 | coe1sclmul 22122 |
. . . . 5
β’ ((π
β Ring β§ (πΌβ((coe1βπ)β(π·βπ))) β (Baseβπ
) β§ π β (Baseβπ)) β (coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) = ((β0 Γ {(πΌβ((coe1βπ)β(π·βπ)))}) βf
(.rβπ
)(coe1βπ))) |
40 | 22, 15, 18, 39 | syl3anc 1368 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β (coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π)) = ((β0 Γ {(πΌβ((coe1βπ)β(π·βπ)))}) βf
(.rβπ
)(coe1βπ))) |
41 | 40 | fveq1d 6883 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β ((coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))β(π·βπ)) = (((β0 Γ {(πΌβ((coe1βπ)β(π·βπ)))}) βf
(.rβπ
)(coe1βπ))β(π·βπ))) |
42 | | nn0ex 12474 |
. . . . . . 7
β’
β0 β V |
43 | 42 | a1i 11 |
. . . . . 6
β’ ((π
β Ring β§ π β πΆ) β β0 β
V) |
44 | | fvexd 6896 |
. . . . . 6
β’ ((π
β Ring β§ π β πΆ) β (πΌβ((coe1βπ)β(π·βπ))) β V) |
45 | | eqid 2724 |
. . . . . . . 8
β’
(coe1βπ) = (coe1βπ) |
46 | 45, 6, 1, 5 | coe1f 22052 |
. . . . . . 7
β’ (π β (Baseβπ) β
(coe1βπ):β0βΆ(Baseβπ
)) |
47 | | ffn 6707 |
. . . . . . 7
β’
((coe1βπ):β0βΆ(Baseβπ
) β
(coe1βπ) Fn
β0) |
48 | 18, 46, 47 | 3syl 18 |
. . . . . 6
β’ ((π
β Ring β§ π β πΆ) β (coe1βπ) Fn
β0) |
49 | | eqidd 2725 |
. . . . . 6
β’ (((π
β Ring β§ π β πΆ) β§ (π·βπ) β β0) β
((coe1βπ)β(π·βπ)) = ((coe1βπ)β(π·βπ))) |
50 | 43, 44, 48, 49 | ofc1 7689 |
. . . . 5
β’ (((π
β Ring β§ π β πΆ) β§ (π·βπ) β β0) β
(((β0 Γ {(πΌβ((coe1βπ)β(π·βπ)))}) βf
(.rβπ
)(coe1βπ))β(π·βπ)) = ((πΌβ((coe1βπ)β(π·βπ)))(.rβπ
)((coe1βπ)β(π·βπ)))) |
51 | 31, 50 | mpdan 684 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β (((β0 Γ
{(πΌβ((coe1βπ)β(π·βπ)))}) βf
(.rβπ
)(coe1βπ))β(π·βπ)) = ((πΌβ((coe1βπ)β(π·βπ)))(.rβπ
)((coe1βπ)β(π·βπ)))) |
52 | | eqid 2724 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
53 | 10, 13, 38, 52 | unitlinv 20284 |
. . . . 5
β’ ((π
β Ring β§
((coe1βπ)β(π·βπ)) β (Unitβπ
)) β ((πΌβ((coe1βπ)β(π·βπ)))(.rβπ
)((coe1βπ)β(π·βπ))) = (1rβπ
)) |
54 | 12, 53 | sylan2 592 |
. . . 4
β’ ((π
β Ring β§ π β πΆ) β ((πΌβ((coe1βπ)β(π·βπ)))(.rβπ
)((coe1βπ)β(π·βπ))) = (1rβπ
)) |
55 | 51, 54 | eqtrd 2764 |
. . 3
β’ ((π
β Ring β§ π β πΆ) β (((β0 Γ
{(πΌβ((coe1βπ)β(π·βπ)))}) βf
(.rβπ
)(coe1βπ))β(π·βπ)) = (1rβπ
)) |
56 | 37, 41, 55 | 3eqtrd 2768 |
. 2
β’ ((π
β Ring β§ π β πΆ) β ((coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))β(π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))) = (1rβπ
)) |
57 | | uc1pmon1p.m |
. . 3
β’ π =
(Monic1pβπ
) |
58 | 1, 6, 33, 9, 57, 52 | ismon1p 25999 |
. 2
β’ (((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β π β (((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (Baseβπ) β§ ((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β (0gβπ) β§
((coe1β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))β(π·β((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π))) = (1rβπ
))) |
59 | 21, 36, 56, 58 | syl3anbrc 1340 |
1
β’ ((π
β Ring β§ π β πΆ) β ((π΄β(πΌβ((coe1βπ)β(π·βπ)))) Β· π) β π) |