Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(odβπ) =
(odβπ) |
2 | | eqid 2733 |
. . 3
β’
(1rβπ) = (1rβπ) |
3 | | eqid 2733 |
. . 3
β’
(chrβπ) =
(chrβπ) |
4 | 1, 2, 3 | chrval 20951 |
. 2
β’
((odβπ)β(1rβπ)) = (chrβπ) |
5 | | eqid 2733 |
. . . . . . . . . 10
β’
(odβπ
) =
(odβπ
) |
6 | | eqid 2733 |
. . . . . . . . . 10
β’
(1rβπ
) = (1rβπ
) |
7 | | eqid 2733 |
. . . . . . . . . 10
β’
(chrβπ
) =
(chrβπ
) |
8 | 5, 6, 7 | chrval 20951 |
. . . . . . . . 9
β’
((odβπ
)β(1rβπ
)) = (chrβπ
) |
9 | 8 | eqcomi 2742 |
. . . . . . . 8
β’
(chrβπ
) =
((odβπ
)β(1rβπ
)) |
10 | | id 22 |
. . . . . . . . . 10
β’ (π
β CRing β π
β CRing) |
11 | 10 | crnggrpd 19986 |
. . . . . . . . 9
β’ (π
β CRing β π
β Grp) |
12 | | crngring 19984 |
. . . . . . . . . 10
β’ (π
β CRing β π
β Ring) |
13 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
14 | 13, 6 | ringidcl 19997 |
. . . . . . . . . 10
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
β’ (π
β CRing β
(1rβπ
)
β (Baseβπ
)) |
16 | 7 | chrcl 20952 |
. . . . . . . . . 10
β’ (π
β Ring β
(chrβπ
) β
β0) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
β’ (π
β CRing β
(chrβπ
) β
β0) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(.gβπ
) = (.gβπ
) |
19 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβπ
) = (0gβπ
) |
20 | 13, 5, 18, 19 | odeq 19340 |
. . . . . . . . 9
β’ ((π
β Grp β§
(1rβπ
)
β (Baseβπ
) β§
(chrβπ
) β
β0) β ((chrβπ
) = ((odβπ
)β(1rβπ
)) β βπ β β0
((chrβπ
) β₯
π β (π(.gβπ
)(1rβπ
)) = (0gβπ
)))) |
21 | 11, 15, 17, 20 | syl3anc 1372 |
. . . . . . . 8
β’ (π
β CRing β
((chrβπ
) =
((odβπ
)β(1rβπ
)) β βπ β β0
((chrβπ
) β₯
π β (π(.gβπ
)(1rβπ
)) = (0gβπ
)))) |
22 | 9, 21 | mpbii 232 |
. . . . . . 7
β’ (π
β CRing β
βπ β
β0 ((chrβπ
) β₯ π β (π(.gβπ
)(1rβπ
)) = (0gβπ
))) |
23 | 22 | r19.21bi 3233 |
. . . . . 6
β’ ((π
β CRing β§ π β β0)
β ((chrβπ
)
β₯ π β (π(.gβπ
)(1rβπ
)) = (0gβπ
))) |
24 | | ply1chr.1 |
. . . . . . 7
β’ π = (Poly1βπ
) |
25 | | eqid 2733 |
. . . . . . 7
β’
(algScβπ) =
(algScβπ) |
26 | 12 | adantr 482 |
. . . . . . 7
β’ ((π
β CRing β§ π β β0)
β π
β
Ring) |
27 | 11 | grpmndd 18768 |
. . . . . . . . 9
β’ (π
β CRing β π
β Mnd) |
28 | 27 | adantr 482 |
. . . . . . . 8
β’ ((π
β CRing β§ π β β0)
β π
β
Mnd) |
29 | | simpr 486 |
. . . . . . . 8
β’ ((π
β CRing β§ π β β0)
β π β
β0) |
30 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π
β CRing β§ π β β0)
β (1rβπ
) β (Baseβπ
)) |
31 | 13, 18, 28, 29, 30 | mulgnn0cld 18905 |
. . . . . . 7
β’ ((π
β CRing β§ π β β0)
β (π(.gβπ
)(1rβπ
)) β (Baseβπ
)) |
32 | | simpl 484 |
. . . . . . . 8
β’ ((π
β CRing β§ π β β0)
β π
β
CRing) |
33 | 13, 19 | ring0cl 19998 |
. . . . . . . 8
β’ (π
β Ring β
(0gβπ
)
β (Baseβπ
)) |
34 | 32, 12, 33 | 3syl 18 |
. . . . . . 7
β’ ((π
β CRing β§ π β β0)
β (0gβπ
) β (Baseβπ
)) |
35 | 24, 13, 25, 26, 31, 34 | ply1scleq 32322 |
. . . . . 6
β’ ((π
β CRing β§ π β β0)
β (((algScβπ)β(π(.gβπ
)(1rβπ
))) = ((algScβπ)β(0gβπ
)) β (π(.gβπ
)(1rβπ
)) = (0gβπ
))) |
36 | 24 | ply1sca 21647 |
. . . . . . . . . . . 12
β’ (π
β CRing β π
= (Scalarβπ)) |
37 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π β β0)
β π
=
(Scalarβπ)) |
38 | 37 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π β β0)
β (.gβπ
) = (.gβ(Scalarβπ))) |
39 | 38 | oveqd 7378 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β β0)
β (π(.gβπ
)(1rβπ
)) = (π(.gβ(Scalarβπ))(1rβπ
))) |
40 | 39 | fveq2d 6850 |
. . . . . . . 8
β’ ((π
β CRing β§ π β β0)
β ((algScβπ)β(π(.gβπ
)(1rβπ
))) = ((algScβπ)β(π(.gβ(Scalarβπ))(1rβπ
)))) |
41 | 24 | ply1assa 21593 |
. . . . . . . . . 10
β’ (π
β CRing β π β AssAlg) |
42 | 41 | adantr 482 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β β0)
β π β
AssAlg) |
43 | 37 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π
β CRing β§ π β β0)
β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
44 | 30, 43 | eleqtrd 2836 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β β0)
β (1rβπ
) β (Baseβ(Scalarβπ))) |
45 | | eqid 2733 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
46 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
47 | | eqid 2733 |
. . . . . . . . . 10
β’
(.gβπ) = (.gβπ) |
48 | | eqid 2733 |
. . . . . . . . . 10
β’
(.gβ(Scalarβπ)) =
(.gβ(Scalarβπ)) |
49 | 25, 45, 46, 47, 48 | asclmulg 32318 |
. . . . . . . . 9
β’ ((π β AssAlg β§ π β β0
β§ (1rβπ
) β (Baseβ(Scalarβπ))) β ((algScβπ)β(π(.gβ(Scalarβπ))(1rβπ
))) = (π(.gβπ)((algScβπ)β(1rβπ
)))) |
50 | 42, 29, 44, 49 | syl3anc 1372 |
. . . . . . . 8
β’ ((π
β CRing β§ π β β0)
β ((algScβπ)β(π(.gβ(Scalarβπ))(1rβπ
))) = (π(.gβπ)((algScβπ)β(1rβπ
)))) |
51 | 40, 50 | eqtrd 2773 |
. . . . . . 7
β’ ((π
β CRing β§ π β β0)
β ((algScβπ)β(π(.gβπ
)(1rβπ
))) = (π(.gβπ)((algScβπ)β(1rβπ
)))) |
52 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
53 | 24, 25, 19, 52 | ply1scl0 21684 |
. . . . . . . 8
β’ (π
β Ring β
((algScβπ)β(0gβπ
)) = (0gβπ)) |
54 | 32, 12, 53 | 3syl 18 |
. . . . . . 7
β’ ((π
β CRing β§ π β β0)
β ((algScβπ)β(0gβπ
)) = (0gβπ)) |
55 | 51, 54 | eqeq12d 2749 |
. . . . . 6
β’ ((π
β CRing β§ π β β0)
β (((algScβπ)β(π(.gβπ
)(1rβπ
))) = ((algScβπ)β(0gβπ
)) β (π(.gβπ)((algScβπ)β(1rβπ
))) = (0gβπ))) |
56 | 23, 35, 55 | 3bitr2d 307 |
. . . . 5
β’ ((π
β CRing β§ π β β0)
β ((chrβπ
)
β₯ π β (π(.gβπ)((algScβπ)β(1rβπ
))) = (0gβπ))) |
57 | 56 | ralrimiva 3140 |
. . . 4
β’ (π
β CRing β
βπ β
β0 ((chrβπ
) β₯ π β (π(.gβπ)((algScβπ)β(1rβπ
))) = (0gβπ))) |
58 | 24 | ply1crng 21592 |
. . . . . 6
β’ (π
β CRing β π β CRing) |
59 | 58 | crnggrpd 19986 |
. . . . 5
β’ (π
β CRing β π β Grp) |
60 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
61 | 24, 25, 13, 60 | ply1sclcl 21680 |
. . . . . 6
β’ ((π
β Ring β§
(1rβπ
)
β (Baseβπ
))
β ((algScβπ)β(1rβπ
)) β (Baseβπ)) |
62 | 12, 15, 61 | syl2anc 585 |
. . . . 5
β’ (π
β CRing β
((algScβπ)β(1rβπ
)) β (Baseβπ)) |
63 | 60, 1, 47, 52 | odeq 19340 |
. . . . 5
β’ ((π β Grp β§
((algScβπ)β(1rβπ
)) β (Baseβπ) β§ (chrβπ
) β β0)
β ((chrβπ
) =
((odβπ)β((algScβπ)β(1rβπ
))) β βπ β β0
((chrβπ
) β₯
π β (π(.gβπ)((algScβπ)β(1rβπ
))) = (0gβπ)))) |
64 | 59, 62, 17, 63 | syl3anc 1372 |
. . . 4
β’ (π
β CRing β
((chrβπ
) =
((odβπ)β((algScβπ)β(1rβπ
))) β βπ β β0
((chrβπ
) β₯
π β (π(.gβπ)((algScβπ)β(1rβπ
))) = (0gβπ)))) |
65 | 57, 64 | mpbird 257 |
. . 3
β’ (π
β CRing β
(chrβπ
) =
((odβπ)β((algScβπ)β(1rβπ
)))) |
66 | 24, 25, 6, 2 | ply1scl1 21686 |
. . . . 5
β’ (π
β Ring β
((algScβπ)β(1rβπ
)) = (1rβπ)) |
67 | 66 | fveq2d 6850 |
. . . 4
β’ (π
β Ring β
((odβπ)β((algScβπ)β(1rβπ
))) = ((odβπ)β(1rβπ))) |
68 | 12, 67 | syl 17 |
. . 3
β’ (π
β CRing β
((odβπ)β((algScβπ)β(1rβπ
))) = ((odβπ)β(1rβπ))) |
69 | 65, 68 | eqtr2d 2774 |
. 2
β’ (π
β CRing β
((odβπ)β(1rβπ)) = (chrβπ
)) |
70 | 4, 69 | eqtr3id 2787 |
1
β’ (π
β CRing β
(chrβπ) =
(chrβπ
)) |