Step | Hyp | Ref
| Expression |
1 | | n0i 4298 |
. 2
β’ (π β π β Β¬ π = β
) |
2 | | pf1rcl.q |
. . . 4
β’ π = ran
(eval1βπ
) |
3 | | eqid 2737 |
. . . . . 6
β’
(eval1βπ
) = (eval1βπ
) |
4 | | eqid 2737 |
. . . . . 6
β’
(1o eval π
) = (1o eval π
) |
5 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
6 | 3, 4, 5 | evl1fval 21710 |
. . . . 5
β’
(eval1βπ
) = ((π₯ β ((Baseβπ
) βm ((Baseβπ
) βm
1o)) β¦ (π₯
β (π¦ β
(Baseβπ
) β¦
(1o Γ {π¦})))) β (1o eval π
)) |
7 | 6 | rneqi 5897 |
. . . 4
β’ ran
(eval1βπ
)
= ran ((π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β
(1o eval π
)) |
8 | | rnco2 6210 |
. . . 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 2769 |
. . 3
β’ π = ((π₯ β ((Baseβπ
) βm ((Baseβπ
) βm
1o)) β¦ (π₯
β (π¦ β
(Baseβπ
) β¦
(1o Γ {π¦})))) β ran (1o eval π
)) |
10 | | inss2 4194 |
. . . . 5
β’ (dom
(π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β© ran
(1o eval π
))
β ran (1o eval π
) |
11 | | neq0 4310 |
. . . . . . 7
β’ (Β¬
ran (1o eval π
)
= β
β βπ₯
π₯ β ran (1o
eval π
)) |
12 | 4, 5 | evlval 21521 |
. . . . . . . . . . 11
β’
(1o eval π
) = ((1o evalSub π
)β(Baseβπ
)) |
13 | 12 | rneqi 5897 |
. . . . . . . . . 10
β’ ran
(1o eval π
) =
ran ((1o evalSub π
)β(Baseβπ
)) |
14 | 13 | mpfrcl 21511 |
. . . . . . . . 9
β’ (π₯ β ran (1o eval
π
) β (1o
β V β§ π
β
CRing β§ (Baseβπ
)
β (SubRingβπ
))) |
15 | 14 | simp2d 1144 |
. . . . . . . 8
β’ (π₯ β ran (1o eval
π
) β π
β CRing) |
16 | 15 | exlimiv 1934 |
. . . . . . 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 4364 |
. . . . 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 588 |
. . . 4
β’ (Β¬
π
β CRing β (dom
(π₯ β
((Baseβπ
)
βm ((Baseβπ
) βm 1o)) β¦
(π₯ β (π¦ β (Baseβπ
) β¦ (1o Γ
{π¦})))) β© ran
(1o eval π
)) =
β
) |
21 | | imadisj 6037 |
. . . 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 2789 |
. 2
β’ (Β¬
π
β CRing β π = β
) |
24 | 1, 23 | nsyl2 141 |
1
β’ (π β π β π
β CRing) |