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 } ∈ 𝑆 )