Step | Hyp | Ref
| Expression |
1 | | ne0i 4298 |
. . 3
β’ (π β ran ((πΌ evalSub π)βπ
) β ran ((πΌ evalSub π)βπ
) β β
) |
2 | | mpfrcl.q |
. . 3
β’ π = ran ((πΌ evalSub π)βπ
) |
3 | 1, 2 | eleq2s 2852 |
. 2
β’ (π β π β ran ((πΌ evalSub π)βπ
) β β
) |
4 | | rneq 5895 |
. . . 4
β’ (((πΌ evalSub π)βπ
) = β
β ran ((πΌ evalSub π)βπ
) = ran β
) |
5 | | rn0 5885 |
. . . 4
β’ ran
β
= β
|
6 | 4, 5 | eqtrdi 2789 |
. . 3
β’ (((πΌ evalSub π)βπ
) = β
β ran ((πΌ evalSub π)βπ
) = β
) |
7 | 6 | necon3i 2973 |
. 2
β’ (ran
((πΌ evalSub π)βπ
) β β
β ((πΌ evalSub π)βπ
) β β
) |
8 | | fveq1 6845 |
. . . . . . 7
β’ ((πΌ evalSub π) = β
β ((πΌ evalSub π)βπ
) = (β
βπ
)) |
9 | | 0fv 6890 |
. . . . . . 7
β’
(β
βπ
) =
β
|
10 | 8, 9 | eqtrdi 2789 |
. . . . . 6
β’ ((πΌ evalSub π) = β
β ((πΌ evalSub π)βπ
) = β
) |
11 | 10 | necon3i 2973 |
. . . . 5
β’ (((πΌ evalSub π)βπ
) β β
β (πΌ evalSub π) β β
) |
12 | | reldmevls 21517 |
. . . . . . . 8
β’ Rel dom
evalSub |
13 | 12 | ovprc1 7400 |
. . . . . . 7
β’ (Β¬
πΌ β V β (πΌ evalSub π) = β
) |
14 | 13 | necon1ai 2968 |
. . . . . 6
β’ ((πΌ evalSub π) β β
β πΌ β V) |
15 | | n0 4310 |
. . . . . . 7
β’ ((πΌ evalSub π) β β
β βπ π β (πΌ evalSub π)) |
16 | | df-evls 21505 |
. . . . . . . . . 10
β’ evalSub
= (π β V, π β CRing β¦
β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) |
17 | 16 | elmpocl2 7601 |
. . . . . . . . 9
β’ (π β (πΌ evalSub π) β π β CRing) |
18 | 17 | a1d 25 |
. . . . . . . 8
β’ (π β (πΌ evalSub π) β (πΌ β V β π β CRing)) |
19 | 18 | exlimiv 1934 |
. . . . . . 7
β’
(βπ π β (πΌ evalSub π) β (πΌ β V β π β CRing)) |
20 | 15, 19 | sylbi 216 |
. . . . . 6
β’ ((πΌ evalSub π) β β
β (πΌ β V β π β CRing)) |
21 | 14, 20 | jcai 518 |
. . . . 5
β’ ((πΌ evalSub π) β β
β (πΌ β V β§ π β CRing)) |
22 | 11, 21 | syl 17 |
. . . 4
β’ (((πΌ evalSub π)βπ
) β β
β (πΌ β V β§ π β CRing)) |
23 | | fvex 6859 |
. . . . . . . . . . . . 13
β’
(Baseβπ )
β V |
24 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π(SubRingβπ ) |
25 | | nfcsb1v 3884 |
. . . . . . . . . . . . . 14
β’
β²πβ¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) |
26 | 24, 25 | nfmpt 5216 |
. . . . . . . . . . . . 13
β’
β²π(π β (SubRingβπ ) β¦ β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
27 | | csbeq1a 3873 |
. . . . . . . . . . . . . 14
β’ (π = (Baseβπ ) β β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
28 | 27 | mpteq2dv 5211 |
. . . . . . . . . . . . 13
β’ (π = (Baseβπ ) β (π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ ) β¦ β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) |
29 | 23, 26, 28 | csbief 3894 |
. . . . . . . . . . . 12
β’
β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ ) β¦ β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
30 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (SubRingβπ ) = (SubRingβπ)) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π = πΌ β§ π = π) β (SubRingβπ ) = (SubRingβπ)) |
32 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (Baseβπ ) = (Baseβπ)) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π = πΌ β§ π = π) β (Baseβπ ) = (Baseβπ)) |
34 | 33 | csbeq1d 3863 |
. . . . . . . . . . . . . 14
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(Baseβπ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
35 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π = πΌ β π = πΌ) |
36 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π βΎs π) = (π βΎs π)) |
37 | 35, 36 | oveqan12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ ((π = πΌ β§ π = π) β (π mPoly (π βΎs π)) = (πΌ mPoly (π βΎs π))) |
38 | 37 | csbeq1d 3863 |
. . . . . . . . . . . . . . . 16
β’ ((π = πΌ β§ π = π) β β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
39 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β π = π) |
40 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = πΌ β (π βm π) = (π βm πΌ)) |
41 | 39, 40 | oveqan12rd 7381 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = πΌ β§ π = π) β (π βs (π βm π)) = (π βs (π βm πΌ))) |
42 | 41 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = πΌ β§ π = π) β (π€ RingHom (π βs (π βm π))) = (π€ RingHom (π βs (π βm πΌ)))) |
43 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π = πΌ β§ π = π) β (π βm π) = (π βm πΌ)) |
44 | 43 | xpeq1d 5666 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = πΌ β§ π = π) β ((π βm π) Γ {π₯}) = ((π βm πΌ) Γ {π₯})) |
45 | 44 | mpteq2dv 5211 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = πΌ β§ π = π) β (π₯ β π β¦ ((π βm π) Γ {π₯})) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯}))) |
46 | 45 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = πΌ β§ π = π) β ((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β (π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})))) |
47 | 35, 36 | oveqan12d 7380 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = πΌ β§ π = π) β (π mVar (π βΎs π)) = (πΌ mVar (π βΎs π))) |
48 | 47 | coeq2d 5822 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = πΌ β§ π = π) β (π β (π mVar (π βΎs π))) = (π β (πΌ mVar (π βΎs π)))) |
49 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = πΌ β§ π = π) β π = πΌ) |
50 | 43 | mpteq1d 5204 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = πΌ β§ π = π) β (π β (π βm π) β¦ (πβπ₯)) = (π β (π βm πΌ) β¦ (πβπ₯))) |
51 | 49, 50 | mpteq12dv 5200 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = πΌ β§ π = π) β (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))) |
52 | 48, 51 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = πΌ β§ π = π) β ((π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))) β (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯))))) |
53 | 46, 52 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = πΌ β§ π = π) β (((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))) β ((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
54 | 42, 53 | riotaeqbidv 7320 |
. . . . . . . . . . . . . . . . 17
β’ ((π = πΌ β§ π = π) β (β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = (β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
55 | 54 | csbeq2dv 3866 |
. . . . . . . . . . . . . . . 16
β’ ((π = πΌ β§ π = π) β β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
56 | 38, 55 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π = πΌ β§ π = π) β β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
57 | 56 | csbeq2dv 3866 |
. . . . . . . . . . . . . 14
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
58 | 34, 57 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) = β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
59 | 31, 58 | mpteq12dv 5200 |
. . . . . . . . . . . 12
β’ ((π = πΌ β§ π = π) β (π β (SubRingβπ ) β¦ β¦(Baseβπ ) / πβ¦β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯))))))) |
60 | 29, 59 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π = πΌ β§ π = π) β β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯))))))) |
61 | | fvex 6859 |
. . . . . . . . . . . 12
β’
(SubRingβπ)
β V |
62 | 61 | mptex 7177 |
. . . . . . . . . . 11
β’ (π β (SubRingβπ) β¦
β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) β V |
63 | 60, 16, 62 | ovmpoa 7514 |
. . . . . . . . . 10
β’ ((πΌ β V β§ π β CRing) β (πΌ evalSub π) = (π β (SubRingβπ) β¦ β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯))))))) |
64 | 63 | dmeqd 5865 |
. . . . . . . . 9
β’ ((πΌ β V β§ π β CRing) β dom (πΌ evalSub π) = dom (π β (SubRingβπ) β¦ β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯))))))) |
65 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (SubRingβπ) β¦
β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) = (π β (SubRingβπ) β¦ β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) |
66 | 65 | dmmptss 6197 |
. . . . . . . . 9
β’ dom
(π β
(SubRingβπ) β¦
β¦(Baseβπ) / πβ¦β¦(πΌ mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm πΌ)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm πΌ) Γ {π₯})) β§ (π β (πΌ mVar (π βΎs π))) = (π₯ β πΌ β¦ (π β (π βm πΌ) β¦ (πβπ₯)))))) β (SubRingβπ) |
67 | 64, 66 | eqsstrdi 4002 |
. . . . . . . 8
β’ ((πΌ β V β§ π β CRing) β dom (πΌ evalSub π) β (SubRingβπ)) |
68 | 67 | ssneld 3950 |
. . . . . . 7
β’ ((πΌ β V β§ π β CRing) β (Β¬
π
β
(SubRingβπ) β
Β¬ π
β dom (πΌ evalSub π))) |
69 | | ndmfv 6881 |
. . . . . . 7
β’ (Β¬
π
β dom (πΌ evalSub π) β ((πΌ evalSub π)βπ
) = β
) |
70 | 68, 69 | syl6 35 |
. . . . . 6
β’ ((πΌ β V β§ π β CRing) β (Β¬
π
β
(SubRingβπ) β
((πΌ evalSub π)βπ
) = β
)) |
71 | 70 | necon1ad 2957 |
. . . . 5
β’ ((πΌ β V β§ π β CRing) β (((πΌ evalSub π)βπ
) β β
β π
β (SubRingβπ))) |
72 | 71 | com12 32 |
. . . 4
β’ (((πΌ evalSub π)βπ
) β β
β ((πΌ β V β§ π β CRing) β π
β (SubRingβπ))) |
73 | 22, 72 | jcai 518 |
. . 3
β’ (((πΌ evalSub π)βπ
) β β
β ((πΌ β V β§ π β CRing) β§ π
β (SubRingβπ))) |
74 | | df-3an 1090 |
. . 3
β’ ((πΌ β V β§ π β CRing β§ π
β (SubRingβπ)) β ((πΌ β V β§ π β CRing) β§ π
β (SubRingβπ))) |
75 | 73, 74 | sylibr 233 |
. 2
β’ (((πΌ evalSub π)βπ
) β β
β (πΌ β V β§ π β CRing β§ π
β (SubRingβπ))) |
76 | 3, 7, 75 | 3syl 18 |
1
β’ (π β π β (πΌ β V β§ π β CRing β§ π
β (SubRingβπ))) |