Step | Hyp | Ref
| Expression |
1 | | crngring 19362 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | | zartop.1 |
. . . . 5
⊢ 𝑆 = (Spec‘𝑅) |
3 | | zartop.2 |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝑆) |
4 | | eqid 2759 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
5 | 2, 3, 4 | zar0ring 31334 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅}) |
6 | 1, 5 | sylan 584 |
. . 3
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅}) |
7 | | 0cmp 22079 |
. . 3
⊢ {∅}
∈ Comp |
8 | 6, 7 | eqeltrdi 2859 |
. 2
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) = 1) → 𝐽 ∈ Comp) |
9 | 2, 3 | zartop 31332 |
. . 3
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top) |
10 | | zarcmplem.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
11 | | fvex 6664 |
. . . . . . . . . . . . . . . 16
⊢
(LIdeal‘𝑅)
∈ V |
12 | 11 | mptex 6970 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ∈ V |
13 | 10, 12 | eqeltri 2847 |
. . . . . . . . . . . . . 14
⊢ 𝑉 ∈ V |
14 | | imaexg 7618 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ V → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ V) |
15 | 13, 14 | mp1i 13 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ V) |
16 | | suppssdm 7844 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑎 |
17 | | imass2 5930 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 supp (0g‘𝑅)) ⊆ dom 𝑎 → (𝑉 “ (𝑎 supp (0g‘𝑅))) ⊆ (𝑉 “ dom 𝑎)) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ⊆ (𝑉 “ dom 𝑎)) |
19 | 10 | funmpt2 6367 |
. . . . . . . . . . . . . . 15
⊢ Fun 𝑉 |
20 | | ssidd 3911 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 ⊆ dom 𝑎) |
21 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → 𝑎 ∈ ((Base‘𝑅) ↑m (◡𝑉 “ 𝑥))) |
22 | | fvexd 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (Base‘𝑅) ∈ V) |
23 | 13 | cnvex 7628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ◡𝑉 ∈ V |
24 | 23 | imaex 7619 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝑉 “ 𝑥) ∈ V |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (◡𝑉 “ 𝑥) ∈ V) |
26 | 22, 25 | elmapd 8423 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (𝑎 ∈ ((Base‘𝑅) ↑m (◡𝑉 “ 𝑥)) ↔ 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅))) |
27 | 21, 26 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅)) |
28 | 27 | fdmd 6501 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → dom 𝑎 = (◡𝑉 “ 𝑥)) |
29 | 28 | adantr 485 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 = (◡𝑉 “ 𝑥)) |
30 | 20, 29 | sseqtrd 3928 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 ⊆ (◡𝑉 “ 𝑥)) |
31 | | funimass2 6411 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝑉 ∧ dom 𝑎 ⊆ (◡𝑉 “ 𝑥)) → (𝑉 “ dom 𝑎) ⊆ 𝑥) |
32 | 19, 30, 31 | sylancr 591 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ dom 𝑎) ⊆ 𝑥) |
33 | 18, 32 | sstrd 3898 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ⊆ 𝑥) |
34 | 15, 33 | elpwd 4495 |
. . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ 𝒫 𝑥) |
35 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑎 finSupp (0g‘𝑅)) |
36 | 35 | fsuppimpd 8858 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ∈ Fin) |
37 | | imafi 8835 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑉 ∧ (𝑎 supp (0g‘𝑅)) ∈ Fin) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ Fin) |
38 | 19, 36, 37 | sylancr 591 |
. . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ Fin) |
39 | 34, 38 | elind 4095 |
. . . . . . . . . . 11
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ (𝒫 𝑥 ∩ Fin)) |
40 | | inteq 4834 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑉 “ (𝑎 supp (0g‘𝑅))) → ∩
𝑦 = ∩ (𝑉
“ (𝑎 supp
(0g‘𝑅)))) |
41 | 40 | eqeq2d 2770 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑉 “ (𝑎 supp (0g‘𝑅))) → (∅ = ∩ 𝑦
↔ ∅ = ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))))) |
42 | 41 | adantl 486 |
. . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑦 = (𝑉 “ (𝑎 supp (0g‘𝑅)))) → (∅ = ∩ 𝑦
↔ ∅ = ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))))) |
43 | 16, 29 | sseqtrid 3940 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ (◡𝑉 “ 𝑥)) |
44 | | cnvimass 5914 |
. . . . . . . . . . . . . 14
⊢ (◡𝑉 “ 𝑥) ⊆ dom 𝑉 |
45 | 43, 44 | sstrdi 3900 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑉) |
46 | | intimafv 30552 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑉 ∧ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑉) → ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))) = ∩
𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙)) |
47 | 19, 45, 46 | sylancr 591 |
. . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))) = ∩
𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙)) |
48 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑅 ∈
CRing) |
49 | 48 | crngringd 19363 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑅 ∈
Ring) |
50 | 49 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑅 ∈ Ring) |
51 | | fvex 6664 |
. . . . . . . . . . . . . . . 16
⊢
(PrmIdeal‘𝑅)
∈ V |
52 | 51 | rabex 5195 |
. . . . . . . . . . . . . . 15
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} ∈ V |
53 | 52, 10 | dmmpti 6468 |
. . . . . . . . . . . . . 14
⊢ dom 𝑉 = (LIdeal‘𝑅) |
54 | 45, 53 | sseqtrdi 3938 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ (LIdeal‘𝑅)) |
55 | | simp-7r 790 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (♯‘(Base‘𝑅)) ≠ 1) |
56 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(1r‘𝑅) =
(𝑅
Σg 𝑎)) |
57 | | res0 5820 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ↾ ∅) =
∅ |
58 | 57 | oveq2i 7154 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 Σg
(𝑎 ↾ ∅)) =
(𝑅
Σg ∅) |
59 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘𝑅) = (0g‘𝑅) |
60 | 59 | gsum0 17945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 Σg
∅) = (0g‘𝑅) |
61 | 58, 60 | eqtri 2782 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Σg
(𝑎 ↾ ∅)) =
(0g‘𝑅) |
62 | | ringcmn 19387 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
63 | 1, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd) |
64 | 63 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → 𝑅 ∈ CMnd) |
65 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (◡𝑉 “ 𝑥) ∈ V) |
66 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅)) |
67 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑎 supp (0g‘𝑅)) = ∅) |
68 | | ssidd 3911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → ∅ ⊆
∅) |
69 | 67, 68 | eqsstrd 3926 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑎 supp (0g‘𝑅)) ⊆ ∅) |
70 | 35 | adantr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → 𝑎 finSupp (0g‘𝑅)) |
71 | 4, 59, 64, 65, 66, 69, 70 | gsumres 19086 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑅 Σg (𝑎 ↾ ∅)) = (𝑅 Σg
𝑎)) |
72 | 61, 71 | syl5reqr 2809 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑅 Σg 𝑎) = (0g‘𝑅)) |
73 | 56, 72 | eqtr2d 2795 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(0g‘𝑅) =
(1r‘𝑅)) |
74 | | eqid 2759 |
. . . . . . . . . . . . . . . . . 18
⊢
(1r‘𝑅) = (1r‘𝑅) |
75 | 4, 59, 74 | 01eq0ring 20098 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝑅) =
(1r‘𝑅))
→ (Base‘𝑅) =
{(0g‘𝑅)}) |
76 | 50, 73, 75 | syl2an2r 685 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (Base‘𝑅) = {(0g‘𝑅)}) |
77 | 76 | fveq2d 6655 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(♯‘(Base‘𝑅)) =
(♯‘{(0g‘𝑅)})) |
78 | | fvex 6664 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) ∈ V |
79 | | hashsng 13765 |
. . . . . . . . . . . . . . . 16
⊢
((0g‘𝑅) ∈ V →
(♯‘{(0g‘𝑅)}) = 1) |
80 | 78, 79 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(♯‘{(0g‘𝑅)}) = 1 |
81 | 77, 80 | eqtrdi 2810 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(♯‘(Base‘𝑅)) = 1) |
82 | 55, 81 | mteqand 3052 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ≠ ∅) |
83 | | eqid 2759 |
. . . . . . . . . . . . . 14
⊢
(RSpan‘𝑅) =
(RSpan‘𝑅) |
84 | 10, 83 | zarclsiin 31327 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝑎 supp (0g‘𝑅)) ⊆ (LIdeal‘𝑅) ∧ (𝑎 supp (0g‘𝑅)) ≠ ∅) → ∩ 𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))))) |
85 | 50, 54, 82, 84 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∩
𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))))) |
86 | | nfv 1916 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑙((((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) |
87 | | nfra1 3145 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑙∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 |
88 | 86, 87 | nfan 1901 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑙(((((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) |
89 | 54 | sselda 3888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0g‘𝑅))) → 𝑙 ∈ (LIdeal‘𝑅)) |
90 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
91 | 4, 90 | lidlss 20036 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ (LIdeal‘𝑅) → 𝑙 ⊆ (Base‘𝑅)) |
92 | 89, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0g‘𝑅))) → 𝑙 ⊆ (Base‘𝑅)) |
93 | 92 | ex 417 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑙 ∈ (𝑎 supp (0g‘𝑅)) → 𝑙 ⊆ (Base‘𝑅))) |
94 | 88, 93 | ralrimi 3142 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∀𝑙 ∈ (𝑎 supp (0g‘𝑅))𝑙 ⊆ (Base‘𝑅)) |
95 | | unissb 4825 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ (𝑎
supp (0g‘𝑅)) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (𝑎 supp (0g‘𝑅))𝑙 ⊆ (Base‘𝑅)) |
96 | 94, 95 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∪ (𝑎 supp (0g‘𝑅)) ⊆ (Base‘𝑅)) |
97 | 83, 4, 90 | rspcl 20048 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ ∪ (𝑎
supp (0g‘𝑅)) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅)) |
98 | 50, 96, 97 | syl2anc 588 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅)) |
99 | 4, 90 | lidlss 20036 |
. . . . . . . . . . . . . . . 16
⊢
(((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅))) ⊆ (Base‘𝑅)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ⊆ (Base‘𝑅)) |
101 | 83, 4, 74 | rsp1 20050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring →
((RSpan‘𝑅)‘{(1r‘𝑅)}) = (Base‘𝑅)) |
102 | 50, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1r‘𝑅)}) = (Base‘𝑅)) |
103 | 27 | adantr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅)) |
104 | 103, 43 | fssresd 6523 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g‘𝑅))):(𝑎 supp (0g‘𝑅))⟶(Base‘𝑅)) |
105 | | fvex 6664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑅)
∈ V |
106 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 supp (0g‘𝑅)) ∈ V |
107 | 105, 106 | elmap 8446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ↾ (𝑎 supp (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅))) ↔ (𝑎 ↾ (𝑎 supp (0g‘𝑅))):(𝑎 supp (0g‘𝑅))⟶(Base‘𝑅)) |
108 | 104, 107 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅)))) |
109 | | breq1 5028 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (𝑏 finSupp (0g‘𝑅) ↔ (𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅))) |
110 | | oveq2 7151 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (𝑅 Σg 𝑏) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅))))) |
111 | 110 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → ((1r‘𝑅) = (𝑅 Σg 𝑏) ↔
(1r‘𝑅) =
(𝑅
Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))))) |
112 | | fveq1 6650 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (𝑏‘𝑘) = ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘)) |
113 | 112 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → ((𝑏‘𝑘) ∈ 𝑘 ↔ ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘)) |
114 | 113 | ralbidv 3124 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘 ↔ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘)) |
115 | 109, 111,
114 | 3anbi123d 1434 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → ((𝑏 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘) ↔ ((𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘))) |
116 | 115 | adantl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) → ((𝑏 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘) ↔ ((𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘))) |
117 | | fvexd 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (0g‘𝑅) ∈ V) |
118 | 35, 117 | fsuppres 8876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅)) |
119 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1r‘𝑅) = (𝑅 Σg 𝑎)) |
120 | 50, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑅 ∈ CMnd) |
121 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (◡𝑉 “ 𝑥) ∈ V) |
122 | | ssidd 3911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ (𝑎 supp (0g‘𝑅))) |
123 | 4, 59, 120, 121, 103, 122, 35 | gsumres 19086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) = (𝑅 Σg 𝑎)) |
124 | 119, 123 | eqtr4d 2797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1r‘𝑅) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅))))) |
125 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → 𝑘 ∈ (𝑎 supp (0g‘𝑅))) |
126 | 125 | fvresd 6671 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) = (𝑎‘𝑘)) |
127 | 16, 28 | sseqtrid 3940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (𝑎 supp (0g‘𝑅)) ⊆ (◡𝑉 “ 𝑥)) |
128 | 127 | sselda 3888 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → 𝑘 ∈ (◡𝑉 “ 𝑥)) |
129 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 = 𝑘 → (𝑎‘𝑙) = (𝑎‘𝑘)) |
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘) |
131 | 129, 130 | eleq12d 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙 = 𝑘 → ((𝑎‘𝑙) ∈ 𝑙 ↔ (𝑎‘𝑘) ∈ 𝑘)) |
132 | 131 | adantl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) ∧ 𝑙 = 𝑘) → ((𝑎‘𝑙) ∈ 𝑙 ↔ (𝑎‘𝑘) ∈ 𝑘)) |
133 | 128, 132 | rspcdv 3531 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → (∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 → (𝑎‘𝑘) ∈ 𝑘)) |
134 | 133 | imp 411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎‘𝑘) ∈ 𝑘) |
135 | 134 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → (𝑎‘𝑘) ∈ 𝑘) |
136 | 126, 135 | eqeltrd 2851 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘) |
137 | 136 | ralrimiva 3111 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘) |
138 | 118, 124,
137 | 3jca 1126 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘)) |
139 | 108, 116,
138 | rspcedvd 3542 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∃𝑏 ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅)))(𝑏 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘)) |
140 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(.r‘𝑅) = (.r‘𝑅) |
141 | 83, 4, 59, 140, 50, 54 | elrspunidl 31112 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅))) ↔ ∃𝑏 ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅)))(𝑏 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘))) |
142 | 139, 141 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) |
143 | 142 | snssd 4692 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → {(1r‘𝑅)} ⊆ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) |
144 | 83, 90 | rspssp 20052 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧
((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅) ∧
{(1r‘𝑅)}
⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) → ((RSpan‘𝑅)‘{(1r‘𝑅)}) ⊆ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) |
145 | 50, 98, 143, 144 | syl3anc 1369 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1r‘𝑅)}) ⊆ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) |
146 | 102, 145 | eqsstrrd 3927 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (Base‘𝑅) ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) |
147 | 100, 146 | eqssd 3905 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) = (Base‘𝑅)) |
148 | 147 | fveq2d 6655 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) = (𝑉‘(Base‘𝑅))) |
149 | 90, 4 | lidl1 20046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ∈
(LIdeal‘𝑅)) |
150 | 1, 149 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) ∈
(LIdeal‘𝑅)) |
151 | 10, 4 | zarcls1 31325 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ CRing ∧
(Base‘𝑅) ∈
(LIdeal‘𝑅)) →
((𝑉‘(Base‘𝑅)) = ∅ ↔
(Base‘𝑅) =
(Base‘𝑅))) |
152 | 150, 151 | mpdan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → ((𝑉‘(Base‘𝑅)) = ∅ ↔
(Base‘𝑅) =
(Base‘𝑅))) |
153 | 4, 152 | mpbiri 261 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ CRing → (𝑉‘(Base‘𝑅)) = ∅) |
154 | 153 | ad7antr 738 |
. . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘(Base‘𝑅)) = ∅) |
155 | 148, 154 | eqtrd 2794 |
. . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) = ∅) |
156 | 47, 85, 155 | 3eqtrrd 2799 |
. . . . . . . . . . 11
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∅ = ∩ (𝑉
“ (𝑎 supp
(0g‘𝑅)))) |
157 | 39, 42, 156 | rspcedvd 3542 |
. . . . . . . . . 10
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦) |
158 | 157 | exp41 439 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) → (𝑎 finSupp (0g‘𝑅) →
((1r‘𝑅) =
(𝑅
Σg 𝑎) → (∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)))) |
159 | 158 | 3imp2 1347 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ (𝑎 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦) |
160 | 4, 74 | ringidcl 19374 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
161 | 49, 160 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (1r‘𝑅) ∈ (Base‘𝑅)) |
162 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ∈
𝒫 (Clsd‘𝐽)) |
163 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . 19
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) |
164 | 2, 3, 163, 10 | zartopn 31331 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ CRing → (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) ∧ ran 𝑉 = (Clsd‘𝐽))) |
165 | 164 | simprd 500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ CRing → ran 𝑉 = (Clsd‘𝐽)) |
166 | 48, 165 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ran 𝑉 =
(Clsd‘𝐽)) |
167 | 166 | pweqd 4506 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝒫 ran 𝑉 = 𝒫 (Clsd‘𝐽)) |
168 | 162, 167 | eleqtrrd 2854 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ∈
𝒫 ran 𝑉) |
169 | 168 | elpwid 4498 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ⊆
ran 𝑉) |
170 | | intimafv 30552 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝑉 ∧ (◡𝑉 “ 𝑥) ⊆ dom 𝑉) → ∩ (𝑉 “ (◡𝑉 “ 𝑥)) = ∩
𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙)) |
171 | 19, 44, 170 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ ∩ (𝑉
“ (◡𝑉 “ 𝑥)) = ∩
𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) |
172 | | funimacnv 6409 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑉 → (𝑉 “ (◡𝑉 “ 𝑥)) = (𝑥 ∩ ran 𝑉)) |
173 | 19, 172 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 “ (◡𝑉 “ 𝑥)) = (𝑥 ∩ ran 𝑉) |
174 | | df-ss 3871 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ⊆ ran 𝑉 ↔ (𝑥 ∩ ran 𝑉) = 𝑥) |
175 | 174 | biimpi 219 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ ran 𝑉 → (𝑥 ∩ ran 𝑉) = 𝑥) |
176 | 173, 175 | syl5eq 2806 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ ran 𝑉 → (𝑉 “ (◡𝑉 “ 𝑥)) = 𝑥) |
177 | 176 | inteqd 4836 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ran 𝑉 → ∩ (𝑉 “ (◡𝑉 “ 𝑥)) = ∩ 𝑥) |
178 | 171, 177 | syl5eqr 2808 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ran 𝑉 → ∩
𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) = ∩ 𝑥) |
179 | 169, 178 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∩ 𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) = ∩ 𝑥) |
180 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (◡𝑉 “ 𝑥) ⊆ dom 𝑉) |
181 | 180, 53 | sseqtrdi 3938 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (◡𝑉 “ 𝑥) ⊆ (LIdeal‘𝑅)) |
182 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → Fun 𝑉) |
183 | | inteq 4834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ∅ → ∩ 𝑥 =
∩ ∅) |
184 | | int0 4845 |
. . . . . . . . . . . . . . . . . 18
⊢ ∩ ∅ = V |
185 | 183, 184 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ → ∩ 𝑥 =
V) |
186 | | vn0 4233 |
. . . . . . . . . . . . . . . . . 18
⊢ V ≠
∅ |
187 | | neeq1 3011 |
. . . . . . . . . . . . . . . . . 18
⊢ (∩ 𝑥 =
V → (∩ 𝑥 ≠ ∅ ↔ V ≠
∅)) |
188 | 186, 187 | mpbiri 261 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ 𝑥 =
V → ∩ 𝑥 ≠ ∅) |
189 | 185, 188 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → ∩ 𝑥
≠ ∅) |
190 | 189 | necon2i 2983 |
. . . . . . . . . . . . . . 15
⊢ (∩ 𝑥 =
∅ → 𝑥 ≠
∅) |
191 | 190 | adantl 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ≠
∅) |
192 | | preiman0 30551 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝑉 ∧ 𝑥 ⊆ ran 𝑉 ∧ 𝑥 ≠ ∅) → (◡𝑉 “ 𝑥) ≠ ∅) |
193 | 182, 169,
191, 192 | syl3anc 1369 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (◡𝑉 “ 𝑥) ≠ ∅) |
194 | 10, 83 | zarclsiin 31327 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (◡𝑉 “ 𝑥) ⊆ (LIdeal‘𝑅) ∧ (◡𝑉 “ 𝑥) ≠ ∅) → ∩ 𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)))) |
195 | 49, 181, 193, 194 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∩ 𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)))) |
196 | | simpr 489 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∩ 𝑥 = ∅) |
197 | 179, 195,
196 | 3eqtr3d 2802 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) = ∅) |
198 | 181 | sselda 3888 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑙 ∈
(◡𝑉 “ 𝑥)) → 𝑙 ∈ (LIdeal‘𝑅)) |
199 | 198, 91 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑙 ∈
(◡𝑉 “ 𝑥)) → 𝑙 ⊆ (Base‘𝑅)) |
200 | 199 | ralrimiva 3111 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∀𝑙
∈ (◡𝑉 “ 𝑥)𝑙 ⊆ (Base‘𝑅)) |
201 | | unissb 4825 |
. . . . . . . . . . . . . 14
⊢ (∪ (◡𝑉 “ 𝑥) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (◡𝑉 “ 𝑥)𝑙 ⊆ (Base‘𝑅)) |
202 | 200, 201 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∪ (◡𝑉 “ 𝑥) ⊆ (Base‘𝑅)) |
203 | 83, 4, 90 | rspcl 20048 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ ∪ (◡𝑉 “ 𝑥) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) |
204 | 49, 202, 203 | syl2anc 588 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) |
205 | 10, 4 | zarcls1 31325 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧
((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) → ((𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) = (Base‘𝑅))) |
206 | 48, 204, 205 | syl2anc 588 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) = (Base‘𝑅))) |
207 | 197, 206 | mpbid 235 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) = (Base‘𝑅)) |
208 | 161, 207 | eleqtrrd 2854 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) |
209 | 83, 4, 59, 140, 49, 181 | elrspunidl 31112 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ↔ ∃𝑎 ∈ ((Base‘𝑅) ↑m (◡𝑉 “ 𝑥))(𝑎 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙))) |
210 | 208, 209 | mpbid 235 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∃𝑎
∈ ((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))(𝑎 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)) |
211 | 159, 210 | r19.29a 3211 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∃𝑦
∈ (𝒫 𝑥 ∩
Fin)∅ = ∩ 𝑦) |
212 | | 0ex 5170 |
. . . . . . . 8
⊢ ∅
∈ V |
213 | | vex 3411 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
214 | | elfi 8895 |
. . . . . . . 8
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ (∅ ∈ (fi‘𝑥) ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)) |
215 | 212, 213,
214 | mp2an 692 |
. . . . . . 7
⊢ (∅
∈ (fi‘𝑥) ↔
∃𝑦 ∈ (𝒫
𝑥 ∩ Fin)∅ = ∩ 𝑦) |
216 | 211, 215 | sylibr 237 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∅ ∈ (fi‘𝑥)) |
217 | 216 | ex 417 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (∩ 𝑥 =
∅ → ∅ ∈ (fi‘𝑥))) |
218 | 217 | necon3bd 2963 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (¬ ∅ ∈
(fi‘𝑥) → ∩ 𝑥
≠ ∅)) |
219 | 218 | ralrimiva 3111 |
. . 3
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) → ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈
(fi‘𝑥) → ∩ 𝑥
≠ ∅)) |
220 | | cmpfi 22093 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔
∀𝑥 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑥)
→ ∩ 𝑥 ≠ ∅))) |
221 | 220 | biimpar 482 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑥)
→ ∩ 𝑥 ≠ ∅)) → 𝐽 ∈ Comp) |
222 | 9, 219, 221 | syl2an2r 685 |
. 2
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) → 𝐽 ∈ Comp) |
223 | 8, 222 | pm2.61dane 3036 |
1
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp) |