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

Definition df-asp 16404
 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 16401 . 2 AlgSpan
2 vw . . 3
3 casa 16400 . . 3 AssAlg
4 vs . . . 4
52cv 1652 . . . . . 6
6 cbs 13500 . . . . . 6
75, 6cfv 5483 . . . . 5
87cpw 3823 . . . 4
94cv 1652 . . . . . . 7
10 vt . . . . . . . 8
1110cv 1652 . . . . . . 7
129, 11wss 3306 . . . . . 6
13 csubrg 15895 . . . . . . . 8 SubRing
145, 13cfv 5483 . . . . . . 7 SubRing
15 clss 16039 . . . . . . . 8
165, 15cfv 5483 . . . . . . 7
1714, 16cin 3305 . . . . . 6 SubRing
1812, 10, 17crab 2715 . . . . 5 SubRing
1918cint 4074 . . . 4 SubRing
204, 8, 19cmpt 4291 . . 3 SubRing
212, 3, 20cmpt 4291 . 2 AssAlg SubRing
221, 21wceq 1653 1 AlgSpan AssAlg SubRing
 Colors of variables: wff set class This definition is referenced by:  aspval  16418
 Copyright terms: Public domain W3C validator