Theorem zarcmplem 31337

Description: Lemma for zarcmp 31338. (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.

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)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  ∀wral 3068  ∃wrex 3069  {crab 3072  Vcvv 3407   ∩ cin 3853   ⊆ wss 3854  ∅c0 4221  𝒫 cpw 4487  {csn 4515  ∪ cuni 4791  ∩ cint 4831  ∩ ciin 4877   class class class wbr 5025   ↦ cmpt 5105  ^◡ccnv 5516  dom cdm 5517  ran crn 5518   ↾ cres 5519   “ cima 5520  Fun wfun 6322  ⟶wf 6324  ‘cfv 6328  (class class class)co 7143   supp csupp 7828   ↑_m cmap 8409  Fincfn 8520   finSupp cfsupp 8851  ficfi 8892  1c1 10561  ♯chash 13725  Basecbs 16526  ._rcmulr 16609  TopOpenctopn 16738  0_gc0g 16756   Σ_g cgsu 16757  CMndccmn 18958  1_rcur 19304  Ringcrg 19350  CRingccrg 19351  LIdealclidl 19995  RSpancrsp 19996  Topctop 21578  TopOnctopon 21595  Clsdccld 21701  Compccmp 22071  PrmIdealcprmidl 31116  Speccrspec 31318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-reg 9074  ax-inf2 9122  ax-ac2 9908  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-addf 10639  ax-mulf 10640

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-iin 4879  df-disj 4991  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  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 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-of 7398  df-rpss 7440  df-om 7573  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-ixp 8473  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-fsupp 8852  df-fi 8893  df-sup 8924  df-oi 8992  df-r1 9211  df-rank 9212  df-dju 9348  df-card 9386  df-ac 9561  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-7 11727  df-8 11728  df-9 11729  df-n0 11920  df-xnn0 11992  df-z 12006  df-dec 12123  df-uz 12268  df-fz 12925  df-fzo 13068  df-seq 13404  df-hash 13726  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-starv 16623  df-sca 16624  df-vsca 16625  df-ip 16626  df-tset 16627  df-ple 16628  df-ds 16630  df-unif 16631  df-hom 16632  df-cco 16633  df-rest 16739  df-topn 16740  df-0g 16758  df-gsum 16759  df-prds 16764  df-pws 16766  df-mre 16900  df-mrc 16901  df-acs 16903  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-mhm 18007  df-submnd 18008  df-grp 18157  df-minusg 18158  df-sbg 18159  df-mulg 18277  df-subg 18328  df-ghm 18408  df-cntz 18499  df-lsm 18813  df-cmn 18960  df-abl 18961  df-mgp 19293  df-ur 19305  df-ring 19352  df-cring 19353  df-rnghom 19523  df-subrg 19586  df-lmod 19689  df-lss 19757  df-lsp 19797  df-lmhm 19847  df-lbs 19900  df-sra 19997  df-rgmod 19998  df-lidl 19999  df-rsp 20000  df-lpidl 20069  df-nzr 20084  df-cnfld 20152  df-zring 20224  df-zrh 20258  df-dsmm 20482  df-frlm 20497  df-uvc 20533  df-top 21579  df-topon 21596  df-cld 21704  df-cmp 22072  df-prmidl 31117  df-mxidl 31138  df-idlsrg 31152  df-rspec 31319

This theorem is referenced by:  zarcmp  31338