| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | crngring 20243 | . . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 2 |  | zartop.1 | . . . . 5
⊢ 𝑆 = (Spec‘𝑅) | 
| 3 |  | zartop.2 | . . . . 5
⊢ 𝐽 = (TopOpen‘𝑆) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 5 | 2, 3, 4 | zar0ring 33878 | . . . 4
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅}) | 
| 6 | 1, 5 | sylan 580 | . . 3
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅}) | 
| 7 |  | 0cmp 23403 | . . 3
⊢ {∅}
∈ Comp | 
| 8 | 6, 7 | eqeltrdi 2848 | . 2
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) = 1) → 𝐽 ∈ Comp) | 
| 9 | 2, 3 | zartop 33876 | . . 3
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top) | 
| 10 |  | zarcmplem.1 | . . . . . . . . . . . . . . 15
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) | 
| 11 |  | fvex 6918 | . . . . . . . . . . . . . . . 16
⊢
(LIdeal‘𝑅)
∈ V | 
| 12 | 11 | mptex 7244 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ∈ V | 
| 13 | 10, 12 | eqeltri 2836 | . . . . . . . . . . . . . 14
⊢ 𝑉 ∈ V | 
| 14 |  | imaexg 7936 | . . . . . . . . . . . . . 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 8203 | . . . . . . . . . . . . . . 15
⊢ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑎 | 
| 17 |  | imass2 6119 | . . . . . . . . . . . . . . 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 6604 | . . . . . . . . . . . . . . 15
⊢ Fun 𝑉 | 
| 20 |  | ssidd 4006 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 ⊆ dom 𝑎) | 
| 21 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → 𝑎 ∈ ((Base‘𝑅) ↑m (◡𝑉 “ 𝑥))) | 
| 22 |  | fvexd 6920 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (Base‘𝑅) ∈ V) | 
| 23 | 13 | cnvex 7948 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ◡𝑉 ∈ V | 
| 24 | 23 | imaex 7937 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝑉 “ 𝑥) ∈ V | 
| 25 | 24 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (◡𝑉 “ 𝑥) ∈ V) | 
| 26 | 22, 25 | elmapd 8881 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (𝑎 ∈ ((Base‘𝑅) ↑m (◡𝑉 “ 𝑥)) ↔ 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅))) | 
| 27 | 21, 26 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅)) | 
| 28 | 27 | fdmd 6745 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → dom 𝑎 = (◡𝑉 “ 𝑥)) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 = (◡𝑉 “ 𝑥)) | 
| 30 | 20, 29 | sseqtrd 4019 | . . . . . . . . . . . . . . 15
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 ⊆ (◡𝑉 “ 𝑥)) | 
| 31 |  | funimass2 6648 | . . . . . . . . . . . . . . 15
⊢ ((Fun
𝑉 ∧ dom 𝑎 ⊆ (◡𝑉 “ 𝑥)) → (𝑉 “ dom 𝑎) ⊆ 𝑥) | 
| 32 | 19, 30, 31 | sylancr 587 | . . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ dom 𝑎) ⊆ 𝑥) | 
| 33 | 18, 32 | sstrd 3993 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ⊆ 𝑥) | 
| 34 | 15, 33 | elpwd 4605 | . . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ 𝒫 𝑥) | 
| 35 |  | simpllr 775 | . . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑎 finSupp (0g‘𝑅)) | 
| 36 | 35 | fsuppimpd 9410 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ∈ Fin) | 
| 37 |  | imafi 9354 | . . . . . . . . . . . . 13
⊢ ((Fun
𝑉 ∧ (𝑎 supp (0g‘𝑅)) ∈ Fin) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ Fin) | 
| 38 | 19, 36, 37 | sylancr 587 | . . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ Fin) | 
| 39 | 34, 38 | elind 4199 | . . . . . . . . . . 11
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g‘𝑅))) ∈ (𝒫 𝑥 ∩ Fin)) | 
| 40 |  | inteq 4948 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝑉 “ (𝑎 supp (0g‘𝑅))) → ∩
𝑦 = ∩ (𝑉
“ (𝑎 supp
(0g‘𝑅)))) | 
| 41 | 40 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑉 “ (𝑎 supp (0g‘𝑅))) → (∅ = ∩ 𝑦
↔ ∅ = ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))))) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . 11
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑦 = (𝑉 “ (𝑎 supp (0g‘𝑅)))) → (∅ = ∩ 𝑦
↔ ∅ = ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))))) | 
| 43 | 16, 29 | sseqtrid 4025 | . . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ (◡𝑉 “ 𝑥)) | 
| 44 |  | cnvimass 6099 | . . . . . . . . . . . . . 14
⊢ (◡𝑉 “ 𝑥) ⊆ dom 𝑉 | 
| 45 | 43, 44 | sstrdi 3995 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑉) | 
| 46 |  | intimafv 32721 | . . . . . . . . . . . . 13
⊢ ((Fun
𝑉 ∧ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑉) → ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))) = ∩
𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙)) | 
| 47 | 19, 45, 46 | sylancr 587 | . . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∩ (𝑉 “ (𝑎 supp (0g‘𝑅))) = ∩
𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙)) | 
| 48 |  | simplll 774 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑅 ∈
CRing) | 
| 49 | 48 | crngringd 20244 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑅 ∈
Ring) | 
| 50 | 49 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑅 ∈ Ring) | 
| 51 |  | fvex 6918 | . . . . . . . . . . . . . . . 16
⊢
(PrmIdeal‘𝑅)
∈ V | 
| 52 | 51 | rabex 5338 | . . . . . . . . . . . . . . 15
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} ∈ V | 
| 53 | 52, 10 | dmmpti 6711 | . . . . . . . . . . . . . 14
⊢ dom 𝑉 = (LIdeal‘𝑅) | 
| 54 | 45, 53 | sseqtrdi 4023 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ (LIdeal‘𝑅)) | 
| 55 |  | simp-7r 789 | . . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (♯‘(Base‘𝑅)) ≠ 1) | 
| 56 |  | simpllr 775 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(1r‘𝑅) =
(𝑅
Σg 𝑎)) | 
| 57 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 58 |  | ringcmn 20280 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) | 
| 59 | 1, 58 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd) | 
| 60 | 59 | ad8antr 740 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → 𝑅 ∈ CMnd) | 
| 61 | 24 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (◡𝑉 “ 𝑥) ∈ V) | 
| 62 | 27 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅)) | 
| 63 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑎 supp (0g‘𝑅)) = ∅) | 
| 64 |  | ssidd 4006 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → ∅ ⊆
∅) | 
| 65 | 63, 64 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑎 supp (0g‘𝑅)) ⊆ ∅) | 
| 66 | 35 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → 𝑎 finSupp (0g‘𝑅)) | 
| 67 | 4, 57, 60, 61, 62, 65, 66 | gsumres 19932 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑅 Σg (𝑎 ↾ ∅)) = (𝑅 Σg
𝑎)) | 
| 68 |  | res0 6000 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ↾ ∅) =
∅ | 
| 69 | 68 | oveq2i 7443 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 Σg
(𝑎 ↾ ∅)) =
(𝑅
Σg ∅) | 
| 70 | 57 | gsum0 18698 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 Σg
∅) = (0g‘𝑅) | 
| 71 | 69, 70 | eqtri 2764 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Σg
(𝑎 ↾ ∅)) =
(0g‘𝑅) | 
| 72 | 67, 71 | eqtr3di 2791 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) → (𝑅 Σg 𝑎) = (0g‘𝑅)) | 
| 73 | 56, 72 | eqtr2d 2777 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(0g‘𝑅) =
(1r‘𝑅)) | 
| 74 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 75 | 4, 57, 74 | 01eq0ring 20531 | . . . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . . . 15
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(♯‘(Base‘𝑅)) =
(♯‘{(0g‘𝑅)})) | 
| 78 |  | fvex 6918 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) ∈ V | 
| 79 |  | hashsng 14409 | . . . . . . . . . . . . . . . 16
⊢
((0g‘𝑅) ∈ V →
(♯‘{(0g‘𝑅)}) = 1) | 
| 80 | 78, 79 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢
(♯‘{(0g‘𝑅)}) = 1 | 
| 81 | 77, 80 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g‘𝑅)) = ∅) →
(♯‘(Base‘𝑅)) = 1) | 
| 82 | 55, 81 | mteqand 3032 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ≠ ∅) | 
| 83 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(RSpan‘𝑅) =
(RSpan‘𝑅) | 
| 84 | 10, 83 | zarclsiin 33871 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝑎 supp (0g‘𝑅)) ⊆ (LIdeal‘𝑅) ∧ (𝑎 supp (0g‘𝑅)) ≠ ∅) → ∩ 𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))))) | 
| 85 | 50, 54, 82, 84 | syl3anc 1372 | . . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∩
𝑙 ∈ (𝑎 supp (0g‘𝑅))(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))))) | 
| 86 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑙((((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) | 
| 87 |  | nfra1 3283 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑙∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 | 
| 88 | 86, 87 | nfan 1898 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑙(((((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) | 
| 89 | 54 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0g‘𝑅))) → 𝑙 ∈ (LIdeal‘𝑅)) | 
| 90 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 91 | 4, 90 | lidlss 21223 | . . . . . . . . . . . . . . . . . . . . 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 412 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑙 ∈ (𝑎 supp (0g‘𝑅)) → 𝑙 ⊆ (Base‘𝑅))) | 
| 94 | 88, 93 | ralrimi 3256 | . . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∀𝑙 ∈ (𝑎 supp (0g‘𝑅))𝑙 ⊆ (Base‘𝑅)) | 
| 95 |  | unissb 4938 | . . . . . . . . . . . . . . . . . 18
⊢ (∪ (𝑎
supp (0g‘𝑅)) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (𝑎 supp (0g‘𝑅))𝑙 ⊆ (Base‘𝑅)) | 
| 96 | 94, 95 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∪ (𝑎 supp (0g‘𝑅)) ⊆ (Base‘𝑅)) | 
| 97 | 83, 4, 90 | rspcl 21246 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ ∪ (𝑎
supp (0g‘𝑅)) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅)) | 
| 98 | 50, 96, 97 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅)) | 
| 99 | 4, 90 | lidlss 21223 | . . . . . . . . . . . . . . . 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 21248 | . . . . . . . . . . . . . . . . 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 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑎:(◡𝑉 “ 𝑥)⟶(Base‘𝑅)) | 
| 104 | 103, 43 | fssresd 6774 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g‘𝑅))):(𝑎 supp (0g‘𝑅))⟶(Base‘𝑅)) | 
| 105 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑅)
∈ V | 
| 106 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 supp (0g‘𝑅)) ∈ V | 
| 107 | 105, 106 | elmap 8912 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ↾ (𝑎 supp (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅))) ↔ (𝑎 ↾ (𝑎 supp (0g‘𝑅))):(𝑎 supp (0g‘𝑅))⟶(Base‘𝑅)) | 
| 108 | 104, 107 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅)))) | 
| 109 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (𝑏 finSupp (0g‘𝑅) ↔ (𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅))) | 
| 110 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (𝑅 Σg 𝑏) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅))))) | 
| 111 | 110 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → ((1r‘𝑅) = (𝑅 Σg 𝑏) ↔
(1r‘𝑅) =
(𝑅
Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))))) | 
| 112 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (𝑏‘𝑘) = ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘)) | 
| 113 | 112 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → ((𝑏‘𝑘) ∈ 𝑘 ↔ ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘)) | 
| 114 | 113 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → (∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘 ↔ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘)) | 
| 115 | 109, 111,
114 | 3anbi123d 1437 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0g‘𝑅))) → ((𝑏 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘) ↔ ((𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘))) | 
| 116 | 115 | adantl 481 | . . . . . . . . . . . . . . . . . . . 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 6920 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (0g‘𝑅) ∈ V) | 
| 118 | 35, 117 | fsuppres 9434 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g‘𝑅))) finSupp (0g‘𝑅)) | 
| 119 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1r‘𝑅) = (𝑅 Σg 𝑎)) | 
| 120 | 50, 58 | 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 4006 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0g‘𝑅)) ⊆ (𝑎 supp (0g‘𝑅))) | 
| 123 | 4, 57, 120, 121, 103, 122, 35 | gsumres 19932 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅)))) = (𝑅 Σg 𝑎)) | 
| 124 | 119, 123 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1r‘𝑅) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g‘𝑅))))) | 
| 125 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → 𝑘 ∈ (𝑎 supp (0g‘𝑅))) | 
| 126 | 125 | fvresd 6925 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) = (𝑎‘𝑘)) | 
| 127 | 16, 28 | sseqtrid 4025 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) → (𝑎 supp (0g‘𝑅)) ⊆ (◡𝑉 “ 𝑥)) | 
| 128 | 127 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → 𝑘 ∈ (◡𝑉 “ 𝑥)) | 
| 129 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 = 𝑘 → (𝑎‘𝑙) = (𝑎‘𝑘)) | 
| 130 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘) | 
| 131 | 129, 130 | eleq12d 2834 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙 = 𝑘 → ((𝑎‘𝑙) ∈ 𝑙 ↔ (𝑎‘𝑘) ∈ 𝑘)) | 
| 132 | 131 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) ∧ 𝑙 = 𝑘) → ((𝑎‘𝑙) ∈ 𝑙 ↔ (𝑎‘𝑘) ∈ 𝑘)) | 
| 133 | 128, 132 | rspcdv 3613 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → (∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 → (𝑎‘𝑘) ∈ 𝑘)) | 
| 134 | 133 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . 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 2840 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g‘𝑅))) → ((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘) | 
| 137 | 136 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))((𝑎 ↾ (𝑎 supp (0g‘𝑅)))‘𝑘) ∈ 𝑘) | 
| 138 | 118, 124,
137 | 3jca 1128 | . . . . . . . . . . . . . . . . . . . 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 3623 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∃𝑏 ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g‘𝑅)))(𝑏 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g‘𝑅))(𝑏‘𝑘) ∈ 𝑘)) | 
| 140 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 141 | 83, 4, 57, 140, 50, 54 | elrspunidl 33457 | . . . . . . . . . . . . . . . . . . 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 257 | . . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) | 
| 143 | 142 | snssd 4808 | . . . . . . . . . . . . . . . . 17
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → {(1r‘𝑅)} ⊆ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) | 
| 144 | 83, 90 | rspssp 21250 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧
((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) ∈ (LIdeal‘𝑅) ∧
{(1r‘𝑅)}
⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) → ((RSpan‘𝑅)‘{(1r‘𝑅)}) ⊆ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) | 
| 145 | 50, 98, 143, 144 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1r‘𝑅)}) ⊆ ((RSpan‘𝑅)‘∪ (𝑎
supp (0g‘𝑅)))) | 
| 146 | 102, 145 | eqsstrrd 4018 | . . . . . . . . . . . . . . 15
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (Base‘𝑅) ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) | 
| 147 | 100, 146 | eqssd 4000 | . . . . . . . . . . . . . 14
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅))) = (Base‘𝑅)) | 
| 148 | 147 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) = (𝑉‘(Base‘𝑅))) | 
| 149 | 90, 4 | lidl1 21244 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ∈
(LIdeal‘𝑅)) | 
| 150 | 1, 149 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) ∈
(LIdeal‘𝑅)) | 
| 151 | 10, 4 | zarcls1 33869 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ CRing ∧
(Base‘𝑅) ∈
(LIdeal‘𝑅)) →
((𝑉‘(Base‘𝑅)) = ∅ ↔
(Base‘𝑅) =
(Base‘𝑅))) | 
| 152 | 150, 151 | mpdan 687 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → ((𝑉‘(Base‘𝑅)) = ∅ ↔
(Base‘𝑅) =
(Base‘𝑅))) | 
| 153 | 4, 152 | mpbiri 258 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ CRing → (𝑉‘(Base‘𝑅)) = ∅) | 
| 154 | 153 | ad7antr 738 | . . . . . . . . . . . . 13
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘(Base‘𝑅)) = ∅) | 
| 155 | 148, 154 | eqtrd 2776 | . . . . . . . . . . . 12
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0g‘𝑅)))) = ∅) | 
| 156 | 47, 85, 155 | 3eqtrrd 2781 | . . . . . . . . . . 11
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∅ = ∩ (𝑉
“ (𝑎 supp
(0g‘𝑅)))) | 
| 157 | 39, 42, 156 | rspcedvd 3623 | . . . . . . . . . 10
⊢
((((((((𝑅 ∈
CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0g‘𝑅)) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎)) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦) | 
| 158 | 157 | exp41 434 | . . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) → (𝑎 finSupp (0g‘𝑅) →
((1r‘𝑅) =
(𝑅
Σg 𝑎) → (∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)))) | 
| 159 | 158 | 3imp2 1349 | . . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑎 ∈
((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))) ∧ (𝑎 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦) | 
| 160 | 4, 74 | ringidcl 20263 | . . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 161 | 49, 160 | syl 17 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 162 |  | simplr 768 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ∈
𝒫 (Clsd‘𝐽)) | 
| 163 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) | 
| 164 | 2, 3, 163, 10 | zartopn 33875 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ CRing → (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) ∧ ran 𝑉 = (Clsd‘𝐽))) | 
| 165 | 164 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ CRing → ran 𝑉 = (Clsd‘𝐽)) | 
| 166 | 48, 165 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ran 𝑉 =
(Clsd‘𝐽)) | 
| 167 | 166 | pweqd 4616 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝒫 ran 𝑉 = 𝒫 (Clsd‘𝐽)) | 
| 168 | 162, 167 | eleqtrrd 2843 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ∈
𝒫 ran 𝑉) | 
| 169 | 168 | elpwid 4608 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ⊆
ran 𝑉) | 
| 170 |  | intimafv 32721 | . . . . . . . . . . . . . . 15
⊢ ((Fun
𝑉 ∧ (◡𝑉 “ 𝑥) ⊆ dom 𝑉) → ∩ (𝑉 “ (◡𝑉 “ 𝑥)) = ∩
𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙)) | 
| 171 | 19, 44, 170 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ ∩ (𝑉
“ (◡𝑉 “ 𝑥)) = ∩
𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) | 
| 172 |  | funimacnv 6646 | . . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑉 → (𝑉 “ (◡𝑉 “ 𝑥)) = (𝑥 ∩ ran 𝑉)) | 
| 173 | 19, 172 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢ (𝑉 “ (◡𝑉 “ 𝑥)) = (𝑥 ∩ ran 𝑉) | 
| 174 |  | dfss2 3968 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ⊆ ran 𝑉 ↔ (𝑥 ∩ ran 𝑉) = 𝑥) | 
| 175 | 174 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ ran 𝑉 → (𝑥 ∩ ran 𝑉) = 𝑥) | 
| 176 | 173, 175 | eqtrid 2788 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ ran 𝑉 → (𝑉 “ (◡𝑉 “ 𝑥)) = 𝑥) | 
| 177 | 176 | inteqd 4950 | . . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ran 𝑉 → ∩ (𝑉 “ (◡𝑉 “ 𝑥)) = ∩ 𝑥) | 
| 178 | 171, 177 | eqtr3id 2790 | . . . . . . . . . . . . 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 4023 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (◡𝑉 “ 𝑥) ⊆ (LIdeal‘𝑅)) | 
| 182 | 19 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → Fun 𝑉) | 
| 183 |  | inteq 4948 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ∅ → ∩ 𝑥 =
∩ ∅) | 
| 184 |  | int0 4961 | . . . . . . . . . . . . . . . . . 18
⊢ ∩ ∅ = V | 
| 185 | 183, 184 | eqtrdi 2792 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∅ → ∩ 𝑥 =
V) | 
| 186 |  | vn0 4344 | . . . . . . . . . . . . . . . . . 18
⊢ V ≠
∅ | 
| 187 |  | neeq1 3002 | . . . . . . . . . . . . . . . . . 18
⊢ (∩ 𝑥 =
V → (∩ 𝑥 ≠ ∅ ↔ V ≠
∅)) | 
| 188 | 186, 187 | mpbiri 258 | . . . . . . . . . . . . . . . . 17
⊢ (∩ 𝑥 =
V → ∩ 𝑥 ≠ ∅) | 
| 189 | 185, 188 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → ∩ 𝑥
≠ ∅) | 
| 190 | 189 | necon2i 2974 | . . . . . . . . . . . . . . 15
⊢ (∩ 𝑥 =
∅ → 𝑥 ≠
∅) | 
| 191 | 190 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → 𝑥 ≠
∅) | 
| 192 |  | preiman0 32720 | . . . . . . . . . . . . . 14
⊢ ((Fun
𝑉 ∧ 𝑥 ⊆ ran 𝑉 ∧ 𝑥 ≠ ∅) → (◡𝑉 “ 𝑥) ≠ ∅) | 
| 193 | 182, 169,
191, 192 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (◡𝑉 “ 𝑥) ≠ ∅) | 
| 194 | 10, 83 | zarclsiin 33871 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (◡𝑉 “ 𝑥) ⊆ (LIdeal‘𝑅) ∧ (◡𝑉 “ 𝑥) ≠ ∅) → ∩ 𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)))) | 
| 195 | 49, 181, 193, 194 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∩ 𝑙 ∈ (◡𝑉 “ 𝑥)(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)))) | 
| 196 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∩ 𝑥 = ∅) | 
| 197 | 179, 195,
196 | 3eqtr3d 2784 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) = ∅) | 
| 198 | 181 | sselda 3982 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑙 ∈
(◡𝑉 “ 𝑥)) → 𝑙 ∈ (LIdeal‘𝑅)) | 
| 199 | 198, 91 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ CRing
∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) ∧ 𝑙 ∈
(◡𝑉 “ 𝑥)) → 𝑙 ⊆ (Base‘𝑅)) | 
| 200 | 199 | ralrimiva 3145 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∀𝑙
∈ (◡𝑉 “ 𝑥)𝑙 ⊆ (Base‘𝑅)) | 
| 201 |  | unissb 4938 | . . . . . . . . . . . . . 14
⊢ (∪ (◡𝑉 “ 𝑥) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (◡𝑉 “ 𝑥)𝑙 ⊆ (Base‘𝑅)) | 
| 202 | 200, 201 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∪ (◡𝑉 “ 𝑥) ⊆ (Base‘𝑅)) | 
| 203 | 83, 4, 90 | rspcl 21246 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ ∪ (◡𝑉 “ 𝑥) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) | 
| 204 | 49, 202, 203 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) | 
| 205 | 10, 4 | zarcls1 33869 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧
((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) → ((𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) = (Base‘𝑅))) | 
| 206 | 48, 204, 205 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((𝑉‘((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) = (Base‘𝑅))) | 
| 207 | 197, 206 | mpbid 232 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) = (Base‘𝑅)) | 
| 208 | 161, 207 | eleqtrrd 2843 | . . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → (1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥))) | 
| 209 | 83, 4, 57, 140, 49, 181 | elrspunidl 33457 | . . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ((1r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (◡𝑉 “ 𝑥)) ↔ ∃𝑎 ∈ ((Base‘𝑅) ↑m (◡𝑉 “ 𝑥))(𝑎 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙))) | 
| 210 | 208, 209 | mpbid 232 | . . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∃𝑎
∈ ((Base‘𝑅)
↑m (◡𝑉 “ 𝑥))(𝑎 finSupp (0g‘𝑅) ∧
(1r‘𝑅) =
(𝑅
Σg 𝑎) ∧ ∀𝑙 ∈ (◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)) | 
| 211 | 159, 210 | r19.29a 3161 | . . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∃𝑦
∈ (𝒫 𝑥 ∩
Fin)∅ = ∩ 𝑦) | 
| 212 |  | 0ex 5306 | . . . . . . . 8
⊢ ∅
∈ V | 
| 213 |  | vex 3483 | . . . . . . . 8
⊢ 𝑥 ∈ V | 
| 214 |  | elfi 9454 | . . . . . . . 8
⊢ ((∅
∈ V ∧ 𝑥 ∈ V)
→ (∅ ∈ (fi‘𝑥) ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)) | 
| 215 | 212, 213,
214 | mp2an 692 | . . . . . . 7
⊢ (∅
∈ (fi‘𝑥) ↔
∃𝑦 ∈ (𝒫
𝑥 ∩ Fin)∅ = ∩ 𝑦) | 
| 216 | 211, 215 | sylibr 234 | . . . . . 6
⊢ ((((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 =
∅) → ∅ ∈ (fi‘𝑥)) | 
| 217 | 216 | ex 412 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (∩ 𝑥 =
∅ → ∅ ∈ (fi‘𝑥))) | 
| 218 | 217 | necon3bd 2953 | . . . 4
⊢ (((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (¬ ∅ ∈
(fi‘𝑥) → ∩ 𝑥
≠ ∅)) | 
| 219 | 218 | ralrimiva 3145 | . . 3
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) → ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈
(fi‘𝑥) → ∩ 𝑥
≠ ∅)) | 
| 220 |  | cmpfi 23417 | . . . 4
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔
∀𝑥 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑥)
→ ∩ 𝑥 ≠ ∅))) | 
| 221 | 220 | biimpar 477 | . . 3
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑥)
→ ∩ 𝑥 ≠ ∅)) → 𝐽 ∈ Comp) | 
| 222 | 9, 219, 221 | syl2an2r 685 | . 2
⊢ ((𝑅 ∈ CRing ∧
(♯‘(Base‘𝑅)) ≠ 1) → 𝐽 ∈ Comp) | 
| 223 | 8, 222 | pm2.61dane 3028 | 1
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp) |