Metamath Proof Explorer

Theorem lsssn0

Description: The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lss0cl.z ⊢ 0 = ( 0g ‘ 𝑊 )
lss0cl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lsssn0 ( 𝑊 ∈ LMod → { 0 } ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lss0cl.z ⊢ 0 = ( 0g ‘ 𝑊 )
2 lss0cl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 eqidd ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) )
4 eqidd ⊢ ( 𝑊 ∈ LMod → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
5 eqidd ⊢ ( 𝑊 ∈ LMod → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
6 eqidd ⊢ ( 𝑊 ∈ LMod → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) )
7 eqidd ⊢ ( 𝑊 ∈ LMod → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) )
8 2 a1i ⊢ ( 𝑊 ∈ LMod → 𝑆 = ( LSubSp ‘ 𝑊 ) )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 9 1 lmod0vcl ⊢ ( 𝑊 ∈ LMod → 0 ∈ ( Base ‘ 𝑊 ) )
11 10 snssd ⊢ ( 𝑊 ∈ LMod → { 0 } ⊆ ( Base ‘ 𝑊 ) )
12 1 fvexi ⊢ 0 ∈ V
13 12 snnz ⊢ { 0 } ≠ ∅
14 13 a1i ⊢ ( 𝑊 ∈ LMod → { 0 } ≠ ∅ )
15 simpr2 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → 𝑎 ∈ { 0 } )
16 elsni ⊢ ( 𝑎 ∈ { 0 } → 𝑎 = 0 )
17 15 16 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → 𝑎 = 0 )
18 17 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 0 ) )
19 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
21 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
22 19 20 21 1 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 0 ) = 0 )
23 22 3ad2antr1 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 0 ) = 0 )
24 18 23 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) = 0 )
25 simpr3 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → 𝑏 ∈ { 0 } )
26 elsni ⊢ ( 𝑏 ∈ { 0 } → 𝑏 = 0 )
27 25 26 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → 𝑏 = 0 )
28 24 27 oveq12d ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 0 ( +g ‘ 𝑊 ) 0 ) )
29 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
30 9 29 1 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ 0 ∈ ( Base ‘ 𝑊 ) ) → ( 0 ( +g ‘ 𝑊 ) 0 ) = 0 )
31 10 30 mpdan ⊢ ( 𝑊 ∈ LMod → ( 0 ( +g ‘ 𝑊 ) 0 ) = 0 )
32 31 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( 0 ( +g ‘ 𝑊 ) 0 ) = 0 )
33 28 32 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = 0 )
34 ovex ⊢ ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ V
35 34 elsn ⊢ ( ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ { 0 } ↔ ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = 0 )
36 33 35 sylibr ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ { 0 } ∧ 𝑏 ∈ { 0 } ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ { 0 } )
37 3 4 5 6 7 8 11 14 36 islssd ⊢ ( 𝑊 ∈ LMod → { 0 } ∈ 𝑆 )