Definition df-lbs

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

	Ref	Expression
Assertion	df-lbs	⊢ LBasis = ( 𝑤 ∈ V ↦ { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clbs	⊢ LBasis
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vb	⊢ 𝑏
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		clspn	⊢ LSpan
9	5 8	cfv	⊢ ( LSpan ‘ 𝑤 )
10		vn	⊢ 𝑛
11		csca	⊢ Scalar
12	5 11	cfv	⊢ ( Scalar ‘ 𝑤 )
13		vs	⊢ 𝑠
14	10	cv	⊢ 𝑛
15	3	cv	⊢ 𝑏
16	15 14	cfv	⊢ ( 𝑛 ‘ 𝑏 )
17	16 6	wceq	⊢ ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 )
18		vx	⊢ 𝑥
19		vy	⊢ 𝑦
20	13	cv	⊢ 𝑠
21	20 4	cfv	⊢ ( Base ‘ 𝑠 )
22		c0g	⊢ 0g
23	20 22	cfv	⊢ ( 0g ‘ 𝑠 )
24	23	csn	⊢ { ( 0g ‘ 𝑠 ) }
25	21 24	cdif	⊢ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } )
26	19	cv	⊢ 𝑦
27		cvsca	⊢ ·𝑠
28	5 27	cfv	⊢ ( ·𝑠 ‘ 𝑤 )
29	18	cv	⊢ 𝑥
30	26 29 28	co	⊢ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 )
31	29	csn	⊢ { 𝑥 }
32	15 31	cdif	⊢ ( 𝑏 ∖ { 𝑥 } )
33	32 14	cfv	⊢ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) )
34	30 33	wcel	⊢ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) )
35	34	wn	⊢ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) )
36	35 19 25	wral	⊢ ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) )
37	36 18 15	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) )
38	17 37	wa	⊢ ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) )
39	38 13 12	wsbc	⊢ [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) )
40	39 10 9	wsbc	⊢ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) )
41	40 3 7	crab	⊢ { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) }
42	1 2 41	cmpt	⊢ ( 𝑤 ∈ V ↦ { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
43	0 42	wceq	⊢ LBasis = ( 𝑤 ∈ V ↦ { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )