Definition df-lbs 19075

Description: Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014.)

Assertion

Ref	Expression
df-lbs	|- LBasis = ( w e. _V |-> { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) } )

Distinct variable group:   n, b, s, w, x, y

Detailed syntax breakdown of Definition df-lbs

Step	Hyp	Ref	Expression
1		clbs 19074	. 2 class LBasis
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vb	. . . . . . . . . 10 setvar b
5	4	cv 1482	. . . . . . . . 9 class b
6		vn	. . . . . . . . . 10 setvar n
7	6	cv 1482	. . . . . . . . 9 class n
8	5, 7	cfv 5888	. . . . . . . 8 class ( n ` b )
9	2	cv 1482	. . . . . . . . 9 class w
10		cbs 15857	. . . . . . . . 9 class Base
11	9, 10	cfv 5888	. . . . . . . 8 class ( Base ` w )
12	8, 11	wceq 1483	. . . . . . 7 wff ( n ` b ) = ( Base ` w )
13		vy	. . . . . . . . . . . . 13 setvar y
14	13	cv 1482	. . . . . . . . . . . 12 class y
15		vx	. . . . . . . . . . . . 13 setvar x
16	15	cv 1482	. . . . . . . . . . . 12 class x
17		cvsca 15945	. . . . . . . . . . . . 13 class .s
18	9, 17	cfv 5888	. . . . . . . . . . . 12 class ( .s ` w )
19	14, 16, 18	co 6650	. . . . . . . . . . 11 class ( y ( .s ` w ) x )
20	16	csn 4177	. . . . . . . . . . . . 13 class { x }
21	5, 20	cdif 3571	. . . . . . . . . . . 12 class ( b \ { x } )
22	21, 7	cfv 5888	. . . . . . . . . . 11 class ( n ` ( b \ { x } ) )
23	19, 22	wcel 1990	. . . . . . . . . 10 wff ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
24	23	wn 3	. . . . . . . . 9 wff -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
25		vs	. . . . . . . . . . . 12 setvar s
26	25	cv 1482	. . . . . . . . . . 11 class s
27	26, 10	cfv 5888	. . . . . . . . . 10 class ( Base ` s )
28		c0g 16100	. . . . . . . . . . . 12 class 0g
29	26, 28	cfv 5888	. . . . . . . . . . 11 class ( 0g ` s )
30	29	csn 4177	. . . . . . . . . 10 class { ( 0g ` s ) }
31	27, 30	cdif 3571	. . . . . . . . 9 class ( ( Base ` s ) \ { ( 0g ` s ) } )
32	24, 13, 31	wral 2912	. . . . . . . 8 wff A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
33	32, 15, 5	wral 2912	. . . . . . 7 wff A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
34	12, 33	wa 384	. . . . . 6 wff ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) )
35		csca 15944	. . . . . . 7 class Scalar
36	9, 35	cfv 5888	. . . . . 6 class (Scalar ` w )
37	34, 25, 36	wsbc 3435	. . . . 5 wff [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) )
38		clspn 18971	. . . . . 6 class LSpan
39	9, 38	cfv 5888	. . . . 5 class ( LSpan ` w )
40	37, 6, 39	wsbc 3435	. . . 4 wff [. ( LSpan ` w ) / n ]. [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) )
41	11	cpw 4158	. . . 4 class ~P ( Base ` w )
42	40, 4, 41	crab 2916	. . 3 class { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) }
43	2, 3, 42	cmpt 4729	. 2 class ( w e. _V |-> { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) } )
44	1, 43	wceq 1483	1 wff LBasis = ( w e. _V |-> { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. (Scalar ` w ) / s ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) } )

This definition is referenced by:  islbs  19076