Step | Hyp | Ref
| Expression |
1 | | evlsval.q |
. . . 4
β’ π = ((πΌ evalSub π)βπ
) |
2 | | elex 3477 |
. . . . 5
β’ (πΌ β π β πΌ β V) |
3 | | fveq2 6862 |
. . . . . . . . . 10
β’ (π = π β (Baseβπ ) = (Baseβπ)) |
4 | 3 | adantl 482 |
. . . . . . . . 9
β’ ((π = πΌ β§ π = π) β (Baseβπ ) = (Baseβπ)) |
5 | 4 | csbeq1d 3877 |
. . . . . . . 8
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = β¦(Baseβπ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) |
6 | | fvex 6875 |
. . . . . . . . . 10
β’
(Baseβπ)
β V |
7 | 6 | a1i 11 |
. . . . . . . . 9
β’ ((π = πΌ β§ π = π) β (Baseβπ) β V) |
8 | | simplr 767 |
. . . . . . . . . . 11
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β π = π) |
9 | 8 | fveq2d 6866 |
. . . . . . . . . 10
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β (SubRingβπ ) = (SubRingβπ)) |
10 | | simpll 765 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β π = πΌ) |
11 | | oveq1 7384 |
. . . . . . . . . . . . . 14
β’ (π = π β (π βΎs π) = (π βΎs π)) |
12 | 11 | ad2antlr 725 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β (π βΎs π) = (π βΎs π)) |
13 | 10, 12 | oveq12d 7395 |
. . . . . . . . . . . 12
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β (π mPoly (π βΎs π)) = (πΌ mPoly (π βΎs π))) |
14 | 13 | csbeq1d 3877 |
. . . . . . . . . . 11
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
15 | | ovexd 7412 |
. . . . . . . . . . . 12
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β (πΌ mPoly (π βΎs π)) β V) |
16 | | simprr 771 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β π€ = (πΌ mPoly (π βΎs π))) |
17 | | simplr 767 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β π = π) |
18 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β π = (Baseβπ)) |
19 | | simpll 765 |
. . . . . . . . . . . . . . . . 17
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β π = πΌ) |
20 | 18, 19 | oveq12d 7395 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π βm π) = ((Baseβπ) βm πΌ)) |
21 | 17, 20 | oveq12d 7395 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π βs (π βm π)) = (π βs
((Baseβπ)
βm πΌ))) |
22 | 16, 21 | oveq12d 7395 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π€ RingHom (π βs (π βm π))) = ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))) |
23 | 16 | fveq2d 6866 |
. . . . . . . . . . . . . . . . 17
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (algScβπ€) = (algScβ(πΌ mPoly (π βΎs π)))) |
24 | 23 | coeq2d 5838 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π β (algScβπ€)) = (π β (algScβ(πΌ mPoly (π βΎs π))))) |
25 | 20 | xpeq1d 5682 |
. . . . . . . . . . . . . . . . 17
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β ((π βm π) Γ {π₯}) = (((Baseβπ) βm πΌ) Γ {π₯})) |
26 | 25 | mpteq2dv 5227 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π₯ β π β¦ ((π βm π) Γ {π₯})) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯}))) |
27 | 24, 26 | eqeq12d 2747 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β ((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β (π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})))) |
28 | 17 | oveq1d 7392 |
. . . . . . . . . . . . . . . . . 18
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π βΎs π) = (π βΎs π)) |
29 | 19, 28 | oveq12d 7395 |
. . . . . . . . . . . . . . . . 17
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π mVar (π βΎs π)) = (πΌ mVar (π βΎs π))) |
30 | 29 | coeq2d 5838 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π β (π mVar (π βΎs π))) = (π β (πΌ mVar (π βΎs π)))) |
31 | 20 | mpteq1d 5220 |
. . . . . . . . . . . . . . . . 17
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π β (π βm π) β¦ (πβπ₯)) = (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))) |
32 | 19, 31 | mpteq12dv 5216 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))) |
33 | 30, 32 | eqeq12d 2747 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β ((π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))) β (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))) |
34 | 27, 33 | anbi12d 631 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))) β ((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
35 | 22, 34 | riotaeqbidv 7336 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π = π) β§ (π = (Baseβπ) β§ π€ = (πΌ mPoly (π βΎs π)))) β (β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
36 | 35 | anassrs 468 |
. . . . . . . . . . . 12
β’ ((((π = πΌ β§ π = π) β§ π = (Baseβπ)) β§ π€ = (πΌ mPoly (π βΎs π))) β (β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
37 | 15, 36 | csbied 3911 |
. . . . . . . . . . 11
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
38 | 14, 37 | eqtrd 2771 |
. . . . . . . . . 10
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
39 | 9, 38 | mpteq12dv 5216 |
. . . . . . . . 9
β’ (((π = πΌ β§ π = π) β§ π = (Baseβπ)) β (π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))) |
40 | 7, 39 | csbied 3911 |
. . . . . . . 8
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))) |
41 | 5, 40 | eqtrd 2771 |
. . . . . . 7
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))) |
42 | | df-evls 21534 |
. . . . . . 7
β’ evalSub
= (π β V, π β CRing β¦
β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) |
43 | | fvex 6875 |
. . . . . . . 8
β’
(SubRingβπ)
β V |
44 | 43 | mptex 7193 |
. . . . . . 7
β’ (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) β V |
45 | 41, 42, 44 | ovmpoa 7530 |
. . . . . 6
β’ ((πΌ β V β§ π β CRing) β (πΌ evalSub π) = (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))) |
46 | 45 | fveq1d 6864 |
. . . . 5
β’ ((πΌ β V β§ π β CRing) β ((πΌ evalSub π)βπ
) = ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
)) |
47 | 2, 46 | sylan 580 |
. . . 4
β’ ((πΌ β π β§ π β CRing) β ((πΌ evalSub π)βπ
) = ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
)) |
48 | 1, 47 | eqtrid 2783 |
. . 3
β’ ((πΌ β π β§ π β CRing) β π = ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
)) |
49 | 48 | 3adant3 1132 |
. 2
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π = ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
)) |
50 | | oveq2 7385 |
. . . . . . . 8
β’ (π = π
β (π βΎs π) = (π βΎs π
)) |
51 | 50 | oveq2d 7393 |
. . . . . . 7
β’ (π = π
β (πΌ mPoly (π βΎs π)) = (πΌ mPoly (π βΎs π
))) |
52 | 51 | oveq1d 7392 |
. . . . . 6
β’ (π = π
β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ))) =
((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))) |
53 | 51 | fveq2d 6866 |
. . . . . . . . 9
β’ (π = π
β (algScβ(πΌ mPoly (π βΎs π))) = (algScβ(πΌ mPoly (π βΎs π
)))) |
54 | 53 | coeq2d 5838 |
. . . . . . . 8
β’ (π = π
β (π β (algScβ(πΌ mPoly (π βΎs π)))) = (π β (algScβ(πΌ mPoly (π βΎs π
))))) |
55 | | mpteq1 5218 |
. . . . . . . 8
β’ (π = π
β (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯}))) |
56 | 54, 55 | eqeq12d 2747 |
. . . . . . 7
β’ (π = π
β ((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β (π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})))) |
57 | 50 | oveq2d 7393 |
. . . . . . . . 9
β’ (π = π
β (πΌ mVar (π βΎs π)) = (πΌ mVar (π βΎs π
))) |
58 | 57 | coeq2d 5838 |
. . . . . . . 8
β’ (π = π
β (π β (πΌ mVar (π βΎs π))) = (π β (πΌ mVar (π βΎs π
)))) |
59 | 58 | eqeq1d 2733 |
. . . . . . 7
β’ (π = π
β ((π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))) β (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))) |
60 | 56, 59 | anbi12d 631 |
. . . . . 6
β’ (π = π
β (((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))) β ((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
61 | 52, 60 | riotaeqbidv 7336 |
. . . . 5
β’ (π = π
β (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))) = (β©π β ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
62 | | eqid 2731 |
. . . . 5
β’ (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
63 | | riotaex 7337 |
. . . . 5
β’
(β©π
β ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))) β V |
64 | 61, 62, 63 | fvmpt 6968 |
. . . 4
β’ (π
β (SubRingβπ) β ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
) = (β©π β ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
65 | | evlsval.w |
. . . . . . . . 9
β’ π = (πΌ mPoly π) |
66 | | evlsval.u |
. . . . . . . . . 10
β’ π = (π βΎs π
) |
67 | 66 | oveq2i 7388 |
. . . . . . . . 9
β’ (πΌ mPoly π) = (πΌ mPoly (π βΎs π
)) |
68 | 65, 67 | eqtri 2759 |
. . . . . . . 8
β’ π = (πΌ mPoly (π βΎs π
)) |
69 | | evlsval.t |
. . . . . . . . 9
β’ π = (π βs (π΅ βm πΌ)) |
70 | | evlsval.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ) |
71 | 70 | oveq1i 7387 |
. . . . . . . . . 10
β’ (π΅ βm πΌ) = ((Baseβπ) βm πΌ) |
72 | 71 | oveq2i 7388 |
. . . . . . . . 9
β’ (π βs
(π΅ βm πΌ)) = (π βs
((Baseβπ)
βm πΌ)) |
73 | 69, 72 | eqtri 2759 |
. . . . . . . 8
β’ π = (π βs
((Baseβπ)
βm πΌ)) |
74 | 68, 73 | oveq12i 7389 |
. . . . . . 7
β’ (π RingHom π) = ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ))) |
75 | 74 | a1i 11 |
. . . . . 6
β’ (β€
β (π RingHom π) = ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))) |
76 | | evlsval.a |
. . . . . . . . . . 11
β’ π΄ = (algScβπ) |
77 | 68 | fveq2i 6865 |
. . . . . . . . . . 11
β’
(algScβπ) =
(algScβ(πΌ mPoly
(π βΎs
π
))) |
78 | 76, 77 | eqtri 2759 |
. . . . . . . . . 10
β’ π΄ = (algScβ(πΌ mPoly (π βΎs π
))) |
79 | 78 | coeq2i 5836 |
. . . . . . . . 9
β’ (π β π΄) = (π β (algScβ(πΌ mPoly (π βΎs π
)))) |
80 | | evlsval.x |
. . . . . . . . . 10
β’ π = (π₯ β π
β¦ ((π΅ βm πΌ) Γ {π₯})) |
81 | 71 | xpeq1i 5679 |
. . . . . . . . . . 11
β’ ((π΅ βm πΌ) Γ {π₯}) = (((Baseβπ) βm πΌ) Γ {π₯}) |
82 | 81 | mpteq2i 5230 |
. . . . . . . . . 10
β’ (π₯ β π
β¦ ((π΅ βm πΌ) Γ {π₯})) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) |
83 | 80, 82 | eqtri 2759 |
. . . . . . . . 9
β’ π = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) |
84 | 79, 83 | eqeq12i 2749 |
. . . . . . . 8
β’ ((π β π΄) = π β (π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯}))) |
85 | | evlsval.v |
. . . . . . . . . . 11
β’ π = (πΌ mVar π) |
86 | 66 | oveq2i 7388 |
. . . . . . . . . . 11
β’ (πΌ mVar π) = (πΌ mVar (π βΎs π
)) |
87 | 85, 86 | eqtri 2759 |
. . . . . . . . . 10
β’ π = (πΌ mVar (π βΎs π
)) |
88 | 87 | coeq2i 5836 |
. . . . . . . . 9
β’ (π β π) = (π β (πΌ mVar (π βΎs π
))) |
89 | | evlsval.y |
. . . . . . . . . 10
β’ π = (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) |
90 | | eqid 2731 |
. . . . . . . . . . . 12
β’ (πβπ₯) = (πβπ₯) |
91 | 71, 90 | mpteq12i 5231 |
. . . . . . . . . . 11
β’ (π β (π΅ βm πΌ) β¦ (πβπ₯)) = (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)) |
92 | 91 | mpteq2i 5230 |
. . . . . . . . . 10
β’ (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))) |
93 | 89, 92 | eqtri 2759 |
. . . . . . . . 9
β’ π = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))) |
94 | 88, 93 | eqeq12i 2749 |
. . . . . . . 8
β’ ((π β π) = π β (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))) |
95 | 84, 94 | anbi12i 627 |
. . . . . . 7
β’ (((π β π΄) = π β§ (π β π) = π) β ((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))) |
96 | 95 | a1i 11 |
. . . . . 6
β’ (β€
β (((π β π΄) = π β§ (π β π) = π) β ((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
97 | 75, 96 | riotaeqbidv 7336 |
. . . . 5
β’ (β€
β (β©π
β (π RingHom π)((π β π΄) = π β§ (π β π) = π)) = (β©π β ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯)))))) |
98 | 97 | mptru 1548 |
. . . 4
β’
(β©π
β (π RingHom π)((π β π΄) = π β§ (π β π) = π)) = (β©π β ((πΌ mPoly (π βΎs π
)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π
)))) = (π₯ β π
β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π
))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))) |
99 | 64, 98 | eqtr4di 2789 |
. . 3
β’ (π
β (SubRingβπ) β ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
) = (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π))) |
100 | 99 | 3ad2ant3 1135 |
. 2
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β ((π β (SubRingβπ) β¦ (β©π β ((πΌ mPoly (π βΎs π)) RingHom (π βs
((Baseβπ)
βm πΌ)))((π β (algScβ(πΌ mPoly (π βΎs π)))) = (π₯ β π β¦ (((Baseβπ) βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β ((Baseβπ) βm πΌ) β¦ (πβπ₯))))))βπ
) = (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π))) |
101 | 49, 100 | eqtrd 2771 |
1
β’ ((πΌ β π β§ π β CRing β§ π
β (SubRingβπ)) β π = (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π))) |