Metamath Proof Explorer

Theorem zarcmplem

Description: Lemma for zarcmp . (Contributed by Thierry Arnoux, 2-Jul-2024)

Ref Expression
Hypotheses zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
zarcmplem.1 ⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
Assertion zarcmplem ( 𝑅 ∈ CRing → 𝐽 ∈ Comp )

Proof

Step Hyp Ref Expression
1 zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
2 zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3 zarcmplem.1 ⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
4 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 1 2 5 zar0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → 𝐽 = { ∅ } )
7 4 6 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → 𝐽 = { ∅ } )
8 0cmp ⊢ { ∅ } ∈ Comp
9 7 8 eqeltrdi ⊢ ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → 𝐽 ∈ Comp )
10 1 2 zartop ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Top )
11 fvex ⊢ ( LIdeal ‘ 𝑅 ) ∈ V
12 11 mptex ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ∈ V
13 3 12 eqeltri ⊢ 𝑉 ∈ V
14 imaexg ⊢ ( 𝑉 ∈ V → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ V )
15 13 14 mp1i ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ V )
16 suppssdm ⊢ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ dom 𝑎
17 imass2 ⊢ ( ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ dom 𝑎 → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ( 𝑉 “ dom 𝑎 ) )
18 16 17 mp1i ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ( 𝑉 “ dom 𝑎 ) )
19 3 funmpt2 ⊢ Fun 𝑉
20 ssidd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → dom 𝑎 ⊆ dom 𝑎 )
21 simpllr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) )
22 fvexd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → ( Base ‘ 𝑅 ) ∈ V )
23 13 cnvex ⊢ ◡ 𝑉 ∈ V
24 23 imaex ⊢ ( ◡ 𝑉 “ 𝑥 ) ∈ V
25 24 a1i ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → ( ◡ 𝑉 “ 𝑥 ) ∈ V )
26 22 25 elmapd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → ( 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ↔ 𝑎 : ( ◡ 𝑉 “ 𝑥 ) ⟶ ( Base ‘ 𝑅 ) ) )
27 21 26 mpbid ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → 𝑎 : ( ◡ 𝑉 “ 𝑥 ) ⟶ ( Base ‘ 𝑅 ) )
28 27 fdmd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → dom 𝑎 = ( ◡ 𝑉 “ 𝑥 ) )
29 28 adantr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → dom 𝑎 = ( ◡ 𝑉 “ 𝑥 ) )
30 20 29 sseqtrd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → dom 𝑎 ⊆ ( ◡ 𝑉 “ 𝑥 ) )
31 funimass2 ⊢ ( ( Fun 𝑉 ∧ dom 𝑎 ⊆ ( ◡ 𝑉 “ 𝑥 ) ) → ( 𝑉 “ dom 𝑎 ) ⊆ 𝑥 )
32 19 30 31 sylancr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ dom 𝑎 ) ⊆ 𝑥 )
33 18 32 sstrd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ⊆ 𝑥 )
34 15 33 elpwd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ 𝒫 𝑥 )
35 simpllr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → 𝑎 finSupp ( 0g ‘ 𝑅 ) )
36 35 fsuppimpd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ∈ Fin )
37 imafi ⊢ ( ( Fun 𝑉 ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ∈ Fin ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin )
38 19 36 37 sylancr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ Fin )
39 34 38 elind ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( 𝒫 𝑥 ∩ Fin ) )
40 inteq ⊢ ( 𝑦 = ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ∩ 𝑦 = ∩ ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
41 40 eqeq2d ⊢ ( 𝑦 = ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ∅ = ∩ 𝑦 ↔ ∅ = ∩ ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) )
42 41 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑦 = ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ∅ = ∩ 𝑦 ↔ ∅ = ∩ ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) )
43 16 29 sseqtrid ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( ◡ 𝑉 “ 𝑥 ) )
44 cnvimass ⊢ ( ◡ 𝑉 “ 𝑥 ) ⊆ dom 𝑉
45 43 44 sstrdi ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ dom 𝑉 )
46 intimafv ⊢ ( ( Fun 𝑉 ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ dom 𝑉 ) → ∩ ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) = ∩ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑉 ‘ 𝑙 ) )
47 19 45 46 sylancr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∩ ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) = ∩ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑉 ‘ 𝑙 ) )
48 simplll ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝑅 ∈ CRing )
49 48 crngringd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝑅 ∈ Ring )
50 49 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → 𝑅 ∈ Ring )
51 fvex ⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
52 51 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ∈ V
53 52 3 dmmpti ⊢ dom 𝑉 = ( LIdeal ‘ 𝑅 )
54 45 53 sseqtrdi ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( LIdeal ‘ 𝑅 ) )
55 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 )
56 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) )
57 res0 ⊢ ( 𝑎 ↾ ∅ ) = ∅
58 57 oveq2i ⊢ ( 𝑅 Σg ( 𝑎 ↾ ∅ ) ) = ( 𝑅 Σg ∅ )
59 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
60 59 gsum0 ⊢ ( 𝑅 Σg ∅ ) = ( 0g ‘ 𝑅 )
61 58 60 eqtri ⊢ ( 𝑅 Σg ( 𝑎 ↾ ∅ ) ) = ( 0g ‘ 𝑅 )
62 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
63 4 62 syl ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CMnd )
64 63 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → 𝑅 ∈ CMnd )
65 24 a1i ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( ◡ 𝑉 “ 𝑥 ) ∈ V )
66 27 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → 𝑎 : ( ◡ 𝑉 “ 𝑥 ) ⟶ ( Base ‘ 𝑅 ) )
67 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ )
68 ssidd ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ∅ ⊆ ∅ )
69 67 68 eqsstrd ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ∅ )
70 35 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → 𝑎 finSupp ( 0g ‘ 𝑅 ) )
71 5 59 64 65 66 69 70 gsumres ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑅 Σg ( 𝑎 ↾ ∅ ) ) = ( 𝑅 Σg 𝑎 ) )
72 61 71 syl5reqr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑅 Σg 𝑎 ) = ( 0g ‘ 𝑅 ) )
73 56 72 eqtr2d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
74 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
75 5 59 74 01eq0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) = { ( 0g ‘ 𝑅 ) } )
76 50 73 75 syl2an2r ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( Base ‘ 𝑅 ) = { ( 0g ‘ 𝑅 ) } )
77 76 fveq2d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) )
78 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
79 hashsng ⊢ ( ( 0g ‘ 𝑅 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1 )
80 78 79 ax-mp ⊢ ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1
81 77 80 eqtrdi ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
82 55 81 mteqand ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ≠ ∅ )
83 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
84 3 83 zarclsiin ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ≠ ∅ ) → ∩ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) )
85 50 54 82 84 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∩ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) )
86 nfv ⊢ Ⅎ 𝑙 ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) )
87 nfra1 ⊢ Ⅎ 𝑙 ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙
88 86 87 nfan ⊢ Ⅎ 𝑙 ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 )
89 54 sselda ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
90 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
91 5 90 lidlss ⊢ ( 𝑙 ∈ ( LIdeal ‘ 𝑅 ) → 𝑙 ⊆ ( Base ‘ 𝑅 ) )
92 89 91 syl ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → 𝑙 ⊆ ( Base ‘ 𝑅 ) )
93 92 ex ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) → 𝑙 ⊆ ( Base ‘ 𝑅 ) ) )
94 88 93 ralrimi ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∀ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) 𝑙 ⊆ ( Base ‘ 𝑅 ) )
95 unissb ⊢ ( ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( Base ‘ 𝑅 ) ↔ ∀ 𝑙 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) 𝑙 ⊆ ( Base ‘ 𝑅 ) )
96 94 95 sylibr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( Base ‘ 𝑅 ) )
97 83 5 90 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( LIdeal ‘ 𝑅 ) )
98 50 96 97 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( LIdeal ‘ 𝑅 ) )
99 5 90 lidlss ⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( LIdeal ‘ 𝑅 ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ( Base ‘ 𝑅 ) )
100 98 99 syl ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ⊆ ( Base ‘ 𝑅 ) )
101 83 5 74 rsp1 ⊢ ( 𝑅 ∈ Ring → ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) = ( Base ‘ 𝑅 ) )
102 50 101 syl ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) = ( Base ‘ 𝑅 ) )
103 27 adantr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → 𝑎 : ( ◡ 𝑉 “ 𝑥 ) ⟶ ( Base ‘ 𝑅 ) )
104 103 43 fssresd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) : ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⟶ ( Base ‘ 𝑅 ) )
105 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
106 ovex ⊢ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ∈ V
107 105 106 elmap ⊢ ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ↔ ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) : ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⟶ ( Base ‘ 𝑅 ) )
108 104 107 sylibr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
109 breq1 ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( 𝑏 finSupp ( 0g ‘ 𝑅 ) ↔ ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) ) )
110 oveq2 ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( 𝑅 Σg 𝑏 ) = ( 𝑅 Σg ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) )
111 110 eqeq2d ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑏 ) ↔ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) ) )
112 fveq1 ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( 𝑏 ‘ 𝑘 ) = ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) )
113 112 eleq1d ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑏 ‘ 𝑘 ) ∈ 𝑘 ↔ ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) )
114 113 ralbidv ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ∀ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑏 ‘ 𝑘 ) ∈ 𝑘 ↔ ∀ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) )
115 109 111 114 3anbi123d ⊢ ( 𝑏 = ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑏 finSupp ( 0g ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑏 ) ∧ ∀ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑏 ‘ 𝑘 ) ∈ 𝑘 ) ↔ ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) ∧ ∀ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) ) )
116 115 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ 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 ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 0g ‘ 𝑅 ) ∈ V )
118 35 117 fsuppres ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
119 simplr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) )
120 50 62 syl ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → 𝑅 ∈ CMnd )
121 24 a1i ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ◡ 𝑉 “ 𝑥 ) ∈ V )
122 ssidd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) )
123 5 59 120 121 103 122 35 gsumres ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑅 Σg ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑅 Σg 𝑎 ) )
124 119 123 eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 1r ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) )
125 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) )
126 125 fvresd ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) = ( 𝑎 ‘ 𝑘 ) )
127 16 28 sseqtrid ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( ◡ 𝑉 “ 𝑥 ) )
128 127 sselda ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → 𝑘 ∈ ( ◡ 𝑉 “ 𝑥 ) )
129 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑎 ‘ 𝑙 ) = ( 𝑎 ‘ 𝑘 ) )
130 id ⊢ ( 𝑙 = 𝑘 → 𝑙 = 𝑘 )
131 129 130 eleq12d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ↔ ( 𝑎 ‘ 𝑘 ) ∈ 𝑘 ) )
132 131 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∧ 𝑙 = 𝑘 ) → ( ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ↔ ( 𝑎 ‘ 𝑘 ) ∈ 𝑘 ) )
133 128 132 rspcdv ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 → ( 𝑎 ‘ 𝑘 ) ∈ 𝑘 ) )
134 133 imp ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑎 ‘ 𝑘 ) ∈ 𝑘 )
135 134 an32s ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( 𝑎 ‘ 𝑘 ) ∈ 𝑘 )
136 126 135 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) ∈ 𝑘 )
137 136 ralrimiva ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∀ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( ( 𝑎 ↾ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ‘ 𝑘 ) ∈ 𝑘 )
138 118 124 137 3jca ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ 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 ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∃ 𝑏 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ( 𝑏 finSupp ( 0g ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑏 ) ∧ ∀ 𝑘 ∈ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ( 𝑏 ‘ 𝑘 ) ∈ 𝑘 ) )
140 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
141 83 5 59 140 50 54 elrspunidl ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ 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 ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
143 142 snssd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → { ( 1r ‘ 𝑅 ) } ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
144 83 90 rspssp ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ { ( 1r ‘ 𝑅 ) } ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
145 50 98 143 144 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
146 102 145 eqsstrrd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( Base ‘ 𝑅 ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
147 100 146 eqssd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) = ( Base ‘ 𝑅 ) )
148 147 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) )
149 90 5 lidl1 ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( LIdeal ‘ 𝑅 ) )
150 4 149 syl ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) ∈ ( LIdeal ‘ 𝑅 ) )
151 3 5 zarcls1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ ↔ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) )
152 150 151 mpdan ⊢ ( 𝑅 ∈ CRing → ( ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ ↔ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) )
153 5 152 mpbiri ⊢ ( 𝑅 ∈ CRing → ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ )
154 153 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 ‘ ( Base ‘ 𝑅 ) ) = ∅ )
155 148 154 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) ) = ∅ )
156 47 85 155 3eqtrrd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∅ = ∩ ( 𝑉 “ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ) )
157 39 42 156 rspcedvd ⊢ ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∅ = ∩ 𝑦 )
158 157 exp41 ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) → ( 𝑎 finSupp ( 0g ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) → ( ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∅ = ∩ 𝑦 ) ) ) )
159 158 3imp2 ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∅ = ∩ 𝑦 )
160 5 74 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
161 49 160 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
162 simplr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) )
163 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
164 1 2 163 3 zartopn ⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) ∧ ran 𝑉 = ( Clsd ‘ 𝐽 ) ) )
165 164 simprd ⊢ ( 𝑅 ∈ CRing → ran 𝑉 = ( Clsd ‘ 𝐽 ) )
166 48 165 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ran 𝑉 = ( Clsd ‘ 𝐽 ) )
167 166 pweqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝒫 ran 𝑉 = 𝒫 ( Clsd ‘ 𝐽 ) )
168 162 167 eleqtrrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝑥 ∈ 𝒫 ran 𝑉 )
169 168 elpwid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝑥 ⊆ ran 𝑉 )
170 intimafv ⊢ ( ( Fun 𝑉 ∧ ( ◡ 𝑉 “ 𝑥 ) ⊆ dom 𝑉 ) → ∩ ( 𝑉 “ ( ◡ 𝑉 “ 𝑥 ) ) = ∩ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑉 ‘ 𝑙 ) )
171 19 44 170 mp2an ⊢ ∩ ( 𝑉 “ ( ◡ 𝑉 “ 𝑥 ) ) = ∩ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑉 ‘ 𝑙 )
172 funimacnv ⊢ ( Fun 𝑉 → ( 𝑉 “ ( ◡ 𝑉 “ 𝑥 ) ) = ( 𝑥 ∩ ran 𝑉 ) )
173 19 172 ax-mp ⊢ ( 𝑉 “ ( ◡ 𝑉 “ 𝑥 ) ) = ( 𝑥 ∩ ran 𝑉 )
174 df-ss ⊢ ( 𝑥 ⊆ ran 𝑉 ↔ ( 𝑥 ∩ ran 𝑉 ) = 𝑥 )
175 174 biimpi ⊢ ( 𝑥 ⊆ ran 𝑉 → ( 𝑥 ∩ ran 𝑉 ) = 𝑥 )
176 173 175 syl5eq ⊢ ( 𝑥 ⊆ ran 𝑉 → ( 𝑉 “ ( ◡ 𝑉 “ 𝑥 ) ) = 𝑥 )
177 176 inteqd ⊢ ( 𝑥 ⊆ ran 𝑉 → ∩ ( 𝑉 “ ( ◡ 𝑉 “ 𝑥 ) ) = ∩ 𝑥 )
178 171 177 eqtr3id ⊢ ( 𝑥 ⊆ ran 𝑉 → ∩ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑉 ‘ 𝑙 ) = ∩ 𝑥 )
179 169 178 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∩ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑉 ‘ 𝑙 ) = ∩ 𝑥 )
180 44 a1i ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ◡ 𝑉 “ 𝑥 ) ⊆ dom 𝑉 )
181 180 53 sseqtrdi ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ◡ 𝑉 “ 𝑥 ) ⊆ ( LIdeal ‘ 𝑅 ) )
182 19 a1i ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → Fun 𝑉 )
183 inteq ⊢ ( 𝑥 = ∅ → ∩ 𝑥 = ∩ ∅ )
184 int0 ⊢ ∩ ∅ = V
185 183 184 eqtrdi ⊢ ( 𝑥 = ∅ → ∩ 𝑥 = V )
186 vn0 ⊢ V ≠ ∅
187 neeq1 ⊢ ( ∩ 𝑥 = V → ( ∩ 𝑥 ≠ ∅ ↔ V ≠ ∅ ) )
188 186 187 mpbiri ⊢ ( ∩ 𝑥 = V → ∩ 𝑥 ≠ ∅ )
189 185 188 syl ⊢ ( 𝑥 = ∅ → ∩ 𝑥 ≠ ∅ )
190 189 necon2i ⊢ ( ∩ 𝑥 = ∅ → 𝑥 ≠ ∅ )
191 190 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → 𝑥 ≠ ∅ )
192 preiman0 ⊢ ( ( Fun 𝑉 ∧ 𝑥 ⊆ ran 𝑉 ∧ 𝑥 ≠ ∅ ) → ( ◡ 𝑉 “ 𝑥 ) ≠ ∅ )
193 182 169 191 192 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ◡ 𝑉 “ 𝑥 ) ≠ ∅ )
194 3 83 zarclsiin ⊢ ( ( 𝑅 ∈ Ring ∧ ( ◡ 𝑉 “ 𝑥 ) ⊆ ( LIdeal ‘ 𝑅 ) ∧ ( ◡ 𝑉 “ 𝑥 ) ≠ ∅ ) → ∩ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ) )
195 49 181 193 194 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∩ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ) )
196 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∩ 𝑥 = ∅ )
197 179 195 196 3eqtr3d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ) = ∅ )
198 181 sselda ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
199 198 91 syl ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ) → 𝑙 ⊆ ( Base ‘ 𝑅 ) )
200 199 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) 𝑙 ⊆ ( Base ‘ 𝑅 ) )
201 unissb ⊢ ( ∪ ( ◡ 𝑉 “ 𝑥 ) ⊆ ( Base ‘ 𝑅 ) ↔ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) 𝑙 ⊆ ( Base ‘ 𝑅 ) )
202 200 201 sylibr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∪ ( ◡ 𝑉 “ 𝑥 ) ⊆ ( Base ‘ 𝑅 ) )
203 83 5 90 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ ∪ ( ◡ 𝑉 “ 𝑥 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ∈ ( LIdeal ‘ 𝑅 ) )
204 49 202 203 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ∈ ( LIdeal ‘ 𝑅 ) )
205 3 5 zarcls1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ) = ∅ ↔ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) = ( Base ‘ 𝑅 ) ) )
206 48 204 205 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ) = ∅ ↔ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) = ( Base ‘ 𝑅 ) ) )
207 197 206 mpbid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) = ( Base ‘ 𝑅 ) )
208 161 207 eleqtrrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) )
209 83 5 59 140 49 181 elrspunidl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ( ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ ∪ ( ◡ 𝑉 “ 𝑥 ) ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ( 𝑎 finSupp ( 0g ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ) )
210 208 209 mpbid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∃ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ( 𝑎 finSupp ( 0g ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) )
211 159 210 r19.29a ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∅ = ∩ 𝑦 )
212 0ex ⊢ ∅ ∈ V
213 vex ⊢ 𝑥 ∈ V
214 elfi ⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → ( ∅ ∈ ( fi ‘ 𝑥 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∅ = ∩ 𝑦 ) )
215 212 213 214 mp2an ⊢ ( ∅ ∈ ( fi ‘ 𝑥 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ∅ = ∩ 𝑦 )
216 211 215 sylibr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) → ∅ ∈ ( fi ‘ 𝑥 ) )
217 216 ex ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → ( ∩ 𝑥 = ∅ → ∅ ∈ ( fi ‘ 𝑥 ) ) )
218 217 necon3bd ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) )
219 218 ralrimiva ⊢ ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) → ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) )
220 cmpfi ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) )
221 220 biimpar ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) → 𝐽 ∈ Comp )
222 10 219 221 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) → 𝐽 ∈ Comp )
223 9 222 pm2.61dane ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Comp )