| Step | Hyp | Ref
| Expression |
|---|
| 1 | | n0i 4333 |
. 2
β’ (π β π β Β¬ π = β
) |
| 2 | | pf1rcl.q |
. . . 4
β’ π = ran
(eval1βπ
) |
| 3 | | eqid 2732 |
. . . . . 6
β’
(eval1βπ
) = (eval1βπ
) |
| 4 | | eqid 2732 |
. . . . . 6
β’
(1o eval π
) = (1o eval π
) |
| 5 | | eqid 2732 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
| 6 | 3, 4, 5 | evl1fval 22067 |
. . . . 5
β’
(eval1βπ
) = ((π₯ β ((Baseβπ
) βm ((Baseβπ
) βm
1o)) β¦ (π₯
β (π¦ β
(Baseβπ
) β¦
(1o Γ {π¦})))) β (1o eval π
)) |
| 7 | 6 | rneqi 5936 |
. . . 4
β’ ran
(eval1βπ
)
= ran ((π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β
(1o eval π
)) |
| 8 | | rnco2 6252 |
. . . 4
β’ ran
((π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β
(1o eval π
)) =
((π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β ran
(1o eval π
)) |
| 9 | 2, 7, 8 | 3eqtri 2764 |
. . 3
β’ π = ((π₯ β ((Baseβπ
) βm ((Baseβπ
) βm
1o)) β¦ (π₯
β (π¦ β
(Baseβπ
) β¦
(1o Γ {π¦})))) β ran (1o eval π
)) |
| 10 | | inss2 4229 |
. . . . 5
β’ (dom
(π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β© ran
(1o eval π
))
β ran (1o eval π
) |
| 11 | | neq0 4345 |
. . . . . . 7
β’ (Β¬
ran (1o eval π
)
= β
β βπ₯
π₯ β ran (1o
eval π
)) |
| 12 | 4, 5 | evlval 21877 |
. . . . . . . . . . 11
β’
(1o eval π
) = ((1o evalSub π
)β(Baseβπ
)) |
| 13 | 12 | rneqi 5936 |
. . . . . . . . . 10
β’ ran
(1o eval π
) =
ran ((1o evalSub π
)β(Baseβπ
)) |
| 14 | 13 | mpfrcl 21867 |
. . . . . . . . 9
β’ (π₯ β ran (1o eval
π
) β (1o
β V β§ π
β
CRing β§ (Baseβπ
)
β (SubRingβπ
))) |
| 15 | 14 | simp2d 1143 |
. . . . . . . 8
β’ (π₯ β ran (1o eval
π
) β π
β CRing) |
| 16 | 15 | exlimiv 1933 |
. . . . . . 7
β’
(βπ₯ π₯ β ran (1o eval
π
) β π
β CRing) |
| 17 | 11, 16 | sylbi 216 |
. . . . . 6
β’ (Β¬
ran (1o eval π
)
= β
β π
β
CRing) |
| 18 | 17 | con1i 147 |
. . . . 5
β’ (Β¬
π
β CRing β ran
(1o eval π
) =
β
) |
| 19 | | sseq0 4399 |
. . . . 5
β’ (((dom
(π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β© ran
(1o eval π
))
β ran (1o eval π
) β§ ran (1o eval π
) = β
) β (dom (π₯ β ((Baseβπ
) βm
((Baseβπ
)
βm 1o)) β¦ (π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ {π¦})))) β© ran (1o
eval π
)) =
β
) |
| 20 | 10, 18, 19 | sylancr 587 |
. . . 4
β’ (Β¬
π
β CRing β (dom
(π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β© ran
(1o eval π
)) =
β
) |
| 21 | | imadisj 6079 |
. . . 4
β’ (((π₯ β ((Baseβπ
) βm
((Baseβπ
)
βm 1o)) β¦ (π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ {π¦})))) β ran (1o
eval π
)) = β
β
(dom (π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β© ran
(1o eval π
)) =
β
) |
| 22 | 20, 21 | sylibr 233 |
. . 3
β’ (Β¬
π
β CRing β
((π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β ran
(1o eval π
)) =
β
) |
| 23 | 9, 22 | eqtrid 2784 |
. 2
β’ (Β¬
π
β CRing β π = β
) |
| 24 | 1, 23 | nsyl2 141 |
1
β’ (π β π β π
β CRing) |
