This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑠 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )