Metamath Proof Explorer

Definition df-rgspn

Description: The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014)

Ref Expression
Assertion df-rgspn ⊢ RingSpan = w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ ⋂ t ∈ SubRing ⁡ w | s ⊆ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 crgspn class RingSpan
1 vw setvar w
2 cvv class V
3 vs setvar s
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 vt setvar t
9 csubrg class SubRing
10 5 9 cfv class SubRing ⁡ w
11 3 cv setvar s
12 8 cv setvar t
13 11 12 wss wff s ⊆ t
14 13 8 10 crab class t ∈ SubRing ⁡ w | s ⊆ t
15 14 cint class ⋂ t ∈ SubRing ⁡ w | s ⊆ t
16 3 7 15 cmpt class s ∈ 𝒫 Base w ⟼ ⋂ t ∈ SubRing ⁡ w | s ⊆ t
17 1 2 16 cmpt class w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ ⋂ t ∈ SubRing ⁡ w | s ⊆ t
18 0 17 wceq wff RingSpan = w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ ⋂ t ∈ SubRing ⁡ w | s ⊆ t