Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
β’ (π β π) |
2 | | evls1muld.m |
. . . . . 6
β’ (π β π β π΅) |
3 | | evls1muld.n |
. . . . . 6
β’ (π β π β π΅) |
4 | | eqid 2733 |
. . . . . . 7
β’
(Poly1βπ) = (Poly1βπ) |
5 | | ressply1evl.u |
. . . . . . 7
β’ π = (π βΎs π
) |
6 | | ressply1evl.w |
. . . . . . 7
β’ π = (Poly1βπ) |
7 | | ressply1evl.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
8 | | evls1muld.r |
. . . . . . 7
β’ (π β π
β (SubRingβπ)) |
9 | | eqid 2733 |
. . . . . . 7
β’
((Poly1βπ) βΎs π΅) = ((Poly1βπ) βΎs π΅) |
10 | 4, 5, 6, 7, 8, 9 | ressply1mul 21625 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(.rβπ)π) = (π(.rβ((Poly1βπ) βΎs π΅))π)) |
11 | 1, 2, 3, 10 | syl12anc 836 |
. . . . 5
β’ (π β (π(.rβπ)π) = (π(.rβ((Poly1βπ) βΎs π΅))π)) |
12 | | evls1muld.1 |
. . . . . 6
β’ Γ =
(.rβπ) |
13 | 12 | oveqi 7374 |
. . . . 5
β’ (π Γ π) = (π(.rβπ)π) |
14 | 7 | fvexi 6860 |
. . . . . . 7
β’ π΅ β V |
15 | | eqid 2733 |
. . . . . . . 8
β’
(.rβ(Poly1βπ)) =
(.rβ(Poly1βπ)) |
16 | 9, 15 | ressmulr 17196 |
. . . . . . 7
β’ (π΅ β V β
(.rβ(Poly1βπ)) =
(.rβ((Poly1βπ) βΎs π΅))) |
17 | 14, 16 | ax-mp 5 |
. . . . . 6
β’
(.rβ(Poly1βπ)) =
(.rβ((Poly1βπ) βΎs π΅)) |
18 | 17 | oveqi 7374 |
. . . . 5
β’ (π(.rβ(Poly1βπ))π) = (π(.rβ((Poly1βπ) βΎs π΅))π) |
19 | 11, 13, 18 | 3eqtr4g 2798 |
. . . 4
β’ (π β (π Γ π) = (π(.rβ(Poly1βπ))π)) |
20 | 19 | fveq2d 6850 |
. . 3
β’ (π β
((eval1βπ)β(π Γ π)) = ((eval1βπ)β(π(.rβ(Poly1βπ))π))) |
21 | 20 | fveq1d 6848 |
. 2
β’ (π β
(((eval1βπ)β(π Γ π))βπΆ) = (((eval1βπ)β(π(.rβ(Poly1βπ))π))βπΆ)) |
22 | | ressply1evl.q |
. . . . . 6
β’ π = (π evalSub1 π
) |
23 | | ressply1evl.k |
. . . . . 6
β’ πΎ = (Baseβπ) |
24 | | eqid 2733 |
. . . . . 6
β’
(eval1βπ) = (eval1βπ) |
25 | | evls1muld.s |
. . . . . 6
β’ (π β π β CRing) |
26 | 22, 23, 6, 5, 7, 24,
25, 8 | ressply1evl 32328 |
. . . . 5
β’ (π β π = ((eval1βπ) βΎ π΅)) |
27 | 26 | fveq1d 6848 |
. . . 4
β’ (π β (πβ(π Γ π)) = (((eval1βπ) βΎ π΅)β(π Γ π))) |
28 | 5 | subrgring 20267 |
. . . . . . 7
β’ (π
β (SubRingβπ) β π β Ring) |
29 | 6 | ply1ring 21642 |
. . . . . . 7
β’ (π β Ring β π β Ring) |
30 | 8, 28, 29 | 3syl 18 |
. . . . . 6
β’ (π β π β Ring) |
31 | 7, 12, 30, 2, 3 | ringcld 19994 |
. . . . 5
β’ (π β (π Γ π) β π΅) |
32 | 31 | fvresd 6866 |
. . . 4
β’ (π β
(((eval1βπ) βΎ π΅)β(π Γ π)) = ((eval1βπ)β(π Γ π))) |
33 | 27, 32 | eqtr2d 2774 |
. . 3
β’ (π β
((eval1βπ)β(π Γ π)) = (πβ(π Γ π))) |
34 | 33 | fveq1d 6848 |
. 2
β’ (π β
(((eval1βπ)β(π Γ π))βπΆ) = ((πβ(π Γ π))βπΆ)) |
35 | | eqid 2733 |
. . . 4
β’
(Baseβ(Poly1βπ)) =
(Baseβ(Poly1βπ)) |
36 | | evls1muld.c |
. . . 4
β’ (π β πΆ β πΎ) |
37 | | eqid 2733 |
. . . . . . . 8
β’
(PwSer1βπ) = (PwSer1βπ) |
38 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(PwSer1βπ)) =
(Baseβ(PwSer1βπ)) |
39 | 4, 5, 6, 7, 8, 37,
38, 35 | ressply1bas2 21622 |
. . . . . . 7
β’ (π β π΅ =
((Baseβ(PwSer1βπ)) β©
(Baseβ(Poly1βπ)))) |
40 | | inss2 4193 |
. . . . . . 7
β’
((Baseβ(PwSer1βπ)) β©
(Baseβ(Poly1βπ))) β
(Baseβ(Poly1βπ)) |
41 | 39, 40 | eqsstrdi 4002 |
. . . . . 6
β’ (π β π΅ β
(Baseβ(Poly1βπ))) |
42 | 41, 2 | sseldd 3949 |
. . . . 5
β’ (π β π β
(Baseβ(Poly1βπ))) |
43 | 26 | fveq1d 6848 |
. . . . . . 7
β’ (π β (πβπ) = (((eval1βπ) βΎ π΅)βπ)) |
44 | 2 | fvresd 6866 |
. . . . . . 7
β’ (π β
(((eval1βπ) βΎ π΅)βπ) = ((eval1βπ)βπ)) |
45 | 43, 44 | eqtr2d 2774 |
. . . . . 6
β’ (π β
((eval1βπ)βπ) = (πβπ)) |
46 | 45 | fveq1d 6848 |
. . . . 5
β’ (π β
(((eval1βπ)βπ)βπΆ) = ((πβπ)βπΆ)) |
47 | 42, 46 | jca 513 |
. . . 4
β’ (π β (π β
(Baseβ(Poly1βπ)) β§ (((eval1βπ)βπ)βπΆ) = ((πβπ)βπΆ))) |
48 | 41, 3 | sseldd 3949 |
. . . . 5
β’ (π β π β
(Baseβ(Poly1βπ))) |
49 | 26 | fveq1d 6848 |
. . . . . . 7
β’ (π β (πβπ) = (((eval1βπ) βΎ π΅)βπ)) |
50 | 3 | fvresd 6866 |
. . . . . . 7
β’ (π β
(((eval1βπ) βΎ π΅)βπ) = ((eval1βπ)βπ)) |
51 | 49, 50 | eqtr2d 2774 |
. . . . . 6
β’ (π β
((eval1βπ)βπ) = (πβπ)) |
52 | 51 | fveq1d 6848 |
. . . . 5
β’ (π β
(((eval1βπ)βπ)βπΆ) = ((πβπ)βπΆ)) |
53 | 48, 52 | jca 513 |
. . . 4
β’ (π β (π β
(Baseβ(Poly1βπ)) β§ (((eval1βπ)βπ)βπΆ) = ((πβπ)βπΆ))) |
54 | | evls1muld.2 |
. . . 4
β’ Β· =
(.rβπ) |
55 | 24, 4, 23, 35, 25, 36, 47, 53, 15, 54 | evl1muld 21732 |
. . 3
β’ (π β ((π(.rβ(Poly1βπ))π) β (Baseβ(Poly1βπ)) β§
(((eval1βπ)β(π(.rβ(Poly1βπ))π))βπΆ) = (((πβπ)βπΆ) Β· ((πβπ)βπΆ)))) |
56 | 55 | simprd 497 |
. 2
β’ (π β
(((eval1βπ)β(π(.rβ(Poly1βπ))π))βπΆ) = (((πβπ)βπΆ) Β· ((πβπ)βπΆ))) |
57 | 21, 34, 56 | 3eqtr3d 2781 |
1
β’ (π β ((πβ(π Γ π))βπΆ) = (((πβπ)βπΆ) Β· ((πβπ)βπΆ))) |