Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-asp Structured version   Unicode version

Definition df-asp 18089
 Description: Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
df-asp AlgSpan AssAlg SubRing
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-asp
StepHypRef Expression
1 casp 18086 . 2 AlgSpan
2 vw . . 3
3 casa 18085 . . 3 AssAlg
4 vs . . . 4
52cv 1394 . . . . . 6
6 cbs 14644 . . . . . 6
75, 6cfv 5594 . . . . 5
87cpw 4015 . . . 4
94cv 1394 . . . . . . 7
10 vt . . . . . . . 8
1110cv 1394 . . . . . . 7
129, 11wss 3471 . . . . . 6
13 csubrg 17552 . . . . . . . 8 SubRing
145, 13cfv 5594 . . . . . . 7 SubRing
15 clss 17705 . . . . . . . 8
165, 15cfv 5594 . . . . . . 7
1714, 16cin 3470 . . . . . 6 SubRing
1812, 10, 17crab 2811 . . . . 5 SubRing
1918cint 4288 . . . 4 SubRing
204, 8, 19cmpt 4515 . . 3 SubRing
212, 3, 20cmpt 4515 . 2 AssAlg SubRing
221, 21wceq 1395 1 AlgSpan AssAlg SubRing
 Colors of variables: wff setvar class This definition is referenced by:  aspval  18104
 Copyright terms: Public domain W3C validator