Step | Hyp | Ref
| Expression |
1 | | ressply.1 |
. . . . . 6
β’ π = (Poly1βπ
) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
4 | | eqid 2733 |
. . . . . 6
β’ (
deg1 βπ
) =
( deg1 βπ
) |
5 | | ressply1mon1p.m |
. . . . . 6
β’ π =
(Monic1pβπ
) |
6 | | eqid 2733 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
7 | 1, 2, 3, 4, 5, 6 | ismon1p 25530 |
. . . . 5
β’ (π β π β (π β (Baseβπ) β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) |
8 | 7 | anbi2i 624 |
. . . 4
β’ ((π β π΅ β§ π β π) β (π β π΅ β§ (π β (Baseβπ) β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
)))) |
9 | | ressply.2 |
. . . . . . . . . . 11
β’ π» = (π
βΎs π) |
10 | | ressply.3 |
. . . . . . . . . . 11
β’ π = (Poly1βπ») |
11 | | ressply.4 |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ) |
12 | | ressply.5 |
. . . . . . . . . . 11
β’ (π β π β (SubRingβπ
)) |
13 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π βΎs π΅) = (π βΎs π΅) |
14 | 1, 9, 10, 11, 12, 13 | ressply1bas 21623 |
. . . . . . . . . 10
β’ (π β π΅ = (Baseβ(π βΎs π΅))) |
15 | 13, 2 | ressbasss 17129 |
. . . . . . . . . 10
β’
(Baseβ(π
βΎs π΅))
β (Baseβπ) |
16 | 14, 15 | eqsstrdi 4002 |
. . . . . . . . 9
β’ (π β π΅ β (Baseβπ)) |
17 | 16 | sseld 3947 |
. . . . . . . 8
β’ (π β (π β π΅ β π β (Baseβπ))) |
18 | 17 | pm4.71d 563 |
. . . . . . 7
β’ (π β (π β π΅ β (π β π΅ β§ π β (Baseβπ)))) |
19 | 18 | anbi1d 631 |
. . . . . 6
β’ (π β ((π β π΅ β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) β ((π β π΅ β§ π β (Baseβπ)) β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))))) |
20 | | 13an22anass 31444 |
. . . . . 6
β’ ((π β π΅ β§ (π β (Baseβπ) β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) β ((π β π΅ β§ π β (Baseβπ)) β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
)))) |
21 | 19, 20 | bitr4di 289 |
. . . . 5
β’ (π β ((π β π΅ β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) β (π β π΅ β§ (π β (Baseβπ) β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))))) |
22 | 1, 9, 10, 11, 12, 3 | ressply10g 32333 |
. . . . . . . . . 10
β’ (π β (0gβπ) = (0gβπ)) |
23 | 22 | neeq2d 3001 |
. . . . . . . . 9
β’ (π β (π β (0gβπ) β π β (0gβπ))) |
24 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (π β (0gβπ) β π β (0gβπ))) |
25 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β π β π΅) |
26 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β π β (SubRingβπ
)) |
27 | 9, 4, 10, 11, 25, 26 | ressdeg1 32331 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (( deg1 βπ
)βπ) = (( deg1 βπ»)βπ)) |
28 | 27 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β ((coe1βπ)β(( deg1
βπ
)βπ)) =
((coe1βπ)β(( deg1 βπ»)βπ))) |
29 | 9, 6 | subrg1 20274 |
. . . . . . . . . . 11
β’ (π β (SubRingβπ
) β
(1rβπ
) =
(1rβπ»)) |
30 | 12, 29 | syl 17 |
. . . . . . . . . 10
β’ (π β (1rβπ
) = (1rβπ»)) |
31 | 30 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (1rβπ
) = (1rβπ»)) |
32 | 28, 31 | eqeq12d 2749 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
) β
((coe1βπ)β(( deg1 βπ»)βπ)) = (1rβπ»))) |
33 | 24, 32 | anbi12d 632 |
. . . . . . 7
β’ ((π β§ π β π΅) β ((π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
)) β (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»)))) |
34 | 33 | pm5.32da 580 |
. . . . . 6
β’ (π β ((π β π΅ β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) β (π β π΅ β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»))))) |
35 | | 3anass 1096 |
. . . . . 6
β’ ((π β π΅ β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»)) β (π β π΅ β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»)))) |
36 | 34, 35 | bitr4di 289 |
. . . . 5
β’ (π β ((π β π΅ β§ (π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) β (π β π΅ β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»)))) |
37 | 21, 36 | bitr3d 281 |
. . . 4
β’ (π β ((π β π΅ β§ (π β (Baseβπ) β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ
)βπ)) = (1rβπ
))) β (π β π΅ β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»)))) |
38 | 8, 37 | bitr2id 284 |
. . 3
β’ (π β ((π β π΅ β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»)) β (π β π΅ β§ π β π))) |
39 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
40 | | eqid 2733 |
. . . 4
β’ (
deg1 βπ») =
( deg1 βπ») |
41 | | ressply1mon1p.n |
. . . 4
β’ π =
(Monic1pβπ») |
42 | | eqid 2733 |
. . . 4
β’
(1rβπ») = (1rβπ») |
43 | 10, 11, 39, 40, 41, 42 | ismon1p 25530 |
. . 3
β’ (π β π β (π β π΅ β§ π β (0gβπ) β§ ((coe1βπ)β(( deg1
βπ»)βπ)) = (1rβπ»))) |
44 | | elin 3930 |
. . 3
β’ (π β (π΅ β© π) β (π β π΅ β§ π β π)) |
45 | 38, 43, 44 | 3bitr4g 314 |
. 2
β’ (π β (π β π β π β (π΅ β© π))) |
46 | 45 | eqrdv 2731 |
1
β’ (π β π = (π΅ β© π)) |