zarcmplem - Mathbox for Thierry Arnoux

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

Theorem zarcmplem 33316

Description: Lemma for zarcmp 33317. (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 20139	. . . 4 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2		zartop.1	. . . . 5 ⊢ 𝑆 = (Spec‘𝑅)
3		zartop.2	. . . . 5 ⊢ 𝐽 = (TopOpen‘𝑆)
4		eqid 2724	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	2, 3, 4	zar0ring 33313	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅})
6	1, 5	sylan 579	. . 3 ⊢ ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) = 1) → 𝐽 = {∅})
7		0cmp 23219	. . 3 ⊢ {∅} ∈ Comp
8	6, 7	eqeltrdi 2833	. 2 ⊢ ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) = 1) → 𝐽 ∈ Comp)
9	2, 3	zartop 33311	. . 3 ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top)
10		zarcmplem.1	. . . . . . . . . . . . . . 15 ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})
11		fvex 6894	. . . . . . . . . . . . . . . 16 ⊢ (LIdeal‘𝑅) ∈ V
12	11	mptex 7216	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ∈ V
13	10, 12	eqeltri 2821	. . . . . . . . . . . . . 14 ⊢ 𝑉 ∈ V
14		imaexg 7899	. . . . . . . . . . . . . 14 ⊢ (𝑉 ∈ V → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ∈ V)
15	13, 14	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ∈ V)
16		suppssdm 8156	. . . . . . . . . . . . . . 15 ⊢ (𝑎 supp (0_g‘𝑅)) ⊆ dom 𝑎
17		imass2 6091	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 supp (0_g‘𝑅)) ⊆ dom 𝑎 → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ⊆ (𝑉 “ dom 𝑎))
18	16, 17	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ⊆ (𝑉 “ dom 𝑎))
19	10	funmpt2 6577	. . . . . . . . . . . . . . 15 ⊢ Fun 𝑉
20		ssidd 3997	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 ⊆ dom 𝑎)
21		simpllr 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥)))
22		fvexd 6896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → (Base‘𝑅) ∈ V)
23	13	cnvex 7909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ^◡𝑉 ∈ V
24	23	imaex 7900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (^◡𝑉 “ 𝑥) ∈ V
25	24	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → (^◡𝑉 “ 𝑥) ∈ V)
26	22, 25	elmapd 8829	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → (𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥)) ↔ 𝑎:(^◡𝑉 “ 𝑥)⟶(Base‘𝑅)))
27	21, 26	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → 𝑎:(^◡𝑉 “ 𝑥)⟶(Base‘𝑅))
28	27	fdmd 6718	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → dom 𝑎 = (^◡𝑉 “ 𝑥))
29	28	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 = (^◡𝑉 “ 𝑥))
30	20, 29	sseqtrd 4014	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → dom 𝑎 ⊆ (^◡𝑉 “ 𝑥))
31		funimass2 6621	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝑉 ∧ dom 𝑎 ⊆ (^◡𝑉 “ 𝑥)) → (𝑉 “ dom 𝑎) ⊆ 𝑥)
32	19, 30, 31	sylancr 586	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ dom 𝑎) ⊆ 𝑥)
33	18, 32	sstrd 3984	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ⊆ 𝑥)
34	15, 33	elpwd 4600	. . . . . . . . . . . 12 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ∈ 𝒫 𝑥)
35		simpllr 773	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑎 finSupp (0_g‘𝑅))
36	35	fsuppimpd 9364	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0_g‘𝑅)) ∈ Fin)
37		imafi 9170	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑉 ∧ (𝑎 supp (0_g‘𝑅)) ∈ Fin) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ∈ Fin)
38	19, 36, 37	sylancr 586	. . . . . . . . . . . 12 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ∈ Fin)
39	34, 38	elind 4186	. . . . . . . . . . 11 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉 “ (𝑎 supp (0_g‘𝑅))) ∈ (𝒫 𝑥 ∩ Fin))
40		inteq 4943	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑉 “ (𝑎 supp (0_g‘𝑅))) → ∩ 𝑦 = ∩ (𝑉 “ (𝑎 supp (0_g‘𝑅))))
41	40	eqeq2d 2735	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑉 “ (𝑎 supp (0_g‘𝑅))) → (∅ = ∩ 𝑦 ↔ ∅ = ∩ (𝑉 “ (𝑎 supp (0_g‘𝑅)))))
42	41	adantl 481	. . . . . . . . . . 11 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑦 = (𝑉 “ (𝑎 supp (0_g‘𝑅)))) → (∅ = ∩ 𝑦 ↔ ∅ = ∩ (𝑉 “ (𝑎 supp (0_g‘𝑅)))))
43	16, 29	sseqtrid 4026	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0_g‘𝑅)) ⊆ (^◡𝑉 “ 𝑥))
44		cnvimass 6070	. . . . . . . . . . . . . 14 ⊢ (^◡𝑉 “ 𝑥) ⊆ dom 𝑉
45	43, 44	sstrdi 3986	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0_g‘𝑅)) ⊆ dom 𝑉)
46		intimafv 32367	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑉 ∧ (𝑎 supp (0_g‘𝑅)) ⊆ dom 𝑉) → ∩ (𝑉 “ (𝑎 supp (0_g‘𝑅))) = ∩ 𝑙 ∈ (𝑎 supp (0_g‘𝑅))(𝑉‘𝑙))
47	19, 45, 46	sylancr 586	. . . . . . . . . . . 12 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∩ (𝑉 “ (𝑎 supp (0_g‘𝑅))) = ∩ 𝑙 ∈ (𝑎 supp (0_g‘𝑅))(𝑉‘𝑙))
48		simplll 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝑅 ∈ CRing)
49	48	crngringd 20140	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝑅 ∈ Ring)
50	49	ad4antr 729	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑅 ∈ Ring)
51		fvex 6894	. . . . . . . . . . . . . . . 16 ⊢ (PrmIdeal‘𝑅) ∈ V
52	51	rabex 5322	. . . . . . . . . . . . . . 15 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} ∈ V
53	52, 10	dmmpti 6684	. . . . . . . . . . . . . 14 ⊢ dom 𝑉 = (LIdeal‘𝑅)
54	45, 53	sseqtrdi 4024	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0_g‘𝑅)) ⊆ (LIdeal‘𝑅))
55		simp-7r 787	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (♯‘(Base‘𝑅)) ≠ 1)
56		simpllr 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (1_r‘𝑅) = (𝑅 Σ_g 𝑎))
57		eqid 2724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
58		ringcmn 20170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
59	1, 58	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd)
60	59	ad8antr 737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → 𝑅 ∈ CMnd)
61	24	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (^◡𝑉 “ 𝑥) ∈ V)
62	27	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → 𝑎:(^◡𝑉 “ 𝑥)⟶(Base‘𝑅))
63		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (𝑎 supp (0_g‘𝑅)) = ∅)
64		ssidd 3997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → ∅ ⊆ ∅)
65	63, 64	eqsstrd 4012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (𝑎 supp (0_g‘𝑅)) ⊆ ∅)
66	35	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → 𝑎 finSupp (0_g‘𝑅))
67	4, 57, 60, 61, 62, 65, 66	gsumres 19822	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (𝑅 Σ_g (𝑎 ↾ ∅)) = (𝑅 Σ_g 𝑎))
68		res0 5975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ↾ ∅) = ∅
69	68	oveq2i 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Σ_g (𝑎 ↾ ∅)) = (𝑅 Σ_g ∅)
70	57	gsum0 18606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Σ_g ∅) = (0_g‘𝑅)
71	69, 70	eqtri 2752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 Σ_g (𝑎 ↾ ∅)) = (0_g‘𝑅)
72	67, 71	eqtr3di 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (𝑅 Σ_g 𝑎) = (0_g‘𝑅))
73	56, 72	eqtr2d 2765	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (0_g‘𝑅) = (1_r‘𝑅))
74		eqid 2724	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
75	4, 57, 74	01eq0ring 20419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ (0_g‘𝑅) = (1_r‘𝑅)) → (Base‘𝑅) = {(0_g‘𝑅)})
76	50, 73, 75	syl2an2r 682	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (Base‘𝑅) = {(0_g‘𝑅)})
77	76	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (♯‘(Base‘𝑅)) = (♯‘{(0_g‘𝑅)}))
78		fvex 6894	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝑅) ∈ V
79		hashsng 14325	. . . . . . . . . . . . . . . 16 ⊢ ((0_g‘𝑅) ∈ V → (♯‘{(0_g‘𝑅)}) = 1)
80	78, 79	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (♯‘{(0_g‘𝑅)}) = 1
81	77, 80	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ (𝑎 supp (0_g‘𝑅)) = ∅) → (♯‘(Base‘𝑅)) = 1)
82	55, 81	mteqand 3025	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0_g‘𝑅)) ≠ ∅)
83		eqid 2724	. . . . . . . . . . . . . 14 ⊢ (RSpan‘𝑅) = (RSpan‘𝑅)
84	10, 83	zarclsiin 33306	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ (𝑎 supp (0_g‘𝑅)) ⊆ (LIdeal‘𝑅) ∧ (𝑎 supp (0_g‘𝑅)) ≠ ∅) → ∩ 𝑙 ∈ (𝑎 supp (0_g‘𝑅))(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅)))))
85	50, 54, 82, 84	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∩ 𝑙 ∈ (𝑎 supp (0_g‘𝑅))(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅)))))
86		nfv 1909	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑙((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎))
87		nfra1 3273	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑙∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙
88	86, 87	nfan 1894	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑙(((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)
89	54	sselda 3974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0_g‘𝑅))) → 𝑙 ∈ (LIdeal‘𝑅))
90		eqid 2724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
91	4, 90	lidlss 21060	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑙 ∈ (LIdeal‘𝑅) → 𝑙 ⊆ (Base‘𝑅))
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑙 ∈ (𝑎 supp (0_g‘𝑅))) → 𝑙 ⊆ (Base‘𝑅))
93	92	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑙 ∈ (𝑎 supp (0_g‘𝑅)) → 𝑙 ⊆ (Base‘𝑅)))
94	88, 93	ralrimi 3246	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∀𝑙 ∈ (𝑎 supp (0_g‘𝑅))𝑙 ⊆ (Base‘𝑅))
95		unissb 4933	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ (𝑎 supp (0_g‘𝑅)) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (𝑎 supp (0_g‘𝑅))𝑙 ⊆ (Base‘𝑅))
96	94, 95	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∪ (𝑎 supp (0_g‘𝑅)) ⊆ (Base‘𝑅))
97	83, 4, 90	rspcl 21083	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ∪ (𝑎 supp (0_g‘𝑅)) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ∈ (LIdeal‘𝑅))
98	50, 96, 97	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ∈ (LIdeal‘𝑅))
99	4, 90	lidlss 21060	. . . . . . . . . . . . . . . 16 ⊢ (((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ∈ (LIdeal‘𝑅) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ⊆ (Base‘𝑅))
100	98, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ⊆ (Base‘𝑅))
101	83, 4, 74	rsp1 21085	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → ((RSpan‘𝑅)‘{(1_r‘𝑅)}) = (Base‘𝑅))
102	50, 101	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1_r‘𝑅)}) = (Base‘𝑅))
103	27	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑎:(^◡𝑉 “ 𝑥)⟶(Base‘𝑅))
104	103, 43	fssresd 6748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0_g‘𝑅))):(𝑎 supp (0_g‘𝑅))⟶(Base‘𝑅))
105		fvex 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘𝑅) ∈ V
106		ovex 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 supp (0_g‘𝑅)) ∈ V
107	105, 106	elmap 8860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ↾ (𝑎 supp (0_g‘𝑅))) ∈ ((Base‘𝑅) ↑_m (𝑎 supp (0_g‘𝑅))) ↔ (𝑎 ↾ (𝑎 supp (0_g‘𝑅))):(𝑎 supp (0_g‘𝑅))⟶(Base‘𝑅))
108	104, 107	sylibr 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) ∈ ((Base‘𝑅) ↑_m (𝑎 supp (0_g‘𝑅))))
109		breq1 5141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → (𝑏 finSupp (0_g‘𝑅) ↔ (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) finSupp (0_g‘𝑅)))
110		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → (𝑅 Σ_g 𝑏) = (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))))
111	110	eqeq2d 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → ((1_r‘𝑅) = (𝑅 Σ_g 𝑏) ↔ (1_r‘𝑅) = (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅))))))
112		fveq1 6880	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → (𝑏‘𝑘) = ((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘))
113	112	eleq1d 2810	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → ((𝑏‘𝑘) ∈ 𝑘 ↔ ((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘))
114	113	ralbidv 3169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → (∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))(𝑏‘𝑘) ∈ 𝑘 ↔ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘))
115	109, 111, 114	3anbi123d 1432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) → ((𝑏 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))(𝑏‘𝑘) ∈ 𝑘) ↔ ((𝑎 ↾ (𝑎 supp (0_g‘𝑅))) finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘)))
116	115	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑏 = (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))) → ((𝑏 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))(𝑏‘𝑘) ∈ 𝑘) ↔ ((𝑎 ↾ (𝑎 supp (0_g‘𝑅))) finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘)))
117		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (0_g‘𝑅) ∈ V)
118	35, 117	fsuppres 9383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 ↾ (𝑎 supp (0_g‘𝑅))) finSupp (0_g‘𝑅))
119		simplr 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1_r‘𝑅) = (𝑅 Σ_g 𝑎))
120	50, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → 𝑅 ∈ CMnd)
121	24	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (^◡𝑉 “ 𝑥) ∈ V)
122		ssidd 3997	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎 supp (0_g‘𝑅)) ⊆ (𝑎 supp (0_g‘𝑅)))
123	4, 57, 120, 121, 103, 122, 35	gsumres 19822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))) = (𝑅 Σ_g 𝑎))
124	119, 123	eqtr4d 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1_r‘𝑅) = (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))))
125		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) → 𝑘 ∈ (𝑎 supp (0_g‘𝑅)))
126	125	fvresd 6901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) → ((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) = (𝑎‘𝑘))
127	16, 28	sseqtrid 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) → (𝑎 supp (0_g‘𝑅)) ⊆ (^◡𝑉 “ 𝑥))
128	127	sselda 3974	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) → 𝑘 ∈ (^◡𝑉 “ 𝑥))
129		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑙 = 𝑘 → (𝑎‘𝑙) = (𝑎‘𝑘))
130		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘)
131	129, 130	eleq12d 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑙 = 𝑘 → ((𝑎‘𝑙) ∈ 𝑙 ↔ (𝑎‘𝑘) ∈ 𝑘))
132	131	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) ∧ 𝑙 = 𝑘) → ((𝑎‘𝑙) ∈ 𝑙 ↔ (𝑎‘𝑘) ∈ 𝑘))
133	128, 132	rspcdv 3596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) → (∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 → (𝑎‘𝑘) ∈ 𝑘))
134	133	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑎‘𝑘) ∈ 𝑘)
135	134	an32s 649	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) → (𝑎‘𝑘) ∈ 𝑘)
136	126, 135	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) ∧ 𝑘 ∈ (𝑎 supp (0_g‘𝑅))) → ((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘)
137	136	ralrimiva 3138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘)
138	118, 124, 137	3jca 1125	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((𝑎 ↾ (𝑎 supp (0_g‘𝑅))) finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g (𝑎 ↾ (𝑎 supp (0_g‘𝑅)))) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))((𝑎 ↾ (𝑎 supp (0_g‘𝑅)))‘𝑘) ∈ 𝑘))
139	108, 116, 138	rspcedvd 3606	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∃𝑏 ∈ ((Base‘𝑅) ↑_m (𝑎 supp (0_g‘𝑅)))(𝑏 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))(𝑏‘𝑘) ∈ 𝑘))
140		eqid 2724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (._r‘𝑅) = (._r‘𝑅)
141	83, 4, 57, 140, 50, 54	elrspunidl 32981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((1_r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ↔ ∃𝑏 ∈ ((Base‘𝑅) ↑_m (𝑎 supp (0_g‘𝑅)))(𝑏 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑏) ∧ ∀𝑘 ∈ (𝑎 supp (0_g‘𝑅))(𝑏‘𝑘) ∈ 𝑘)))
142	139, 141	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (1_r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))))
143	142	snssd 4804	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → {(1_r‘𝑅)} ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))))
144	83, 90	rspssp 21087	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) ∈ (LIdeal‘𝑅) ∧ {(1_r‘𝑅)} ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅)))) → ((RSpan‘𝑅)‘{(1_r‘𝑅)}) ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))))
145	50, 98, 143, 144	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘{(1_r‘𝑅)}) ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))))
146	102, 145	eqsstrrd 4013	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (Base‘𝑅) ⊆ ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))))
147	100, 146	eqssd 3991	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅))) = (Base‘𝑅))
148	147	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅)))) = (𝑉‘(Base‘𝑅)))
149	90, 4	lidl1 21081	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → (Base‘𝑅) ∈ (LIdeal‘𝑅))
150	1, 149	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ CRing → (Base‘𝑅) ∈ (LIdeal‘𝑅))
151	10, 4	zarcls1 33304	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRing ∧ (Base‘𝑅) ∈ (LIdeal‘𝑅)) → ((𝑉‘(Base‘𝑅)) = ∅ ↔ (Base‘𝑅) = (Base‘𝑅)))
152	150, 151	mpdan 684	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ CRing → ((𝑉‘(Base‘𝑅)) = ∅ ↔ (Base‘𝑅) = (Base‘𝑅)))
153	4, 152	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ CRing → (𝑉‘(Base‘𝑅)) = ∅)
154	153	ad7antr 735	. . . . . . . . . . . . 13 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘(Base‘𝑅)) = ∅)
155	148, 154	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → (𝑉‘((RSpan‘𝑅)‘∪ (𝑎 supp (0_g‘𝑅)))) = ∅)
156	47, 85, 155	3eqtrrd 2769	. . . . . . . . . . 11 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∅ = ∩ (𝑉 “ (𝑎 supp (0_g‘𝑅))))
157	39, 42, 156	rspcedvd 3606	. . . . . . . . . 10 ⊢ ((((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ 𝑎 finSupp (0_g‘𝑅)) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎)) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)
158	157	exp41 434	. . . . . . . . 9 ⊢ (((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) → (𝑎 finSupp (0_g‘𝑅) → ((1_r‘𝑅) = (𝑅 Σ_g 𝑎) → (∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦))))
159	158	3imp2 1346	. . . . . . . 8 ⊢ ((((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))) ∧ (𝑎 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)
160	4, 74	ringidcl 20154	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ (Base‘𝑅))
161	49, 160	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → (1_r‘𝑅) ∈ (Base‘𝑅))
162		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝑥 ∈ 𝒫 (Clsd‘𝐽))
163		eqid 2724	. . . . . . . . . . . . . . . . . . 19 ⊢ (PrmIdeal‘𝑅) = (PrmIdeal‘𝑅)
164	2, 3, 163, 10	zartopn 33310	. . . . . . . . . . . . . . . . . 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 4611	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝒫 ran 𝑉 = 𝒫 (Clsd‘𝐽))
168	162, 167	eleqtrrd 2828	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝑥 ∈ 𝒫 ran 𝑉)
169	168	elpwid 4603	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝑥 ⊆ ran 𝑉)
170		intimafv 32367	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝑉 ∧ (^◡𝑉 “ 𝑥) ⊆ dom 𝑉) → ∩ (𝑉 “ (^◡𝑉 “ 𝑥)) = ∩ 𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑉‘𝑙))
171	19, 44, 170	mp2an 689	. . . . . . . . . . . . . 14 ⊢ ∩ (𝑉 “ (^◡𝑉 “ 𝑥)) = ∩ 𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑉‘𝑙)
172		funimacnv 6619	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑉 → (𝑉 “ (^◡𝑉 “ 𝑥)) = (𝑥 ∩ ran 𝑉))
173	19, 172	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 “ (^◡𝑉 “ 𝑥)) = (𝑥 ∩ ran 𝑉)
174		df-ss 3957	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ⊆ ran 𝑉 ↔ (𝑥 ∩ ran 𝑉) = 𝑥)
175	174	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ ran 𝑉 → (𝑥 ∩ ran 𝑉) = 𝑥)
176	173, 175	eqtrid 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ⊆ ran 𝑉 → (𝑉 “ (^◡𝑉 “ 𝑥)) = 𝑥)
177	176	inteqd 4945	. . . . . . . . . . . . . 14 ⊢ (𝑥 ⊆ ran 𝑉 → ∩ (𝑉 “ (^◡𝑉 “ 𝑥)) = ∩ 𝑥)
178	171, 177	eqtr3id 2778	. . . . . . . . . . . . 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 4024	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → (^◡𝑉 “ 𝑥) ⊆ (LIdeal‘𝑅))
182	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → Fun 𝑉)
183		inteq 4943	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ∅ → ∩ 𝑥 = ∩ ∅)
184		int0 4956	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ ∅ = V
185	183, 184	eqtrdi 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∅ → ∩ 𝑥 = V)
186		vn0 4330	. . . . . . . . . . . . . . . . . 18 ⊢ V ≠ ∅
187		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (∩ 𝑥 = V → (∩ 𝑥 ≠ ∅ ↔ V ≠ ∅))
188	186, 187	mpbiri 258	. . . . . . . . . . . . . . . . 17 ⊢ (∩ 𝑥 = V → ∩ 𝑥 ≠ ∅)
189	185, 188	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → ∩ 𝑥 ≠ ∅)
190	189	necon2i 2967	. . . . . . . . . . . . . . 15 ⊢ (∩ 𝑥 = ∅ → 𝑥 ≠ ∅)
191	190	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → 𝑥 ≠ ∅)
192		preiman0 32366	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝑉 ∧ 𝑥 ⊆ ran 𝑉 ∧ 𝑥 ≠ ∅) → (^◡𝑉 “ 𝑥) ≠ ∅)
193	182, 169, 191, 192	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → (^◡𝑉 “ 𝑥) ≠ ∅)
194	10, 83	zarclsiin 33306	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ (^◡𝑉 “ 𝑥) ⊆ (LIdeal‘𝑅) ∧ (^◡𝑉 “ 𝑥) ≠ ∅) → ∩ 𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥))))
195	49, 181, 193, 194	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∩ 𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥))))
196		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∩ 𝑥 = ∅)
197	179, 195, 196	3eqtr3d 2772	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → (𝑉‘((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥))) = ∅)
198	181	sselda 3974	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑙 ∈ (^◡𝑉 “ 𝑥)) → 𝑙 ∈ (LIdeal‘𝑅))
199	198, 91	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) ∧ 𝑙 ∈ (^◡𝑉 “ 𝑥)) → 𝑙 ⊆ (Base‘𝑅))
200	199	ralrimiva 3138	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∀𝑙 ∈ (^◡𝑉 “ 𝑥)𝑙 ⊆ (Base‘𝑅))
201		unissb 4933	. . . . . . . . . . . . . 14 ⊢ (∪ (^◡𝑉 “ 𝑥) ⊆ (Base‘𝑅) ↔ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)𝑙 ⊆ (Base‘𝑅))
202	200, 201	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∪ (^◡𝑉 “ 𝑥) ⊆ (Base‘𝑅))
203	83, 4, 90	rspcl 21083	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ ∪ (^◡𝑉 “ 𝑥) ⊆ (Base‘𝑅)) → ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅))
204	49, 202, 203	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅))
205	10, 4	zarcls1 33304	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) ∈ (LIdeal‘𝑅)) → ((𝑉‘((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) = (Base‘𝑅)))
206	48, 204, 205	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ((𝑉‘((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥))) = ∅ ↔ ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) = (Base‘𝑅)))
207	197, 206	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) = (Base‘𝑅))
208	161, 207	eleqtrrd 2828	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → (1_r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)))
209	83, 4, 57, 140, 49, 181	elrspunidl 32981	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ((1_r‘𝑅) ∈ ((RSpan‘𝑅)‘∪ (^◡𝑉 “ 𝑥)) ↔ ∃𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))(𝑎 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙)))
210	208, 209	mpbid 231	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∃𝑎 ∈ ((Base‘𝑅) ↑_m (^◡𝑉 “ 𝑥))(𝑎 finSupp (0_g‘𝑅) ∧ (1_r‘𝑅) = (𝑅 Σ_g 𝑎) ∧ ∀𝑙 ∈ (^◡𝑉 “ 𝑥)(𝑎‘𝑙) ∈ 𝑙))
211	159, 210	r19.29a 3154	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)
212		0ex 5297	. . . . . . . 8 ⊢ ∅ ∈ V
213		vex 3470	. . . . . . . 8 ⊢ 𝑥 ∈ V
214		elfi 9403	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝑥 ∈ V) → (∅ ∈ (fi‘𝑥) ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦))
215	212, 213, 214	mp2an 689	. . . . . . 7 ⊢ (∅ ∈ (fi‘𝑥) ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∅ = ∩ 𝑦)
216	211, 215	sylibr 233	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) ∧ ∩ 𝑥 = ∅) → ∅ ∈ (fi‘𝑥))
217	216	ex 412	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (∩ 𝑥 = ∅ → ∅ ∈ (fi‘𝑥)))
218	217	necon3bd 2946	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → (¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅))
219	218	ralrimiva 3138	. . 3 ⊢ ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) → ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅))
220		cmpfi 23233	. . . 4 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))
221	220	biimpar 477	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)) → 𝐽 ∈ Comp)
222	9, 219, 221	syl2an2r 682	. 2 ⊢ ((𝑅 ∈ CRing ∧ (♯‘(Base‘𝑅)) ≠ 1) → 𝐽 ∈ Comp)
223	8, 222	pm2.61dane 3021	1 ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2932 ∀wral 3053 ∃wrex 3062 {crab 3424 Vcvv 3466 ∩ cin 3939 ⊆ wss 3940 ∅c0 4314 𝒫 cpw 4594 {csn 4620 ∪ cuni 4899 ∩ cint 4940 ∩ ciin 4988 class class class wbr 5138 ↦ cmpt 5221 ^◡ccnv 5665 dom cdm 5666 ran crn 5667 ↾ cres 5668 “ cima 5669 Fun wfun 6527 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 supp csupp 8140 ↑_m cmap 8815 Fincfn 8934 finSupp cfsupp 9356 ficfi 9400 1c1 11106 ♯chash 14286 Basecbs 17142 ._rcmulr 17196 TopOpenctopn 17365 0_gc0g 17383 Σ_g cgsu 17384 CMndccmn 19689 1_rcur 20075 Ringcrg 20127 CRingccrg 20128 LIdealclidl 21054 RSpancrsp 21055 Topctop 22716 TopOnctopon 22733 Clsdccld 22841 Compccmp 23211 PrmIdealcprmidl 32988 Speccrspec 33297

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-reg 9582 ax-inf2 9631 ax-ac2 10453 ax-cnex 11161 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 ax-pre-mulgt0 11182 ax-addf 11184 ax-mulf 11185

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-tp 4625 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-iin 4990 df-disj 5104 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-se 5622 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-of 7663 df-rpss 7706 df-om 7849 df-1st 7968 df-2nd 7969 df-supp 8141 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-oadd 8465 df-er 8698 df-map 8817 df-ixp 8887 df-en 8935 df-dom 8936 df-sdom 8937 df-fin 8938 df-fsupp 9357 df-fi 9401 df-sup 9432 df-oi 9500 df-r1 9754 df-rank 9755 df-dju 9891 df-card 9929 df-ac 10106 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-fzo 13624 df-seq 13963 df-hash 14287 df-struct 17078 df-sets 17095 df-slot 17113 df-ndx 17125 df-base 17143 df-ress 17172 df-plusg 17208 df-mulr 17209 df-starv 17210 df-sca 17211 df-vsca 17212 df-ip 17213 df-tset 17214 df-ple 17215 df-ds 17217 df-unif 17218 df-hom 17219 df-cco 17220 df-rest 17366 df-topn 17367 df-0g 17385 df-gsum 17386 df-prds 17391 df-pws 17393 df-mre 17528 df-mrc 17529 df-acs 17531 df-mgm 18562 df-sgrp 18641 df-mnd 18657 df-mhm 18702 df-submnd 18703 df-grp 18855 df-minusg 18856 df-sbg 18857 df-mulg 18985 df-subg 19039 df-ghm 19128 df-cntz 19222 df-lsm 19545 df-cmn 19691 df-abl 19692 df-mgp 20029 df-rng 20047 df-ur 20076 df-ring 20129 df-cring 20130 df-rhm 20363 df-nzr 20404 df-subrng 20435 df-subrg 20460 df-lmod 20697 df-lss 20768 df-lsp 20808 df-lmhm 20859 df-lbs 20912 df-sra 21010 df-rgmod 21011 df-lidl 21056 df-rsp 21057 df-lpidl 21164 df-cnfld 21228 df-zring 21301 df-zrh 21357 df-dsmm 21594 df-frlm 21609 df-uvc 21645 df-top 22717 df-topon 22734 df-cld 22844 df-cmp 23212 df-prmidl 32989 df-mxidl 33011 df-idlsrg 33050 df-rspec 33298

This theorem is referenced by: zarcmp 33317

W3C validator