Theorem lssset

Description: The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 15-Jul-2014)

	Ref	Expression
Hypotheses	lssset.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lssset.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	lssset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lssset.p	⊢ + = ( +g ‘ 𝑊 )
	lssset.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lssset.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssset	⊢ ( 𝑊 ∈ 𝑋 → 𝑆 = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )

Proof

Step	Hyp	Ref	Expression
1		lssset.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lssset.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		lssset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lssset.p	⊢ + = ( +g ‘ 𝑊 )
5		lssset.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lssset.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
7		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
8		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
9	8 3	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
10	9	pweqd	⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
11	10	difeq1d	⊢ ( 𝑤 = 𝑊 → ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
12		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
13	12 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
14	13	fveq2d	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝐹 ) )
15	14 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝐵 )
16		fveq2	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
17	16 5	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
18	17	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) = ( 𝑥 · 𝑎 ) )
19	18	oveq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) = ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) )
20		fveq2	⊢ ( 𝑤 = 𝑊 → ( +g ‘ 𝑤 ) = ( +g ‘ 𝑊 ) )
21	20 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( +g ‘ 𝑤 ) = + )
22	21	oveqd	⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) = ( ( 𝑥 · 𝑎 ) + 𝑏 ) )
23	19 22	eqtrd	⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) = ( ( 𝑥 · 𝑎 ) + 𝑏 ) )
24	23	eleq1d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 ↔ ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ) )
25	24	2ralbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ) )
26	15 25	raleqbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ) )
27	11 26	rabeqbidv	⊢ ( 𝑤 = 𝑊 → { 𝑠 ∈ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 } = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )
28		df-lss	⊢ LSubSp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( 𝒫 ( Base ‘ 𝑤 ) ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑎 ) ( +g ‘ 𝑤 ) 𝑏 ) ∈ 𝑠 } )
29	3	fvexi	⊢ 𝑉 ∈ V
30	29	pwex	⊢ 𝒫 𝑉 ∈ V
31	30	difexi	⊢ ( 𝒫 𝑉 ∖ { ∅ } ) ∈ V
32	31	rabex	⊢ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ∈ V
33	27 28 32	fvmpt	⊢ ( 𝑊 ∈ V → ( LSubSp ‘ 𝑊 ) = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )
34	7 33	syl	⊢ ( 𝑊 ∈ 𝑋 → ( LSubSp ‘ 𝑊 ) = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )
35	6 34	syl5eq	⊢ ( 𝑊 ∈ 𝑋 → 𝑆 = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )