Step | Hyp | Ref
| Expression |
1 | | 1cnd 11205 |
. 2
β’ (π β 1 β
β) |
2 | | fta1g.1 |
. . . . . 6
β’ (π β π
β IDomn) |
3 | | isidom 20914 |
. . . . . . 7
β’ (π
β IDomn β (π
β CRing β§ π
β Domn)) |
4 | | domnnzr 20903 |
. . . . . . 7
β’ (π
β Domn β π
β NzRing) |
5 | 3, 4 | simplbiim 505 |
. . . . . 6
β’ (π
β IDomn β π
β NzRing) |
6 | 2, 5 | syl 17 |
. . . . 5
β’ (π β π
β NzRing) |
7 | | nzrring 20287 |
. . . . 5
β’ (π
β NzRing β π
β Ring) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β π
β Ring) |
9 | | fta1g.2 |
. . . . 5
β’ (π β πΉ β π΅) |
10 | | fta1g.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
11 | | fta1g.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
12 | | fta1glem.k |
. . . . . . . 8
β’ πΎ = (Baseβπ
) |
13 | | fta1glem.x |
. . . . . . . 8
β’ π = (var1βπ
) |
14 | | fta1glem.m |
. . . . . . . 8
β’ β =
(-gβπ) |
15 | | fta1glem.a |
. . . . . . . 8
β’ π΄ = (algScβπ) |
16 | | fta1glem.g |
. . . . . . . 8
β’ πΊ = (π β (π΄βπ)) |
17 | | fta1g.o |
. . . . . . . 8
β’ π = (eval1βπ
) |
18 | 3 | simplbi 498 |
. . . . . . . . 9
β’ (π
β IDomn β π
β CRing) |
19 | 2, 18 | syl 17 |
. . . . . . . 8
β’ (π β π
β CRing) |
20 | | fta1glem.5 |
. . . . . . . . . 10
β’ (π β π β (β‘(πβπΉ) β {π})) |
21 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (π
βs πΎ) = (π
βs πΎ) |
22 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβ(π
βs πΎ)) = (Baseβ(π
βs πΎ)) |
23 | 12 | fvexi 6902 |
. . . . . . . . . . . . . 14
β’ πΎ β V |
24 | 23 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β πΎ β V) |
25 | 17, 10, 21, 12 | evl1rhm 21842 |
. . . . . . . . . . . . . . . 16
β’ (π
β CRing β π β (π RingHom (π
βs πΎ))) |
26 | 19, 25 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π RingHom (π
βs πΎ))) |
27 | 11, 22 | rhmf 20255 |
. . . . . . . . . . . . . . 15
β’ (π β (π RingHom (π
βs πΎ)) β π:π΅βΆ(Baseβ(π
βs πΎ))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π:π΅βΆ(Baseβ(π
βs πΎ))) |
29 | 28, 9 | ffvelcdmd 7084 |
. . . . . . . . . . . . 13
β’ (π β (πβπΉ) β (Baseβ(π
βs πΎ))) |
30 | 21, 12, 22, 2, 24, 29 | pwselbas 17431 |
. . . . . . . . . . . 12
β’ (π β (πβπΉ):πΎβΆπΎ) |
31 | 30 | ffnd 6715 |
. . . . . . . . . . 11
β’ (π β (πβπΉ) Fn πΎ) |
32 | | fniniseg 7058 |
. . . . . . . . . . 11
β’ ((πβπΉ) Fn πΎ β (π β (β‘(πβπΉ) β {π}) β (π β πΎ β§ ((πβπΉ)βπ) = π))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (β‘(πβπΉ) β {π}) β (π β πΎ β§ ((πβπΉ)βπ) = π))) |
34 | 20, 33 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π β πΎ β§ ((πβπΉ)βπ) = π)) |
35 | 34 | simpld 495 |
. . . . . . . 8
β’ (π β π β πΎ) |
36 | | eqid 2732 |
. . . . . . . 8
β’
(Monic1pβπ
) = (Monic1pβπ
) |
37 | | fta1g.d |
. . . . . . . 8
β’ π· = ( deg1
βπ
) |
38 | | fta1g.w |
. . . . . . . 8
β’ π = (0gβπ
) |
39 | 10, 11, 12, 13, 14, 15, 16, 17, 6, 19, 35, 36, 37, 38 | ply1remlem 25671 |
. . . . . . 7
β’ (π β (πΊ β (Monic1pβπ
) β§ (π·βπΊ) = 1 β§ (β‘(πβπΊ) β {π}) = {π})) |
40 | 39 | simp1d 1142 |
. . . . . 6
β’ (π β πΊ β (Monic1pβπ
)) |
41 | | eqid 2732 |
. . . . . . 7
β’
(Unic1pβπ
) = (Unic1pβπ
) |
42 | 41, 36 | mon1puc1p 25659 |
. . . . . 6
β’ ((π
β Ring β§ πΊ β
(Monic1pβπ
)) β πΊ β (Unic1pβπ
)) |
43 | 8, 40, 42 | syl2anc 584 |
. . . . 5
β’ (π β πΊ β (Unic1pβπ
)) |
44 | | eqid 2732 |
. . . . . 6
β’
(quot1pβπ
) = (quot1pβπ
) |
45 | 44, 10, 11, 41 | q1pcl 25664 |
. . . . 5
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β (Unic1pβπ
)) β (πΉ(quot1pβπ
)πΊ) β π΅) |
46 | 8, 9, 43, 45 | syl3anc 1371 |
. . . 4
β’ (π β (πΉ(quot1pβπ
)πΊ) β π΅) |
47 | | fta1glem.4 |
. . . . . . . 8
β’ (π β (π·βπΉ) = (π + 1)) |
48 | | fta1glem.3 |
. . . . . . . . 9
β’ (π β π β
β0) |
49 | | peano2nn0 12508 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β0) |
50 | 48, 49 | syl 17 |
. . . . . . . 8
β’ (π β (π + 1) β
β0) |
51 | 47, 50 | eqeltrd 2833 |
. . . . . . 7
β’ (π β (π·βπΉ) β
β0) |
52 | | fta1g.z |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
53 | 37, 10, 52, 11 | deg1nn0clb 25599 |
. . . . . . . 8
β’ ((π
β Ring β§ πΉ β π΅) β (πΉ β 0 β (π·βπΉ) β
β0)) |
54 | 8, 9, 53 | syl2anc 584 |
. . . . . . 7
β’ (π β (πΉ β 0 β (π·βπΉ) β
β0)) |
55 | 51, 54 | mpbird 256 |
. . . . . 6
β’ (π β πΉ β 0 ) |
56 | 34 | simprd 496 |
. . . . . . . . 9
β’ (π β ((πβπΉ)βπ) = π) |
57 | | eqid 2732 |
. . . . . . . . . 10
β’
(β₯rβπ) = (β₯rβπ) |
58 | 10, 11, 12, 13, 14, 15, 16, 17, 6, 19, 35, 9, 38, 57 | facth1 25673 |
. . . . . . . . 9
β’ (π β (πΊ(β₯rβπ)πΉ β ((πβπΉ)βπ) = π)) |
59 | 56, 58 | mpbird 256 |
. . . . . . . 8
β’ (π β πΊ(β₯rβπ)πΉ) |
60 | | eqid 2732 |
. . . . . . . . . 10
β’
(.rβπ) = (.rβπ) |
61 | 10, 57, 11, 41, 60, 44 | dvdsq1p 25669 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β (Unic1pβπ
)) β (πΊ(β₯rβπ)πΉ β πΉ = ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ))) |
62 | 8, 9, 43, 61 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (πΊ(β₯rβπ)πΉ β πΉ = ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ))) |
63 | 59, 62 | mpbid 231 |
. . . . . . 7
β’ (π β πΉ = ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ)) |
64 | 63 | eqcomd 2738 |
. . . . . 6
β’ (π β ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ) = πΉ) |
65 | 10 | ply1crng 21713 |
. . . . . . . . 9
β’ (π
β CRing β π β CRing) |
66 | 19, 65 | syl 17 |
. . . . . . . 8
β’ (π β π β CRing) |
67 | | crngring 20061 |
. . . . . . . 8
β’ (π β CRing β π β Ring) |
68 | 66, 67 | syl 17 |
. . . . . . 7
β’ (π β π β Ring) |
69 | 10, 11, 36 | mon1pcl 25653 |
. . . . . . . 8
β’ (πΊ β
(Monic1pβπ
) β πΊ β π΅) |
70 | 40, 69 | syl 17 |
. . . . . . 7
β’ (π β πΊ β π΅) |
71 | 11, 60, 52 | ringlz 20100 |
. . . . . . 7
β’ ((π β Ring β§ πΊ β π΅) β ( 0 (.rβπ)πΊ) = 0 ) |
72 | 68, 70, 71 | syl2anc 584 |
. . . . . 6
β’ (π β ( 0 (.rβπ)πΊ) = 0 ) |
73 | 55, 64, 72 | 3netr4d 3018 |
. . . . 5
β’ (π β ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ) β ( 0 (.rβπ)πΊ)) |
74 | | oveq1 7412 |
. . . . . 6
β’ ((πΉ(quot1pβπ
)πΊ) = 0 β ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ) = ( 0 (.rβπ)πΊ)) |
75 | 74 | necon3i 2973 |
. . . . 5
β’ (((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ) β ( 0 (.rβπ)πΊ) β (πΉ(quot1pβπ
)πΊ) β 0 ) |
76 | 73, 75 | syl 17 |
. . . 4
β’ (π β (πΉ(quot1pβπ
)πΊ) β 0 ) |
77 | 37, 10, 52, 11 | deg1nn0cl 25597 |
. . . 4
β’ ((π
β Ring β§ (πΉ(quot1pβπ
)πΊ) β π΅ β§ (πΉ(quot1pβπ
)πΊ) β 0 ) β (π·β(πΉ(quot1pβπ
)πΊ)) β
β0) |
78 | 8, 46, 76, 77 | syl3anc 1371 |
. . 3
β’ (π β (π·β(πΉ(quot1pβπ
)πΊ)) β
β0) |
79 | 78 | nn0cnd 12530 |
. 2
β’ (π β (π·β(πΉ(quot1pβπ
)πΊ)) β β) |
80 | 48 | nn0cnd 12530 |
. 2
β’ (π β π β β) |
81 | 11, 60 | crngcom 20067 |
. . . . . . 7
β’ ((π β CRing β§ (πΉ(quot1pβπ
)πΊ) β π΅ β§ πΊ β π΅) β ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ) = (πΊ(.rβπ)(πΉ(quot1pβπ
)πΊ))) |
82 | 66, 46, 70, 81 | syl3anc 1371 |
. . . . . 6
β’ (π β ((πΉ(quot1pβπ
)πΊ)(.rβπ)πΊ) = (πΊ(.rβπ)(πΉ(quot1pβπ
)πΊ))) |
83 | 63, 82 | eqtrd 2772 |
. . . . 5
β’ (π β πΉ = (πΊ(.rβπ)(πΉ(quot1pβπ
)πΊ))) |
84 | 83 | fveq2d 6892 |
. . . 4
β’ (π β (π·βπΉ) = (π·β(πΊ(.rβπ)(πΉ(quot1pβπ
)πΊ)))) |
85 | | eqid 2732 |
. . . . 5
β’
(RLRegβπ
) =
(RLRegβπ
) |
86 | 39 | simp2d 1143 |
. . . . . . 7
β’ (π β (π·βπΊ) = 1) |
87 | | 1nn0 12484 |
. . . . . . 7
β’ 1 β
β0 |
88 | 86, 87 | eqeltrdi 2841 |
. . . . . 6
β’ (π β (π·βπΊ) β
β0) |
89 | 37, 10, 52, 11 | deg1nn0clb 25599 |
. . . . . . 7
β’ ((π
β Ring β§ πΊ β π΅) β (πΊ β 0 β (π·βπΊ) β
β0)) |
90 | 8, 70, 89 | syl2anc 584 |
. . . . . 6
β’ (π β (πΊ β 0 β (π·βπΊ) β
β0)) |
91 | 88, 90 | mpbird 256 |
. . . . 5
β’ (π β πΊ β 0 ) |
92 | | eqid 2732 |
. . . . . . . 8
β’
(Unitβπ
) =
(Unitβπ
) |
93 | 85, 92 | unitrrg 20901 |
. . . . . . 7
β’ (π
β Ring β
(Unitβπ
) β
(RLRegβπ
)) |
94 | 8, 93 | syl 17 |
. . . . . 6
β’ (π β (Unitβπ
) β (RLRegβπ
)) |
95 | 37, 92, 41 | uc1pldg 25657 |
. . . . . . 7
β’ (πΊ β
(Unic1pβπ
)
β ((coe1βπΊ)β(π·βπΊ)) β (Unitβπ
)) |
96 | 43, 95 | syl 17 |
. . . . . 6
β’ (π β
((coe1βπΊ)β(π·βπΊ)) β (Unitβπ
)) |
97 | 94, 96 | sseldd 3982 |
. . . . 5
β’ (π β
((coe1βπΊ)β(π·βπΊ)) β (RLRegβπ
)) |
98 | 37, 10, 85, 11, 60, 52, 8, 70, 91, 97, 46, 76 | deg1mul2 25623 |
. . . 4
β’ (π β (π·β(πΊ(.rβπ)(πΉ(quot1pβπ
)πΊ))) = ((π·βπΊ) + (π·β(πΉ(quot1pβπ
)πΊ)))) |
99 | 84, 47, 98 | 3eqtr3d 2780 |
. . 3
β’ (π β (π + 1) = ((π·βπΊ) + (π·β(πΉ(quot1pβπ
)πΊ)))) |
100 | | ax-1cn 11164 |
. . . 4
β’ 1 β
β |
101 | | addcom 11396 |
. . . 4
β’ ((π β β β§ 1 β
β) β (π + 1) =
(1 + π)) |
102 | 80, 100, 101 | sylancl 586 |
. . 3
β’ (π β (π + 1) = (1 + π)) |
103 | 86 | oveq1d 7420 |
. . 3
β’ (π β ((π·βπΊ) + (π·β(πΉ(quot1pβπ
)πΊ))) = (1 + (π·β(πΉ(quot1pβπ
)πΊ)))) |
104 | 99, 102, 103 | 3eqtr3rd 2781 |
. 2
β’ (π β (1 + (π·β(πΉ(quot1pβπ
)πΊ))) = (1 + π)) |
105 | 1, 79, 80, 104 | addcanad 11415 |
1
β’ (π β (π·β(πΉ(quot1pβπ
)πΊ)) = π) |