Step | Hyp | Ref
| Expression |
1 | | evls1var.x |
. . . 4
β’ π = (var1βπ) |
2 | | eqid 2737 |
. . . . 5
β’
(var1βπ) = (var1βπ) |
3 | | evls1var.r |
. . . . 5
β’ (π β π
β (SubRingβπ)) |
4 | | evls1var.u |
. . . . 5
β’ π = (π βΎs π
) |
5 | 2, 3, 4 | subrgvr1 21648 |
. . . 4
β’ (π β
(var1βπ) =
(var1βπ)) |
6 | 1, 5 | eqtr4id 2796 |
. . 3
β’ (π β π = (var1βπ)) |
7 | 6 | fveq2d 6851 |
. 2
β’ (π β (πβπ) = (πβ(var1βπ))) |
8 | | eqid 2737 |
. . . . . 6
β’
((1o evalSub π)βπ
) = ((1o evalSub π)βπ
) |
9 | | eqid 2737 |
. . . . . 6
β’
(1o eval π) = (1o eval π) |
10 | | eqid 2737 |
. . . . . 6
β’
(1o mVar π) = (1o mVar π) |
11 | | evls1var.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
12 | | 1on 8429 |
. . . . . . 7
β’
1o β On |
13 | 12 | a1i 11 |
. . . . . 6
β’ (π β 1o β
On) |
14 | | evls1var.s |
. . . . . 6
β’ (π β π β CRing) |
15 | | 0lt1o 8455 |
. . . . . . 7
β’ β
β 1o |
16 | 15 | a1i 11 |
. . . . . 6
β’ (π β β
β
1o) |
17 | 8, 9, 10, 4, 11, 13, 14, 3, 16 | evlsvarsrng 21525 |
. . . . 5
β’ (π β (((1o evalSub
π)βπ
)β((1o mVar π)ββ
)) =
((1o eval π)β((1o mVar π)ββ
))) |
18 | 2 | vr1val 21579 |
. . . . . . 7
β’
(var1βπ) = ((1o mVar π)ββ
) |
19 | | eqid 2737 |
. . . . . . . . 9
β’
(1o mVar π) = (1o mVar π) |
20 | 19, 13, 3, 4 | subrgmvr 21450 |
. . . . . . . 8
β’ (π β (1o mVar π) = (1o mVar π)) |
21 | 20 | fveq1d 6849 |
. . . . . . 7
β’ (π β ((1o mVar π)ββ
) =
((1o mVar π)ββ
)) |
22 | 18, 21 | eqtrid 2789 |
. . . . . 6
β’ (π β
(var1βπ) =
((1o mVar π)ββ
)) |
23 | 22 | fveq2d 6851 |
. . . . 5
β’ (π β (((1o evalSub
π)βπ
)β(var1βπ)) = (((1o evalSub
π)βπ
)β((1o mVar π)ββ
))) |
24 | 22 | fveq2d 6851 |
. . . . 5
β’ (π β ((1o eval π)β(var1βπ)) = ((1o eval π)β((1o mVar
π)ββ
))) |
25 | 17, 23, 24 | 3eqtr4d 2787 |
. . . 4
β’ (π β (((1o evalSub
π)βπ
)β(var1βπ)) = ((1o eval π)β(var1βπ))) |
26 | 25 | coeq1d 5822 |
. . 3
β’ (π β ((((1o evalSub
π)βπ
)β(var1βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦}))) = (((1o eval
π)β(var1βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
27 | | eqid 2737 |
. . . . 5
β’
(Poly1βπ) = (Poly1βπ) |
28 | | eqid 2737 |
. . . . . . 7
β’
(Poly1β(π βΎs π
)) = (Poly1β(π βΎs π
)) |
29 | | eqid 2737 |
. . . . . . 7
β’
(PwSer1β(π βΎs π
)) = (PwSer1β(π βΎs π
)) |
30 | 4 | fveq2i 6850 |
. . . . . . . 8
β’
(Poly1βπ) = (Poly1β(π βΎs π
)) |
31 | 30 | fveq2i 6850 |
. . . . . . 7
β’
(Baseβ(Poly1βπ)) =
(Baseβ(Poly1β(π βΎs π
))) |
32 | 28, 29, 31 | ply1bas 21582 |
. . . . . 6
β’
(Baseβ(Poly1βπ)) = (Baseβ(1o mPoly (π βΎs π
))) |
33 | 32 | eqcomi 2746 |
. . . . 5
β’
(Baseβ(1o mPoly (π βΎs π
))) =
(Baseβ(Poly1βπ)) |
34 | 2, 3, 4, 27, 33 | subrgvr1cl 21649 |
. . . 4
β’ (π β
(var1βπ)
β (Baseβ(1o mPoly (π βΎs π
)))) |
35 | | evls1var.q |
. . . . 5
β’ π = (π evalSub1 π
) |
36 | | eqid 2737 |
. . . . 5
β’
(1o evalSub π) = (1o evalSub π) |
37 | | eqid 2737 |
. . . . 5
β’
(1o mPoly (π βΎs π
)) = (1o mPoly (π βΎs π
)) |
38 | | eqid 2737 |
. . . . 5
β’
(Baseβ(1o mPoly (π βΎs π
))) = (Baseβ(1o mPoly
(π βΎs
π
))) |
39 | 35, 36, 11, 37, 38 | evls1val 21702 |
. . . 4
β’ ((π β CRing β§ π
β (SubRingβπ) β§
(var1βπ)
β (Baseβ(1o mPoly (π βΎs π
)))) β (πβ(var1βπ)) = ((((1o evalSub
π)βπ
)β(var1βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
40 | 14, 3, 34, 39 | syl3anc 1372 |
. . 3
β’ (π β (πβ(var1βπ)) = ((((1o evalSub
π)βπ
)β(var1βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
41 | | crngring 19983 |
. . . . 5
β’ (π β CRing β π β Ring) |
42 | | eqid 2737 |
. . . . . 6
β’
(Poly1βπ) = (Poly1βπ) |
43 | | eqid 2737 |
. . . . . . . 8
β’
(PwSer1βπ) = (PwSer1βπ) |
44 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Poly1βπ)) =
(Baseβ(Poly1βπ)) |
45 | 42, 43, 44 | ply1bas 21582 |
. . . . . . 7
β’
(Baseβ(Poly1βπ)) = (Baseβ(1o mPoly π)) |
46 | 45 | eqcomi 2746 |
. . . . . 6
β’
(Baseβ(1o mPoly π)) =
(Baseβ(Poly1βπ)) |
47 | 2, 42, 46 | vr1cl 21604 |
. . . . 5
β’ (π β Ring β
(var1βπ)
β (Baseβ(1o mPoly π))) |
48 | 14, 41, 47 | 3syl 18 |
. . . 4
β’ (π β
(var1βπ)
β (Baseβ(1o mPoly π))) |
49 | | eqid 2737 |
. . . . 5
β’
(eval1βπ) = (eval1βπ) |
50 | | eqid 2737 |
. . . . 5
β’
(1o mPoly π) = (1o mPoly π) |
51 | | eqid 2737 |
. . . . 5
β’
(Baseβ(1o mPoly π)) = (Baseβ(1o mPoly π)) |
52 | 49, 9, 11, 50, 51 | evl1val 21711 |
. . . 4
β’ ((π β CRing β§
(var1βπ)
β (Baseβ(1o mPoly π))) β ((eval1βπ)β(var1βπ)) = (((1o eval π)β(var1βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
53 | 14, 48, 52 | syl2anc 585 |
. . 3
β’ (π β
((eval1βπ)β(var1βπ)) = (((1o eval π)β(var1βπ)) β (π¦ β π΅ β¦ (1o Γ {π¦})))) |
54 | 26, 40, 53 | 3eqtr4d 2787 |
. 2
β’ (π β (πβ(var1βπ)) =
((eval1βπ)β(var1βπ))) |
55 | 49, 2, 11 | evl1var 21718 |
. . 3
β’ (π β CRing β
((eval1βπ)β(var1βπ)) = ( I βΎ π΅)) |
56 | 14, 55 | syl 17 |
. 2
β’ (π β
((eval1βπ)β(var1βπ)) = ( I βΎ π΅)) |
57 | 7, 54, 56 | 3eqtrd 2781 |
1
β’ (π β (πβπ) = ( I βΎ π΅)) |