Step | Hyp | Ref
| Expression |
1 | | n0i 3920 |
. 2
⊢ (𝑋 ∈ 𝑄 → ¬ 𝑄 = ∅) |
2 | | pf1rcl.q |
. . . 4
⊢ 𝑄 = ran
(eval1‘𝑅) |
3 | | eqid 2622 |
. . . . . 6
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
4 | | eqid 2622 |
. . . . . 6
⊢
(1𝑜 eval 𝑅) = (1𝑜 eval 𝑅) |
5 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | 3, 4, 5 | evl1fval 19692 |
. . . . 5
⊢
(eval1‘𝑅) = ((𝑥 ∈ ((Base‘𝑅) ↑𝑚
((Base‘𝑅)
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑅)) |
7 | 6 | rneqi 5352 |
. . . 4
⊢ ran
(eval1‘𝑅)
= ran ((𝑥 ∈
((Base‘𝑅)
↑𝑚 ((Base‘𝑅) ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑅)) |
8 | | rnco2 5642 |
. . . 4
⊢ ran
((𝑥 ∈
((Base‘𝑅)
↑𝑚 ((Base‘𝑅) ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑅)) = ((𝑥 ∈ ((Base‘𝑅) ↑𝑚
((Base‘𝑅)
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) “ ran
(1𝑜 eval 𝑅)) |
9 | 2, 7, 8 | 3eqtri 2648 |
. . 3
⊢ 𝑄 = ((𝑥 ∈ ((Base‘𝑅) ↑𝑚
((Base‘𝑅)
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) “ ran
(1𝑜 eval 𝑅)) |
10 | | inss2 3834 |
. . . . 5
⊢ (dom
(𝑥 ∈
((Base‘𝑅)
↑𝑚 ((Base‘𝑅) ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∩ ran
(1𝑜 eval 𝑅)) ⊆ ran (1𝑜 eval
𝑅) |
11 | | neq0 3930 |
. . . . . . 7
⊢ (¬
ran (1𝑜 eval 𝑅) = ∅ ↔ ∃𝑥 𝑥 ∈ ran (1𝑜 eval 𝑅)) |
12 | 4, 5 | evlval 19524 |
. . . . . . . . . . 11
⊢
(1𝑜 eval 𝑅) = ((1𝑜 evalSub 𝑅)‘(Base‘𝑅)) |
13 | 12 | rneqi 5352 |
. . . . . . . . . 10
⊢ ran
(1𝑜 eval 𝑅) = ran ((1𝑜 evalSub
𝑅)‘(Base‘𝑅)) |
14 | 13 | mpfrcl 19518 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran
(1𝑜 eval 𝑅) → (1𝑜 ∈ V
∧ 𝑅 ∈ CRing ∧
(Base‘𝑅) ∈
(SubRing‘𝑅))) |
15 | 14 | simp2d 1074 |
. . . . . . . 8
⊢ (𝑥 ∈ ran
(1𝑜 eval 𝑅) → 𝑅 ∈ CRing) |
16 | 15 | exlimiv 1858 |
. . . . . . 7
⊢
(∃𝑥 𝑥 ∈ ran
(1𝑜 eval 𝑅) → 𝑅 ∈ CRing) |
17 | 11, 16 | sylbi 207 |
. . . . . 6
⊢ (¬
ran (1𝑜 eval 𝑅) = ∅ → 𝑅 ∈ CRing) |
18 | 17 | con1i 144 |
. . . . 5
⊢ (¬
𝑅 ∈ CRing → ran
(1𝑜 eval 𝑅) = ∅) |
19 | | sseq0 3975 |
. . . . 5
⊢ (((dom
(𝑥 ∈
((Base‘𝑅)
↑𝑚 ((Base‘𝑅) ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∩ ran
(1𝑜 eval 𝑅)) ⊆ ran (1𝑜 eval
𝑅) ∧ ran
(1𝑜 eval 𝑅) = ∅) → (dom (𝑥 ∈ ((Base‘𝑅) ↑𝑚
((Base‘𝑅)
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∩ ran
(1𝑜 eval 𝑅)) = ∅) |
20 | 10, 18, 19 | sylancr 695 |
. . . 4
⊢ (¬
𝑅 ∈ CRing → (dom
(𝑥 ∈
((Base‘𝑅)
↑𝑚 ((Base‘𝑅) ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∩ ran
(1𝑜 eval 𝑅)) = ∅) |
21 | | imadisj 5484 |
. . . 4
⊢ (((𝑥 ∈ ((Base‘𝑅) ↑𝑚
((Base‘𝑅)
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) “ ran
(1𝑜 eval 𝑅)) = ∅ ↔ (dom (𝑥 ∈ ((Base‘𝑅) ↑𝑚
((Base‘𝑅)
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) ∩ ran
(1𝑜 eval 𝑅)) = ∅) |
22 | 20, 21 | sylibr 224 |
. . 3
⊢ (¬
𝑅 ∈ CRing →
((𝑥 ∈
((Base‘𝑅)
↑𝑚 ((Base‘𝑅) ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1𝑜 ×
{𝑦})))) “ ran
(1𝑜 eval 𝑅)) = ∅) |
23 | 9, 22 | syl5eq 2668 |
. 2
⊢ (¬
𝑅 ∈ CRing → 𝑄 = ∅) |
24 | 1, 23 | nsyl2 142 |
1
⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) |