Definition df-lss

Description: Define the set of linear subspaces of a left module or left vector space. (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 ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 } )