| 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 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
| 58 |
|
ringcmn |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd ) |
| 59 |
4 58
|
syl |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CMnd ) |
| 60 |
59
|
ad8antr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → 𝑅 ∈ CMnd ) |
| 61 |
24
|
a1i |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( ◡ 𝑉 “ 𝑥 ) ∈ V ) |
| 62 |
27
|
ad2antrr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → 𝑎 : ( ◡ 𝑉 “ 𝑥 ) ⟶ ( Base ‘ 𝑅 ) ) |
| 63 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) |
| 64 |
|
ssidd |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ∅ ⊆ ∅ ) |
| 65 |
63 64
|
eqsstrd |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ∅ ) |
| 66 |
35
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → 𝑎 finSupp ( 0g ‘ 𝑅 ) ) |
| 67 |
5 57 60 61 62 65 66
|
gsumres |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ≠ 1 ) ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) ∧ ∩ 𝑥 = ∅ ) ∧ 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ◡ 𝑉 “ 𝑥 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑙 ∈ ( ◡ 𝑉 “ 𝑥 ) ( 𝑎 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) = ∅ ) → ( 𝑅 Σg ( 𝑎 ↾ ∅ ) ) = ( 𝑅 Σg 𝑎 ) ) |
| 68 |
|
res0 |
⊢ ( 𝑎 ↾ ∅ ) = ∅ |
| 69 |
68
|
oveq2i |
⊢ ( 𝑅 Σg ( 𝑎 ↾ ∅ ) ) = ( 𝑅 Σg ∅ ) |
| 70 |
57
|
gsum0 |
⊢ ( 𝑅 Σg ∅ ) = ( 0g ‘ 𝑅 ) |
| 71 |
69 70
|
eqtri |
⊢ ( 𝑅 Σg ( 𝑎 ↾ ∅ ) ) = ( 0g ‘ 𝑅 ) |
| 72 |
67 71
|
eqtr3di |
⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ 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 57 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 58
|
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 57 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 57 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 57 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 ) |