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 = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 casp 
 |-  AlgSpan
1 vw 
 |-  w
2 casa 
 |-  AssAlg
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 vt 
 |-  t
9 csubrg 
 |-  SubRing
10 5 9 cfv 
 |-  ( SubRing ` w )
11 clss 
 |-  LSubSp
12 5 11 cfv 
 |-  ( LSubSp ` w )
13 10 12 cin 
 |-  ( ( SubRing ` w ) i^i ( LSubSp ` w ) )
14 3 cv 
 |-  s
15 8 cv 
 |-  t
16 14 15 wss 
 |-  s C_ t
17 16 8 13 crab 
 |-  { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t }
18 17 cint 
 |-  |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t }
19 3 7 18 cmpt 
 |-  ( s e. ~P ( Base ` w ) |-> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } )
20 1 2 19 cmpt 
 |-  ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
21 0 20 wceq 
 |-  AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )