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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑊 ∈ 𝑋 → 𝑆 = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )