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

Metamath Proof Explorer

Definition df-lss

Description: Define the set of linear subspaces of a left module or left vector space: a linear subspace of a left module or left vector space is a non-empty subset of the base set of the left module/vector space with a closure condition on vector addition and scalar multiplication. (Contributed by NM, 8-Dec-2013)

Ref Expression
Assertion df-lss LSubSp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clss ⊢ LSubSp
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 cbs ⊢ Base
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( Base ‘ 𝑤 )
7 6 cpw ⊢ 𝒫 ( Base ‘ 𝑤 )
8 c0 ⊢ ∅
9 8 csn ⊢ { ∅ }
10 7 9 cdif ⊢ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } )
11 vx ⊢ 𝑥
12 csca ⊢ Scalar
13 5 12 cfv ⊢ ( Scalar ‘ 𝑤 )
14 13 4 cfv ⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) )
15 va ⊢ 𝑎
16 3 cv ⊢ 𝑠
17 vb ⊢ 𝑏
18 11 cv ⊢ 𝑥
19 cvsca ⊢ ·𝑠
20 5 19 cfv ⊢ ( ·𝑠 ‘ 𝑤 )
21 15 cv ⊢ 𝑎
22 18 21 20 co ⊢ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 )
23 cplusg ⊢ +g
24 5 23 cfv ⊢ ( +g ‘ 𝑤 )
25 17 cv ⊢ 𝑏
26 22 25 24 co ⊢ ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 )
27 26 16 wcel ⊢ ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠
28 27 17 16 wral ⊢ ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠
29 28 15 16 wral ⊢ ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠
30 29 11 14 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠
31 30 3 10 crab ⊢ { 𝑠 ∈ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 }
32 1 2 31 cmpt ⊢ ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 } )
33 0 32 wceq ⊢ LSubSp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 } )