Metamath Proof Explorer

Definition df-asp

Description: Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Assertion df-asp AlgSpan = ( 𝑤 ∈ AssAlg ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 casp ⊢ AlgSpan
1 vw ⊢ 𝑤
2 casa ⊢ AssAlg
3 vs ⊢ 𝑠
4 cbs ⊢ Base
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( Base ‘ 𝑤 )
7 6 cpw ⊢ 𝒫 ( Base ‘ 𝑤 )
8 vt ⊢ 𝑡
9 csubrg ⊢ SubRing
10 5 9 cfv ⊢ ( SubRing ‘ 𝑤 )
11 clss ⊢ LSubSp
12 5 11 cfv ⊢ ( LSubSp ‘ 𝑤 )
13 10 12 cin ⊢ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) )
14 3 cv ⊢ 𝑠
15 8 cv ⊢ 𝑡
16 14 15 wss ⊢ 𝑠 ⊆ 𝑡
17 16 8 13 crab ⊢ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 }
18 17 cint ⊢ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 }
19 3 7 18 cmpt ⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } )
20 1 2 19 cmpt ⊢ ( 𝑤 ∈ AssAlg ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } ) )
21 0 20 wceq ⊢ AlgSpan = ( 𝑤 ∈ AssAlg ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } ) )