Step | Hyp | Ref
| Expression |
1 | | deg1mhm.p |
. . . . . 6
β’ π = (Poly1βπ
) |
2 | 1 | ply1domn 25504 |
. . . . 5
β’ (π
β Domn β π β Domn) |
3 | | deg1mhm.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
4 | | deg1mhm.z |
. . . . . . 7
β’ 0 =
(0gβπ) |
5 | | eqid 2737 |
. . . . . . 7
β’
(mulGrpβπ) =
(mulGrpβπ) |
6 | 3, 4, 5 | isdomn3 41560 |
. . . . . 6
β’ (π β Domn β (π β Ring β§ (π΅ β { 0 }) β
(SubMndβ(mulGrpβπ)))) |
7 | 6 | simprbi 498 |
. . . . 5
β’ (π β Domn β (π΅ β { 0 }) β
(SubMndβ(mulGrpβπ))) |
8 | 2, 7 | syl 17 |
. . . 4
β’ (π
β Domn β (π΅ β { 0 }) β
(SubMndβ(mulGrpβπ))) |
9 | | deg1mhm.y |
. . . . 5
β’ π = ((mulGrpβπ) βΎs (π΅ β { 0 })) |
10 | 9 | submmnd 18631 |
. . . 4
β’ ((π΅ β { 0 }) β
(SubMndβ(mulGrpβπ)) β π β Mnd) |
11 | 8, 10 | syl 17 |
. . 3
β’ (π
β Domn β π β Mnd) |
12 | | nn0subm 20868 |
. . . 4
β’
β0 β
(SubMndββfld) |
13 | | deg1mhm.n |
. . . . 5
β’ π = (βfld
βΎs β0) |
14 | 13 | submmnd 18631 |
. . . 4
β’
(β0 β (SubMndββfld) β
π β
Mnd) |
15 | 12, 14 | mp1i 13 |
. . 3
β’ (π
β Domn β π β Mnd) |
16 | 11, 15 | jca 513 |
. 2
β’ (π
β Domn β (π β Mnd β§ π β Mnd)) |
17 | | deg1mhm.d |
. . . . . . . 8
β’ π· = ( deg1
βπ
) |
18 | 17, 1, 3 | deg1xrf 25462 |
. . . . . . 7
β’ π·:π΅βΆβ* |
19 | | ffn 6673 |
. . . . . . 7
β’ (π·:π΅βΆβ* β π· Fn π΅) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
β’ π· Fn π΅ |
21 | | difss 4096 |
. . . . . 6
β’ (π΅ β { 0 }) β π΅ |
22 | | fnssres 6629 |
. . . . . 6
β’ ((π· Fn π΅ β§ (π΅ β { 0 }) β π΅) β (π· βΎ (π΅ β { 0 })) Fn (π΅ β { 0 })) |
23 | 20, 21, 22 | mp2an 691 |
. . . . 5
β’ (π· βΎ (π΅ β { 0 })) Fn (π΅ β { 0 }) |
24 | 23 | a1i 11 |
. . . 4
β’ (π
β Domn β (π· βΎ (π΅ β { 0 })) Fn (π΅ β { 0 })) |
25 | | fvres 6866 |
. . . . . . 7
β’ (π₯ β (π΅ β { 0 }) β ((π· βΎ (π΅ β { 0 }))βπ₯) = (π·βπ₯)) |
26 | 25 | adantl 483 |
. . . . . 6
β’ ((π
β Domn β§ π₯ β (π΅ β { 0 })) β ((π· βΎ (π΅ β { 0 }))βπ₯) = (π·βπ₯)) |
27 | | domnring 20782 |
. . . . . . . 8
β’ (π
β Domn β π
β Ring) |
28 | 27 | adantr 482 |
. . . . . . 7
β’ ((π
β Domn β§ π₯ β (π΅ β { 0 })) β π
β Ring) |
29 | | eldifi 4091 |
. . . . . . . 8
β’ (π₯ β (π΅ β { 0 }) β π₯ β π΅) |
30 | 29 | adantl 483 |
. . . . . . 7
β’ ((π
β Domn β§ π₯ β (π΅ β { 0 })) β π₯ β π΅) |
31 | | eldifsni 4755 |
. . . . . . . 8
β’ (π₯ β (π΅ β { 0 }) β π₯ β 0 ) |
32 | 31 | adantl 483 |
. . . . . . 7
β’ ((π
β Domn β§ π₯ β (π΅ β { 0 })) β π₯ β 0 ) |
33 | 17, 1, 4, 3 | deg1nn0cl 25469 |
. . . . . . 7
β’ ((π
β Ring β§ π₯ β π΅ β§ π₯ β 0 ) β (π·βπ₯) β
β0) |
34 | 28, 30, 32, 33 | syl3anc 1372 |
. . . . . 6
β’ ((π
β Domn β§ π₯ β (π΅ β { 0 })) β (π·βπ₯) β
β0) |
35 | 26, 34 | eqeltrd 2838 |
. . . . 5
β’ ((π
β Domn β§ π₯ β (π΅ β { 0 })) β ((π· βΎ (π΅ β { 0 }))βπ₯) β
β0) |
36 | 35 | ralrimiva 3144 |
. . . 4
β’ (π
β Domn β
βπ₯ β (π΅ β { 0 })((π· βΎ (π΅ β { 0 }))βπ₯) β
β0) |
37 | | ffnfv 7071 |
. . . 4
β’ ((π· βΎ (π΅ β { 0 })):(π΅ β { 0
})βΆβ0 β ((π· βΎ (π΅ β { 0 })) Fn (π΅ β { 0 }) β§ βπ₯ β (π΅ β { 0 })((π· βΎ (π΅ β { 0 }))βπ₯) β
β0)) |
38 | 24, 36, 37 | sylanbrc 584 |
. . 3
β’ (π
β Domn β (π· βΎ (π΅ β { 0 })):(π΅ β { 0
})βΆβ0) |
39 | | eqid 2737 |
. . . . . 6
β’
(RLRegβπ
) =
(RLRegβπ
) |
40 | | eqid 2737 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
41 | 27 | adantr 482 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π
β Ring) |
42 | 29 | ad2antrl 727 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π₯ β π΅) |
43 | 31 | ad2antrl 727 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π₯ β 0 ) |
44 | | simpl 484 |
. . . . . . 7
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π
β Domn) |
45 | | eqid 2737 |
. . . . . . . 8
β’
(coe1βπ₯) = (coe1βπ₯) |
46 | 17, 1, 4, 3, 39, 45 | deg1ldgdomn 25475 |
. . . . . . 7
β’ ((π
β Domn β§ π₯ β π΅ β§ π₯ β 0 ) β
((coe1βπ₯)β(π·βπ₯)) β (RLRegβπ
)) |
47 | 44, 42, 43, 46 | syl3anc 1372 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β
((coe1βπ₯)β(π·βπ₯)) β (RLRegβπ
)) |
48 | | eldifi 4091 |
. . . . . . 7
β’ (π¦ β (π΅ β { 0 }) β π¦ β π΅) |
49 | 48 | ad2antll 728 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π¦ β π΅) |
50 | | eldifsni 4755 |
. . . . . . 7
β’ (π¦ β (π΅ β { 0 }) β π¦ β 0 ) |
51 | 50 | ad2antll 728 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π¦ β 0 ) |
52 | 17, 1, 39, 3, 40, 4, 41, 42, 43, 47, 49, 51 | deg1mul2 25495 |
. . . . 5
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β (π·β(π₯(.rβπ)π¦)) = ((π·βπ₯) + (π·βπ¦))) |
53 | | domnring 20782 |
. . . . . . . . . 10
β’ (π β Domn β π β Ring) |
54 | 2, 53 | syl 17 |
. . . . . . . . 9
β’ (π
β Domn β π β Ring) |
55 | 54 | adantr 482 |
. . . . . . . 8
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π β Ring) |
56 | 3, 40 | ringcl 19988 |
. . . . . . . 8
β’ ((π β Ring β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(.rβπ)π¦) β π΅) |
57 | 55, 42, 49, 56 | syl3anc 1372 |
. . . . . . 7
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β (π₯(.rβπ)π¦) β π΅) |
58 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β π β Domn) |
59 | 3, 40, 4 | domnmuln0 20784 |
. . . . . . . 8
β’ ((π β Domn β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (π₯(.rβπ)π¦) β 0 ) |
60 | 58, 42, 43, 49, 51, 59 | syl122anc 1380 |
. . . . . . 7
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β (π₯(.rβπ)π¦) β 0 ) |
61 | | eldifsn 4752 |
. . . . . . 7
β’ ((π₯(.rβπ)π¦) β (π΅ β { 0 }) β ((π₯(.rβπ)π¦) β π΅ β§ (π₯(.rβπ)π¦) β 0 )) |
62 | 57, 60, 61 | sylanbrc 584 |
. . . . . 6
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β (π₯(.rβπ)π¦) β (π΅ β { 0 })) |
63 | | fvres 6866 |
. . . . . 6
β’ ((π₯(.rβπ)π¦) β (π΅ β { 0 }) β ((π· βΎ (π΅ β { 0 }))β(π₯(.rβπ)π¦)) = (π·β(π₯(.rβπ)π¦))) |
64 | 62, 63 | syl 17 |
. . . . 5
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β ((π· βΎ (π΅ β { 0 }))β(π₯(.rβπ)π¦)) = (π·β(π₯(.rβπ)π¦))) |
65 | | fvres 6866 |
. . . . . . 7
β’ (π¦ β (π΅ β { 0 }) β ((π· βΎ (π΅ β { 0 }))βπ¦) = (π·βπ¦)) |
66 | 25, 65 | oveqan12d 7381 |
. . . . . 6
β’ ((π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 })) β (((π· βΎ (π΅ β { 0 }))βπ₯) + ((π· βΎ (π΅ β { 0 }))βπ¦)) = ((π·βπ₯) + (π·βπ¦))) |
67 | 66 | adantl 483 |
. . . . 5
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β (((π· βΎ (π΅ β { 0 }))βπ₯) + ((π· βΎ (π΅ β { 0 }))βπ¦)) = ((π·βπ₯) + (π·βπ¦))) |
68 | 52, 64, 67 | 3eqtr4d 2787 |
. . . 4
β’ ((π
β Domn β§ (π₯ β (π΅ β { 0 }) β§ π¦ β (π΅ β { 0 }))) β ((π· βΎ (π΅ β { 0 }))β(π₯(.rβπ)π¦)) = (((π· βΎ (π΅ β { 0 }))βπ₯) + ((π· βΎ (π΅ β { 0 }))βπ¦))) |
69 | 68 | ralrimivva 3198 |
. . 3
β’ (π
β Domn β
βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })((π· βΎ (π΅ β { 0 }))β(π₯(.rβπ)π¦)) = (((π· βΎ (π΅ β { 0 }))βπ₯) + ((π· βΎ (π΅ β { 0 }))βπ¦))) |
70 | | eqid 2737 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
71 | 3, 70 | ringidcl 19996 |
. . . . . . 7
β’ (π β Ring β
(1rβπ)
β π΅) |
72 | 54, 71 | syl 17 |
. . . . . 6
β’ (π
β Domn β
(1rβπ)
β π΅) |
73 | | domnnzr 20781 |
. . . . . . 7
β’ (π β Domn β π β NzRing) |
74 | 70, 4 | nzrnz 20746 |
. . . . . . 7
β’ (π β NzRing β
(1rβπ)
β 0
) |
75 | 2, 73, 74 | 3syl 18 |
. . . . . 6
β’ (π
β Domn β
(1rβπ)
β 0
) |
76 | | eldifsn 4752 |
. . . . . 6
β’
((1rβπ) β (π΅ β { 0 }) β
((1rβπ)
β π΅ β§
(1rβπ)
β 0
)) |
77 | 72, 75, 76 | sylanbrc 584 |
. . . . 5
β’ (π
β Domn β
(1rβπ)
β (π΅ β { 0
})) |
78 | | fvres 6866 |
. . . . 5
β’
((1rβπ) β (π΅ β { 0 }) β ((π· βΎ (π΅ β { 0
}))β(1rβπ)) = (π·β(1rβπ))) |
79 | 77, 78 | syl 17 |
. . . 4
β’ (π
β Domn β ((π· βΎ (π΅ β { 0
}))β(1rβπ)) = (π·β(1rβπ))) |
80 | 5, 70 | ringidval 19922 |
. . . . . . 7
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
81 | 9, 80 | subm0 18633 |
. . . . . 6
β’ ((π΅ β { 0 }) β
(SubMndβ(mulGrpβπ)) β (1rβπ) = (0gβπ)) |
82 | 8, 81 | syl 17 |
. . . . 5
β’ (π
β Domn β
(1rβπ) =
(0gβπ)) |
83 | 82 | fveq2d 6851 |
. . . 4
β’ (π
β Domn β ((π· βΎ (π΅ β { 0
}))β(1rβπ)) = ((π· βΎ (π΅ β { 0
}))β(0gβπ))) |
84 | | domnnzr 20781 |
. . . . 5
β’ (π
β Domn β π
β NzRing) |
85 | | eqid 2737 |
. . . . . . 7
β’
(Monic1pβπ
) = (Monic1pβπ
) |
86 | 1, 70, 85, 17 | mon1pid 41561 |
. . . . . 6
β’ (π
β NzRing β
((1rβπ)
β (Monic1pβπ
) β§ (π·β(1rβπ)) = 0)) |
87 | 86 | simprd 497 |
. . . . 5
β’ (π
β NzRing β (π·β(1rβπ)) = 0) |
88 | 84, 87 | syl 17 |
. . . 4
β’ (π
β Domn β (π·β(1rβπ)) = 0) |
89 | 79, 83, 88 | 3eqtr3d 2785 |
. . 3
β’ (π
β Domn β ((π· βΎ (π΅ β { 0
}))β(0gβπ)) = 0) |
90 | 38, 69, 89 | 3jca 1129 |
. 2
β’ (π
β Domn β ((π· βΎ (π΅ β { 0 })):(π΅ β { 0
})βΆβ0 β§ βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })((π· βΎ (π΅ β { 0 }))β(π₯(.rβπ)π¦)) = (((π· βΎ (π΅ β { 0 }))βπ₯) + ((π· βΎ (π΅ β { 0 }))βπ¦)) β§ ((π· βΎ (π΅ β { 0
}))β(0gβπ)) = 0)) |
91 | 5, 3 | mgpbas 19909 |
. . . . 5
β’ π΅ =
(Baseβ(mulGrpβπ)) |
92 | 9, 91 | ressbas2 17127 |
. . . 4
β’ ((π΅ β { 0 }) β π΅ β (π΅ β { 0 }) = (Baseβπ)) |
93 | 21, 92 | ax-mp 5 |
. . 3
β’ (π΅ β { 0 }) = (Baseβπ) |
94 | | nn0sscn 12425 |
. . . 4
β’
β0 β β |
95 | | cnfldbas 20816 |
. . . . 5
β’ β =
(Baseββfld) |
96 | 13, 95 | ressbas2 17127 |
. . . 4
β’
(β0 β β β β0 =
(Baseβπ)) |
97 | 94, 96 | ax-mp 5 |
. . 3
β’
β0 = (Baseβπ) |
98 | 3 | fvexi 6861 |
. . . . 5
β’ π΅ β V |
99 | | difexg 5289 |
. . . . 5
β’ (π΅ β V β (π΅ β { 0 }) β
V) |
100 | 98, 99 | ax-mp 5 |
. . . 4
β’ (π΅ β { 0 }) β
V |
101 | 5, 40 | mgpplusg 19907 |
. . . . 5
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
102 | 9, 101 | ressplusg 17178 |
. . . 4
β’ ((π΅ β { 0 }) β V β
(.rβπ) =
(+gβπ)) |
103 | 100, 102 | ax-mp 5 |
. . 3
β’
(.rβπ) = (+gβπ) |
104 | | nn0ex 12426 |
. . . 4
β’
β0 β V |
105 | | cnfldadd 20817 |
. . . . 5
β’ + =
(+gββfld) |
106 | 13, 105 | ressplusg 17178 |
. . . 4
β’
(β0 β V β + = (+gβπ)) |
107 | 104, 106 | ax-mp 5 |
. . 3
β’ + =
(+gβπ) |
108 | | eqid 2737 |
. . 3
β’
(0gβπ) = (0gβπ) |
109 | | cnfld0 20837 |
. . . . 5
β’ 0 =
(0gββfld) |
110 | 13, 109 | subm0 18633 |
. . . 4
β’
(β0 β (SubMndββfld) β
0 = (0gβπ)) |
111 | 12, 110 | ax-mp 5 |
. . 3
β’ 0 =
(0gβπ) |
112 | 93, 97, 103, 107, 108, 111 | ismhm 18610 |
. 2
β’ ((π· βΎ (π΅ β { 0 })) β (π MndHom π) β ((π β Mnd β§ π β Mnd) β§ ((π· βΎ (π΅ β { 0 })):(π΅ β { 0
})βΆβ0 β§ βπ₯ β (π΅ β { 0 })βπ¦ β (π΅ β { 0 })((π· βΎ (π΅ β { 0 }))β(π₯(.rβπ)π¦)) = (((π· βΎ (π΅ β { 0 }))βπ₯) + ((π· βΎ (π΅ β { 0 }))βπ¦)) β§ ((π· βΎ (π΅ β { 0
}))β(0gβπ)) = 0))) |
113 | 16, 90, 112 | sylanbrc 584 |
1
β’ (π
β Domn β (π· βΎ (π΅ β { 0 })) β (π MndHom π)) |