Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  zarcmplem Structured version   Visualization version   GIF version

Theorem zarcmplem 31234
 Description: Lemma for zarcmp 31235. (Contributed by Thierry Arnoux, 2-Jul-2024.)
Hypotheses
Ref Expression
zartop.1 𝑆 = (Spec‘𝑅)
zartop.2 𝐽 = (TopOpen‘𝑆)
zarcmplem.1 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})
Assertion
Ref Expression
zarcmplem (𝑅 ∈ CRing → 𝐽 ∈ Comp)
Distinct variable groups:   𝑅,𝑖,𝑗   𝑖,𝐽,𝑗   𝑗,𝑉,𝑖
Allowed substitution hints:   𝑆(𝑖,𝑗)

Proof of Theorem zarcmplem
Dummy variables 𝑘 𝑥 𝑦 𝑎 𝑙 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 crngring 19305 . . . 4 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2 zartop.1 . . . . 5 𝑆 = (Spec‘𝑅)
3 zartop.2 . . . . 5 𝐽 = (TopOpen‘𝑆)
4 eqid 2801 . . . . 5 (Base‘𝑅) = (Base‘𝑅)
52, 3, 4zar0ring 31231 . . . 4 ((𝑅 ∈ Ring ∧ (♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅})
61, 5sylan 583 . . 3 ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅})
7 0cmp 22002 . . 3 {∅} ∈ Comp
86, 7eqeltrdi 2901 . 2 ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) = 1) → 𝐽 ∈ Comp)
92, 3zartop 31229 . . 3 (𝑅 ∈ CRing → 𝐽 ∈ Top)
10 zarcmplem.1 . . . . . . . . . . . . . . 15 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})
11 fvex 6662 . . . . . . . . . . . . . . . 16 (LIdeal‘𝑅) ∈ V
1211mptex 6967 . . . . . . . . . . . . . . 15 (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗}) ∈ V
1310, 12eqeltri 2889 . . . . . . . . . . . . . 14 𝑉 ∈ V
14 imaexg 7606 . . . . . . . . . . . . . 14 (𝑉 ∈ V → (𝑉 “ (𝑎 supp (0g𝑅))) ∈ V)
1513, 14mp1i 13 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g𝑅))) ∈ V)
16 suppssdm 7830 . . . . . . . . . . . . . . 15 (𝑎 supp (0g𝑅)) ⊆ dom 𝑎
17 imass2 5936 . . . . . . . . . . . . . . 15 ((𝑎 supp (0g𝑅)) ⊆ dom 𝑎 → (𝑉 “ (𝑎 supp (0g𝑅))) ⊆ (𝑉 “ dom 𝑎))
1816, 17mp1i 13 . . . . . . . . . . . . . 14 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g𝑅))) ⊆ (𝑉 “ dom 𝑎))
1910funmpt2 6367 . . . . . . . . . . . . . . 15 Fun 𝑉
20 ssidd 3941 . . . . . . . . . . . . . . . 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 6664 . . . . . . . . . . . . . . . . . . . 20 (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) → (Base‘𝑅) ∈ V)
2313cnvex 7616 . . . . . . . . . . . . . . . . . . . . . 22 𝑉 ∈ V
2423imaex 7607 . . . . . . . . . . . . . . . . . . . . 21 (𝑉𝑥) ∈ V
2524a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) → (𝑉𝑥) ∈ V)
2622, 25elmapd 8407 . . . . . . . . . . . . . . . . . . 19 (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) → (𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥)) ↔ 𝑎:(𝑉𝑥)⟶(Base‘𝑅)))
2721, 26mpbid 235 . . . . . . . . . . . . . . . . . 18 (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) → 𝑎:(𝑉𝑥)⟶(Base‘𝑅))
2827fdmd 6501 . . . . . . . . . . . . . . . . 17 (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) → dom 𝑎 = (𝑉𝑥))
2928adantr 484 . . . . . . . . . . . . . . . 16 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → dom 𝑎 = (𝑉𝑥))
3020, 29sseqtrd 3958 . . . . . . . . . . . . . . 15 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → dom 𝑎 ⊆ (𝑉𝑥))
31 funimass2 6411 . . . . . . . . . . . . . . 15 ((Fun 𝑉 ∧ dom 𝑎 ⊆ (𝑉𝑥)) → (𝑉 “ dom 𝑎) ⊆ 𝑥)
3219, 30, 31sylancr 590 . . . . . . . . . . . . . 14 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ dom 𝑎) ⊆ 𝑥)
3318, 32sstrd 3928 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g𝑅))) ⊆ 𝑥)
3415, 33elpwd 4508 . . . . . . . . . . . 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𝑅))
3635fsuppimpd 8828 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 supp (0g𝑅)) ∈ Fin)
37 imafi 8805 . . . . . . . . . . . . 13 ((Fun 𝑉 ∧ (𝑎 supp (0g𝑅)) ∈ Fin) → (𝑉 “ (𝑎 supp (0g𝑅))) ∈ Fin)
3819, 36, 37sylancr 590 . . . . . . . . . . . 12 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g𝑅))) ∈ Fin)
3934, 38elind 4124 . . . . . . . . . . 11 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g𝑅))) ∈ (𝒫 𝑥 ∩ Fin))
40 inteq 4844 . . . . . . . . . . . . 13 (𝑦 = (𝑉 “ (𝑎 supp (0g𝑅))) → 𝑦 = (𝑉 “ (𝑎 supp (0g𝑅))))
4140eqeq2d 2812 . . . . . . . . . . . 12 (𝑦 = (𝑉 “ (𝑎 supp (0g𝑅))) → (∅ = 𝑦 ↔ ∅ = (𝑉 “ (𝑎 supp (0g𝑅)))))
4241adantl 485 . . . . . . . . . . 11 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑦 = (𝑉 “ (𝑎 supp (0g𝑅)))) → (∅ = 𝑦 ↔ ∅ = (𝑉 “ (𝑎 supp (0g𝑅)))))
4316, 29sseqtrid 3970 . . . . . . . . . . . . . 14 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 supp (0g𝑅)) ⊆ (𝑉𝑥))
44 cnvimass 5920 . . . . . . . . . . . . . 14 (𝑉𝑥) ⊆ dom 𝑉
4543, 44sstrdi 3930 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 supp (0g𝑅)) ⊆ dom 𝑉)
46 intimafv 30473 . . . . . . . . . . . . 13 ((Fun 𝑉 ∧ (𝑎 supp (0g𝑅)) ⊆ dom 𝑉) → (𝑉 “ (𝑎 supp (0g𝑅))) = 𝑙 ∈ (𝑎 supp (0g𝑅))(𝑉𝑙))
4719, 45, 46sylancr 590 . . . . . . . . . . . 12 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0g𝑅))) = 𝑙 ∈ (𝑎 supp (0g𝑅))(𝑉𝑙))
48 simplll 774 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑅 ∈ CRing)
4948crngringd 19306 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑅 ∈ Ring)
5049ad4antr 731 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → 𝑅 ∈ Ring)
51 fvex 6662 . . . . . . . . . . . . . . . 16 (PrmIdeal‘𝑅) ∈ V
5251rabex 5202 . . . . . . . . . . . . . . 15 {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗} ∈ V
5352, 10dmmpti 6468 . . . . . . . . . . . . . 14 dom 𝑉 = (LIdeal‘𝑅)
5445, 53sseqtrdi 3968 . . . . . . . . . . . . 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 res0 5826 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ↾ ∅) = ∅
5857oveq2i 7150 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Σg (𝑎 ↾ ∅)) = (𝑅 Σg ∅)
59 eqid 2801 . . . . . . . . . . . . . . . . . . . . 21 (0g𝑅) = (0g𝑅)
6059gsum0 17889 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Σg ∅) = (0g𝑅)
6158, 60eqtri 2824 . . . . . . . . . . . . . . . . . . 19 (𝑅 Σg (𝑎 ↾ ∅)) = (0g𝑅)
62 ringcmn 19330 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
631, 62syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ CRing → 𝑅 ∈ CMnd)
6463ad8antr 739 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → 𝑅 ∈ CMnd)
6524a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (𝑉𝑥) ∈ V)
6627ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → 𝑎:(𝑉𝑥)⟶(Base‘𝑅))
67 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (𝑎 supp (0g𝑅)) = ∅)
68 ssidd 3941 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → ∅ ⊆ ∅)
6967, 68eqsstrd 3956 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (𝑎 supp (0g𝑅)) ⊆ ∅)
7035adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → 𝑎 finSupp (0g𝑅))
714, 59, 64, 65, 66, 69, 70gsumres 19029 . . . . . . . . . . . . . . . . . . 19 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (𝑅 Σg (𝑎 ↾ ∅)) = (𝑅 Σg 𝑎))
7261, 71syl5reqr 2851 . . . . . . . . . . . . . . . . . 18 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (𝑅 Σg 𝑎) = (0g𝑅))
7356, 72eqtr2d 2837 . . . . . . . . . . . . . . . . 17 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (0g𝑅) = (1r𝑅))
74 eqid 2801 . . . . . . . . . . . . . . . . . 18 (1r𝑅) = (1r𝑅)
754, 59, 7401eq0ring 20041 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ (0g𝑅) = (1r𝑅)) → (Base‘𝑅) = {(0g𝑅)})
7650, 73, 75syl2an2r 684 . . . . . . . . . . . . . . . 16 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (Base‘𝑅) = {(0g𝑅)})
7776fveq2d 6653 . . . . . . . . . . . . . . 15 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (♯‘(Base‘𝑅)) = (♯‘{(0g𝑅)}))
78 fvex 6662 . . . . . . . . . . . . . . . 16 (0g𝑅) ∈ V
79 hashsng 13730 . . . . . . . . . . . . . . . 16 ((0g𝑅) ∈ V → (♯‘{(0g𝑅)}) = 1)
8078, 79ax-mp 5 . . . . . . . . . . . . . . 15 (♯‘{(0g𝑅)}) = 1
8177, 80eqtrdi 2852 . . . . . . . . . . . . . 14 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ (𝑎 supp (0g𝑅)) = ∅) → (♯‘(Base‘𝑅)) = 1)
8255, 81mteqand 3093 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 supp (0g𝑅)) ≠ ∅)
83 eqid 2801 . . . . . . . . . . . . . 14 (RSpan‘𝑅) = (RSpan‘𝑅)
8410, 83zarclsiin 31224 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑎 supp (0g𝑅)) ⊆ (LIdeal‘𝑅) ∧ (𝑎 supp (0g𝑅)) ≠ ∅) → 𝑙 ∈ (𝑎 supp (0g𝑅))(𝑉𝑙) = (𝑉‘((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅)))))
8550, 54, 82, 84syl3anc 1368 . . . . . . . . . . . 12 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → 𝑙 ∈ (𝑎 supp (0g𝑅))(𝑉𝑙) = (𝑉‘((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅)))))
86 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 𝑙((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎))
87 nfra1 3186 . . . . . . . . . . . . . . . . . . . 20 𝑙𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙
8886, 87nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑙(((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙)
8954sselda 3918 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0g𝑅))) → 𝑙 ∈ (LIdeal‘𝑅))
90 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (LIdeal‘𝑅) = (LIdeal‘𝑅)
914, 90lidlss 19979 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (LIdeal‘𝑅) → 𝑙 ⊆ (Base‘𝑅))
9289, 91syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0g𝑅))) → 𝑙 ⊆ (Base‘𝑅))
9392ex 416 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑙 ∈ (𝑎 supp (0g𝑅)) → 𝑙 ⊆ (Base‘𝑅)))
9488, 93ralrimi 3183 . . . . . . . . . . . . . . . . . 18 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ∀𝑙 ∈ (𝑎 supp (0g𝑅))𝑙 ⊆ (Base‘𝑅))
95 unissb 4835 . . . . . . . . . . . . . . . . . 18 ( (𝑎 supp (0g𝑅)) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (𝑎 supp (0g𝑅))𝑙 ⊆ (Base‘𝑅))
9694, 95sylibr 237 . . . . . . . . . . . . . . . . 17 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 supp (0g𝑅)) ⊆ (Base‘𝑅))
9783, 4, 90rspcl 19991 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ (𝑎 supp (0g𝑅)) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) ∈ (LIdeal‘𝑅))
9850, 96, 97syl2anc 587 . . . . . . . . . . . . . . . 16 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) ∈ (LIdeal‘𝑅))
994, 90lidlss 19979 . . . . . . . . . . . . . . . 16 (((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) ⊆ (Base‘𝑅))
10098, 99syl 17 . . . . . . . . . . . . . . 15 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) ⊆ (Base‘𝑅))
10183, 4, 74rsp1 19993 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Ring → ((RSpan‘𝑅)‘{(1r𝑅)}) = (Base‘𝑅))
10250, 101syl 17 . . . . . . . . . . . . . . . 16 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1r𝑅)}) = (Base‘𝑅))
10327adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → 𝑎:(𝑉𝑥)⟶(Base‘𝑅))
104103, 43fssresd 6523 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g𝑅))):(𝑎 supp (0g𝑅))⟶(Base‘𝑅))
105 fvex 6662 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝑅) ∈ V
106 ovex 7172 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 supp (0g𝑅)) ∈ V
107105, 106elmap 8422 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ↾ (𝑎 supp (0g𝑅))) ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g𝑅))) ↔ (𝑎 ↾ (𝑎 supp (0g𝑅))):(𝑎 supp (0g𝑅))⟶(Base‘𝑅))
108104, 107sylibr 237 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0g𝑅))) ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g𝑅))))
109 breq1 5036 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → (𝑏 finSupp (0g𝑅) ↔ (𝑎 ↾ (𝑎 supp (0g𝑅))) finSupp (0g𝑅)))
110 oveq2 7147 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → (𝑅 Σg 𝑏) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g𝑅)))))
111110eqeq2d 2812 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → ((1r𝑅) = (𝑅 Σg 𝑏) ↔ (1r𝑅) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g𝑅))))))
112 fveq1 6648 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → (𝑏𝑘) = ((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘))
113112eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → ((𝑏𝑘) ∈ 𝑘 ↔ ((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) ∈ 𝑘))
114113ralbidv 3165 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → (∀𝑘 ∈ (𝑎 supp (0g𝑅))(𝑏𝑘) ∈ 𝑘 ↔ ∀𝑘 ∈ (𝑎 supp (0g𝑅))((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) ∈ 𝑘))
115109, 111, 1143anbi123d 1433 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑎 ↾ (𝑎 supp (0g𝑅))) → ((𝑏 finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g𝑅))(𝑏𝑘) ∈ 𝑘) ↔ ((𝑎 ↾ (𝑎 supp (0g𝑅))) finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0g𝑅))((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) ∈ 𝑘)))
116115adantl 485 . . . . . . . . . . . . . . . . . . . 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 6664 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (0g𝑅) ∈ V)
11835, 117fsuppres 8846 . . . . . . . . . . . . . . . . . . . . 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 𝑎))
12050, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → 𝑅 ∈ CMnd)
12124a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉𝑥) ∈ V)
122 ssidd 3941 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎 supp (0g𝑅)) ⊆ (𝑎 supp (0g𝑅)))
1234, 59, 120, 121, 103, 122, 35gsumres 19029 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g𝑅)))) = (𝑅 Σg 𝑎))
124119, 123eqtr4d 2839 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (1r𝑅) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g𝑅)))))
125 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) → 𝑘 ∈ (𝑎 supp (0g𝑅)))
126125fvresd 6669 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) → ((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) = (𝑎𝑘))
12716, 28sseqtrid 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) → (𝑎 supp (0g𝑅)) ⊆ (𝑉𝑥))
128127sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) → 𝑘 ∈ (𝑉𝑥))
129 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 = 𝑘 → (𝑎𝑙) = (𝑎𝑘))
130 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 = 𝑘𝑙 = 𝑘)
131129, 130eleq12d 2887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 = 𝑘 → ((𝑎𝑙) ∈ 𝑙 ↔ (𝑎𝑘) ∈ 𝑘))
132131adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) ∧ 𝑙 = 𝑘) → ((𝑎𝑙) ∈ 𝑙 ↔ (𝑎𝑘) ∈ 𝑘))
133128, 132rspcdv 3566 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) → (∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙 → (𝑎𝑘) ∈ 𝑘))
134133imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑎𝑘) ∈ 𝑘)
135134an32s 651 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) → (𝑎𝑘) ∈ 𝑘)
136126, 135eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0g𝑅))) → ((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) ∈ 𝑘)
137136ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ∀𝑘 ∈ (𝑎 supp (0g𝑅))((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) ∈ 𝑘)
138118, 124, 1373jca 1125 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ((𝑎 ↾ (𝑎 supp (0g𝑅))) finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg (𝑎 ↾ (𝑎 supp (0g𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0g𝑅))((𝑎 ↾ (𝑎 supp (0g𝑅)))‘𝑘) ∈ 𝑘))
139108, 116, 138rspcedvd 3577 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ∃𝑏 ∈ ((Base‘𝑅) ↑m (𝑎 supp (0g𝑅)))(𝑏 finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0g𝑅))(𝑏𝑘) ∈ 𝑘))
140 eqid 2801 . . . . . . . . . . . . . . . . . . . 20 (.r𝑅) = (.r𝑅)
14183, 4, 59, 140, 50, 54elrspunidl 31017 . . . . . . . . . . . . . . . . . . 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𝑅))(𝑏𝑘) ∈ 𝑘)))
142139, 141mpbird 260 . . . . . . . . . . . . . . . . . 18 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (1r𝑅) ∈ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))))
143142snssd 4705 . . . . . . . . . . . . . . . . 17 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → {(1r𝑅)} ⊆ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))))
14483, 90rspssp 19995 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) ∈ (LIdeal‘𝑅) ∧ {(1r𝑅)} ⊆ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅)))) → ((RSpan‘𝑅)‘{(1r𝑅)}) ⊆ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))))
14550, 98, 143, 144syl3anc 1368 . . . . . . . . . . . . . . . 16 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1r𝑅)}) ⊆ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))))
146102, 145eqsstrrd 3957 . . . . . . . . . . . . . . 15 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (Base‘𝑅) ⊆ ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))))
147100, 146eqssd 3935 . . . . . . . . . . . . . 14 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅))) = (Base‘𝑅))
148147fveq2d 6653 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅)))) = (𝑉‘(Base‘𝑅)))
14990, 4lidl1 19989 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Ring → (Base‘𝑅) ∈ (LIdeal‘𝑅))
1501, 149syl 17 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (Base‘𝑅) ∈ (LIdeal‘𝑅))
15110, 4zarcls1 31222 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRing ∧ (Base‘𝑅) ∈ (LIdeal‘𝑅)) → ((𝑉‘(Base‘𝑅)) = ∅ ↔ (Base‘𝑅) = (Base‘𝑅)))
152150, 151mpdan 686 . . . . . . . . . . . . . . 15 (𝑅 ∈ CRing → ((𝑉‘(Base‘𝑅)) = ∅ ↔ (Base‘𝑅) = (Base‘𝑅)))
1534, 152mpbiri 261 . . . . . . . . . . . . . 14 (𝑅 ∈ CRing → (𝑉‘(Base‘𝑅)) = ∅)
154153ad7antr 737 . . . . . . . . . . . . 13 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉‘(Base‘𝑅)) = ∅)
155148, 154eqtrd 2836 . . . . . . . . . . . 12 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘ (𝑎 supp (0g𝑅)))) = ∅)
15647, 85, 1553eqtrrd 2841 . . . . . . . . . . 11 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ∅ = (𝑉 “ (𝑎 supp (0g𝑅))))
15739, 42, 156rspcedvd 3577 . . . . . . . . . 10 ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ 𝑎 finSupp (0g𝑅)) ∧ (1r𝑅) = (𝑅 Σg 𝑎)) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = 𝑦)
158157exp41 438 . . . . . . . . 9 (((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) → (𝑎 finSupp (0g𝑅) → ((1r𝑅) = (𝑅 Σg 𝑎) → (∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = 𝑦))))
1591583imp2 1346 . . . . . . . 8 ((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))) ∧ (𝑎 finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg 𝑎) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = 𝑦)
1604, 74ringidcl 19317 . . . . . . . . . . 11 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
16149, 160syl 17 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (1r𝑅) ∈ (Base‘𝑅))
162 simplr 768 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑥 ∈ 𝒫 (Clsd‘𝐽))
163 eqid 2801 . . . . . . . . . . . . . . . . . . 19 (PrmIdeal‘𝑅) = (PrmIdeal‘𝑅)
1642, 3, 163, 10zartopn 31228 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘(PrmIdeal‘𝑅)) ∧ ran 𝑉 = (Clsd‘𝐽)))
165164simprd 499 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ CRing → ran 𝑉 = (Clsd‘𝐽))
16648, 165syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ran 𝑉 = (Clsd‘𝐽))
167166pweqd 4519 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝒫 ran 𝑉 = 𝒫 (Clsd‘𝐽))
168162, 167eleqtrrd 2896 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑥 ∈ 𝒫 ran 𝑉)
169168elpwid 4511 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑥 ⊆ ran 𝑉)
170 intimafv 30473 . . . . . . . . . . . . . . 15 ((Fun 𝑉 ∧ (𝑉𝑥) ⊆ dom 𝑉) → (𝑉 “ (𝑉𝑥)) = 𝑙 ∈ (𝑉𝑥)(𝑉𝑙))
17119, 44, 170mp2an 691 . . . . . . . . . . . . . 14 (𝑉 “ (𝑉𝑥)) = 𝑙 ∈ (𝑉𝑥)(𝑉𝑙)
172 funimacnv 6409 . . . . . . . . . . . . . . . . 17 (Fun 𝑉 → (𝑉 “ (𝑉𝑥)) = (𝑥 ∩ ran 𝑉))
17319, 172ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑉 “ (𝑉𝑥)) = (𝑥 ∩ ran 𝑉)
174 df-ss 3901 . . . . . . . . . . . . . . . . 17 (𝑥 ⊆ ran 𝑉 ↔ (𝑥 ∩ ran 𝑉) = 𝑥)
175174biimpi 219 . . . . . . . . . . . . . . . 16 (𝑥 ⊆ ran 𝑉 → (𝑥 ∩ ran 𝑉) = 𝑥)
176173, 175syl5eq 2848 . . . . . . . . . . . . . . 15 (𝑥 ⊆ ran 𝑉 → (𝑉 “ (𝑉𝑥)) = 𝑥)
177176inteqd 4846 . . . . . . . . . . . . . 14 (𝑥 ⊆ ran 𝑉 (𝑉 “ (𝑉𝑥)) = 𝑥)
178171, 177syl5eqr 2850 . . . . . . . . . . . . 13 (𝑥 ⊆ ran 𝑉 𝑙 ∈ (𝑉𝑥)(𝑉𝑙) = 𝑥)
179169, 178syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑙 ∈ (𝑉𝑥)(𝑉𝑙) = 𝑥)
18044a1i 11 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (𝑉𝑥) ⊆ dom 𝑉)
181180, 53sseqtrdi 3968 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (𝑉𝑥) ⊆ (LIdeal‘𝑅))
18219a1i 11 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → Fun 𝑉)
183 inteq 4844 . . . . . . . . . . . . . . . . . 18 (𝑥 = ∅ → 𝑥 = ∅)
184 int0 4855 . . . . . . . . . . . . . . . . . 18 ∅ = V
185183, 184eqtrdi 2852 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → 𝑥 = V)
186 vn0 4257 . . . . . . . . . . . . . . . . . 18 V ≠ ∅
187 neeq1 3052 . . . . . . . . . . . . . . . . . 18 ( 𝑥 = V → ( 𝑥 ≠ ∅ ↔ V ≠ ∅))
188186, 187mpbiri 261 . . . . . . . . . . . . . . . . 17 ( 𝑥 = V → 𝑥 ≠ ∅)
189185, 188syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → 𝑥 ≠ ∅)
190189necon2i 3024 . . . . . . . . . . . . . . 15 ( 𝑥 = ∅ → 𝑥 ≠ ∅)
191190adantl 485 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑥 ≠ ∅)
192 preiman0 30472 . . . . . . . . . . . . . 14 ((Fun 𝑉𝑥 ⊆ ran 𝑉𝑥 ≠ ∅) → (𝑉𝑥) ≠ ∅)
193182, 169, 191, 192syl3anc 1368 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (𝑉𝑥) ≠ ∅)
19410, 83zarclsiin 31224 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑉𝑥) ⊆ (LIdeal‘𝑅) ∧ (𝑉𝑥) ≠ ∅) → 𝑙 ∈ (𝑉𝑥)(𝑉𝑙) = (𝑉‘((RSpan‘𝑅)‘ (𝑉𝑥))))
19549, 181, 193, 194syl3anc 1368 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑙 ∈ (𝑉𝑥)(𝑉𝑙) = (𝑉‘((RSpan‘𝑅)‘ (𝑉𝑥))))
196 simpr 488 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → 𝑥 = ∅)
197179, 195, 1963eqtr3d 2844 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (𝑉‘((RSpan‘𝑅)‘ (𝑉𝑥))) = ∅)
198181sselda 3918 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑙 ∈ (𝑉𝑥)) → 𝑙 ∈ (LIdeal‘𝑅))
199198, 91syl 17 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) ∧ 𝑙 ∈ (𝑉𝑥)) → 𝑙 ⊆ (Base‘𝑅))
200199ralrimiva 3152 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ∀𝑙 ∈ (𝑉𝑥)𝑙 ⊆ (Base‘𝑅))
201 unissb 4835 . . . . . . . . . . . . . 14 ( (𝑉𝑥) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (𝑉𝑥)𝑙 ⊆ (Base‘𝑅))
202200, 201sylibr 237 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (𝑉𝑥) ⊆ (Base‘𝑅))
20383, 4, 90rspcl 19991 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑉𝑥) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘ (𝑉𝑥)) ∈ (LIdeal‘𝑅))
20449, 202, 203syl2anc 587 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ((RSpan‘𝑅)‘ (𝑉𝑥)) ∈ (LIdeal‘𝑅))
20510, 4zarcls1 31222 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ ((RSpan‘𝑅)‘ (𝑉𝑥)) ∈ (LIdeal‘𝑅)) → ((𝑉‘((RSpan‘𝑅)‘ (𝑉𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘ (𝑉𝑥)) = (Base‘𝑅)))
20648, 204, 205syl2anc 587 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ((𝑉‘((RSpan‘𝑅)‘ (𝑉𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘ (𝑉𝑥)) = (Base‘𝑅)))
207197, 206mpbid 235 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ((RSpan‘𝑅)‘ (𝑉𝑥)) = (Base‘𝑅))
208161, 207eleqtrrd 2896 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → (1r𝑅) ∈ ((RSpan‘𝑅)‘ (𝑉𝑥)))
20983, 4, 59, 140, 49, 181elrspunidl 31017 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ((1r𝑅) ∈ ((RSpan‘𝑅)‘ (𝑉𝑥)) ↔ ∃𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))(𝑎 finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg 𝑎) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙)))
210208, 209mpbid 235 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ∃𝑎 ∈ ((Base‘𝑅) ↑m (𝑉𝑥))(𝑎 finSupp (0g𝑅) ∧ (1r𝑅) = (𝑅 Σg 𝑎) ∧ ∀𝑙 ∈ (𝑉𝑥)(𝑎𝑙) ∈ 𝑙))
211159, 210r19.29a 3251 . . . . . . 7 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = 𝑦)
212 0ex 5178 . . . . . . . 8 ∅ ∈ V
213 vex 3447 . . . . . . . 8 𝑥 ∈ V
214 elfi 8865 . . . . . . . 8 ((∅ ∈ V ∧ 𝑥 ∈ V) → (∅ ∈ (fi‘𝑥) ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = 𝑦))
215212, 213, 214mp2an 691 . . . . . . 7 (∅ ∈ (fi‘𝑥) ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = 𝑦)
216211, 215sylibr 237 . . . . . 6 ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ 𝑥 = ∅) → ∅ ∈ (fi‘𝑥))
217216ex 416 . . . . 5 (((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ( 𝑥 = ∅ → ∅ ∈ (fi‘𝑥)))
218217necon3bd 3004 . . . 4 (((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (¬ ∅ ∈ (fi‘𝑥) → 𝑥 ≠ ∅))
219218ralrimiva 3152 . . 3 ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) → ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → 𝑥 ≠ ∅))
220 cmpfi 22016 . . . 4 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → 𝑥 ≠ ∅)))
221220biimpar 481 . . 3 ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → 𝑥 ≠ ∅)) → 𝐽 ∈ Comp)
2229, 219, 221syl2an2r 684 . 2 ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) → 𝐽 ∈ Comp)
2238, 222pm2.61dane 3077 1 (𝑅 ∈ CRing → 𝐽 ∈ Comp)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  {crab 3113  Vcvv 3444   ∩ cin 3883   ⊆ wss 3884  ∅c0 4246  𝒫 cpw 4500  {csn 4528  ∪ cuni 4803  ∩ cint 4841  ∩ ciin 4885   class class class wbr 5033   ↦ cmpt 5113  ◡ccnv 5522  dom cdm 5523  ran crn 5524   ↾ cres 5525   “ cima 5526  Fun wfun 6322  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139   supp csupp 7817   ↑m cmap 8393  Fincfn 8496   finSupp cfsupp 8821  ficfi 8862  1c1 10531  ♯chash 13690  Basecbs 16478  .rcmulr 16561  TopOpenctopn 16690  0gc0g 16708   Σg cgsu 16709  CMndccmn 18901  1rcur 19247  Ringcrg 19293  CRingccrg 19294  LIdealclidl 19938  RSpancrsp 19939  Topctop 21501  TopOnctopon 21518  Clsdccld 21624  Compccmp 21994  PrmIdealcprmidl 31018  Speccrspec 31215 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-reg 9044  ax-inf2 9092  ax-ac2 9878  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-addf 10609  ax-mulf 10610 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-disj 4999  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-rpss 7433  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-oi 8962  df-r1 9181  df-rank 9182  df-dju 9318  df-card 9356  df-ac 9531  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12890  df-fzo 13033  df-seq 13369  df-hash 13691  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-prds 16716  df-pws 16718  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18101  df-minusg 18102  df-sbg 18103  df-mulg 18220  df-subg 18271  df-ghm 18351  df-cntz 18442  df-lsm 18756  df-cmn 18903  df-abl 18904  df-mgp 19236  df-ur 19248  df-ring 19295  df-cring 19296  df-rnghom 19466  df-subrg 19529  df-lmod 19632  df-lss 19700  df-lsp 19740  df-lmhm 19790  df-lbs 19843  df-sra 19940  df-rgmod 19941  df-lidl 19942  df-rsp 19943  df-lpidl 20012  df-nzr 20027  df-cnfld 20095  df-zring 20167  df-zrh 20200  df-dsmm 20424  df-frlm 20439  df-uvc 20475  df-top 21502  df-topon 21519  df-cld 21627  df-cmp 21995  df-prmidl 31019  df-mxidl 31040  df-idlsrg 31054  df-rspec 31216 This theorem is referenced by:  zarcmp  31235
 Copyright terms: Public domain W3C validator