Step | Hyp | Ref
| Expression |
1 | | ressply1evl.e |
. . . . . . 7
β’ πΈ = (eval1βπ) |
2 | | ressply1evl.k |
. . . . . . 7
β’ πΎ = (Baseβπ) |
3 | 1, 2 | evl1fval1 21720 |
. . . . . 6
β’ πΈ = (π evalSub1 πΎ) |
4 | | eqid 2733 |
. . . . . 6
β’
(Poly1β(π βΎs πΎ)) = (Poly1β(π βΎs πΎ)) |
5 | | eqid 2733 |
. . . . . 6
β’ (π βΎs πΎ) = (π βΎs πΎ) |
6 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Poly1β(π βΎs πΎ))) =
(Baseβ(Poly1β(π βΎs πΎ))) |
7 | | ressply1evl.s |
. . . . . . 7
β’ (π β π β CRing) |
8 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β π β CRing) |
9 | 7 | crngringd 19985 |
. . . . . . . 8
β’ (π β π β Ring) |
10 | 2 | subrgid 20266 |
. . . . . . . 8
β’ (π β Ring β πΎ β (SubRingβπ)) |
11 | 9, 10 | syl 17 |
. . . . . . 7
β’ (π β πΎ β (SubRingβπ)) |
12 | 11 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β πΎ β (SubRingβπ)) |
13 | | eqid 2733 |
. . . . . . . . . 10
β’
(Poly1βπ) = (Poly1βπ) |
14 | | ressply1evl.u |
. . . . . . . . . 10
β’ π = (π βΎs π
) |
15 | | ressply1evl.w |
. . . . . . . . . 10
β’ π = (Poly1βπ) |
16 | | ressply1evl.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
17 | | ressply1evl.r |
. . . . . . . . . 10
β’ (π β π
β (SubRingβπ)) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(PwSer1βπ) = (PwSer1βπ) |
19 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβ(PwSer1βπ)) =
(Baseβ(PwSer1βπ)) |
20 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβ(Poly1βπ)) =
(Baseβ(Poly1βπ)) |
21 | 13, 14, 15, 16, 17, 18, 19, 20 | ressply1bas2 21622 |
. . . . . . . . 9
β’ (π β π΅ =
((Baseβ(PwSer1βπ)) β©
(Baseβ(Poly1βπ)))) |
22 | | inss2 4193 |
. . . . . . . . 9
β’
((Baseβ(PwSer1βπ)) β©
(Baseβ(Poly1βπ))) β
(Baseβ(Poly1βπ)) |
23 | 21, 22 | eqsstrdi 4002 |
. . . . . . . 8
β’ (π β π΅ β
(Baseβ(Poly1βπ))) |
24 | 2 | ressid 17133 |
. . . . . . . . . . 11
β’ (π β CRing β (π βΎs πΎ) = π) |
25 | 7, 24 | syl 17 |
. . . . . . . . . 10
β’ (π β (π βΎs πΎ) = π) |
26 | 25 | fveq2d 6850 |
. . . . . . . . 9
β’ (π β
(Poly1β(π
βΎs πΎ)) =
(Poly1βπ)) |
27 | 26 | fveq2d 6850 |
. . . . . . . 8
β’ (π β
(Baseβ(Poly1β(π βΎs πΎ))) =
(Baseβ(Poly1βπ))) |
28 | 23, 27 | sseqtrrd 3989 |
. . . . . . 7
β’ (π β π΅ β
(Baseβ(Poly1β(π βΎs πΎ)))) |
29 | 28 | sselda 3948 |
. . . . . 6
β’ ((π β§ π β π΅) β π β
(Baseβ(Poly1β(π βΎs πΎ)))) |
30 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
31 | | eqid 2733 |
. . . . . 6
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
32 | | eqid 2733 |
. . . . . 6
β’
(coe1βπ) = (coe1βπ) |
33 | 3, 2, 4, 5, 6, 8, 12, 29, 30, 31, 32 | evls1fpws 32327 |
. . . . 5
β’ ((π β§ π β π΅) β (πΈβπ) = (π₯ β πΎ β¦ (π Ξ£g (π β β0
β¦ (((coe1βπ)βπ)(.rβπ)(π(.gβ(mulGrpβπ))π₯)))))) |
34 | | ressply1evl.q |
. . . . . 6
β’ π = (π evalSub1 π
) |
35 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β π
β (SubRingβπ)) |
36 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β π΅) β π β π΅) |
37 | 34, 2, 15, 14, 16, 8, 35, 36, 30, 31, 32 | evls1fpws 32327 |
. . . . 5
β’ ((π β§ π β π΅) β (πβπ) = (π₯ β πΎ β¦ (π Ξ£g (π β β0
β¦ (((coe1βπ)βπ)(.rβπ)(π(.gβ(mulGrpβπ))π₯)))))) |
38 | 33, 37 | eqtr4d 2776 |
. . . 4
β’ ((π β§ π β π΅) β (πΈβπ) = (πβπ)) |
39 | 38 | ralrimiva 3140 |
. . 3
β’ (π β βπ β π΅ (πΈβπ) = (πβπ)) |
40 | | eqid 2733 |
. . . . . . 7
β’ (π βs πΎ) = (π βs πΎ) |
41 | 1, 13, 40, 2 | evl1rhm 21721 |
. . . . . 6
β’ (π β CRing β πΈ β
((Poly1βπ)
RingHom (π
βs πΎ))) |
42 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(π
βs πΎ)) = (Baseβ(π βs πΎ)) |
43 | 20, 42 | rhmf 20168 |
. . . . . 6
β’ (πΈ β
((Poly1βπ)
RingHom (π
βs πΎ)) β πΈ:(Baseβ(Poly1βπ))βΆ(Baseβ(π βs πΎ))) |
44 | 7, 41, 43 | 3syl 18 |
. . . . 5
β’ (π β πΈ:(Baseβ(Poly1βπ))βΆ(Baseβ(π βs πΎ))) |
45 | 44 | ffnd 6673 |
. . . 4
β’ (π β πΈ Fn
(Baseβ(Poly1βπ))) |
46 | 34, 2, 40, 14, 15 | evls1rhm 21711 |
. . . . . . 7
β’ ((π β CRing β§ π
β (SubRingβπ)) β π β (π RingHom (π βs πΎ))) |
47 | 7, 17, 46 | syl2anc 585 |
. . . . . 6
β’ (π β π β (π RingHom (π βs πΎ))) |
48 | 16, 42 | rhmf 20168 |
. . . . . 6
β’ (π β (π RingHom (π βs πΎ)) β π:π΅βΆ(Baseβ(π βs πΎ))) |
49 | 47, 48 | syl 17 |
. . . . 5
β’ (π β π:π΅βΆ(Baseβ(π βs πΎ))) |
50 | 49 | ffnd 6673 |
. . . 4
β’ (π β π Fn π΅) |
51 | | fvreseq1 6993 |
. . . 4
β’ (((πΈ Fn
(Baseβ(Poly1βπ)) β§ π Fn π΅) β§ π΅ β
(Baseβ(Poly1βπ))) β ((πΈ βΎ π΅) = π β βπ β π΅ (πΈβπ) = (πβπ))) |
52 | 45, 50, 23, 51 | syl21anc 837 |
. . 3
β’ (π β ((πΈ βΎ π΅) = π β βπ β π΅ (πΈβπ) = (πβπ))) |
53 | 39, 52 | mpbird 257 |
. 2
β’ (π β (πΈ βΎ π΅) = π) |
54 | 53 | eqcomd 2739 |
1
β’ (π β π = (πΈ βΎ π΅)) |