Metamath Proof Explorer

Theorem lss0cl

Description: The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 lss0cl.z ⊢ 0 = ( 0g ‘ 𝑊 )
2 lss0cl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 2 lssn0 ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ≠ ∅ )
4 n0 ⊢ ( 𝑈 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑈 )
5 3 4 sylib ⊢ ( 𝑈 ∈ 𝑆 → ∃ 𝑥 𝑥 ∈ 𝑈 )
6 5 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∃ 𝑥 𝑥 ∈ 𝑈 )
7 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → 𝑊 ∈ LMod )
8 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9 8 2 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
10 9 3adant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
11 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
12 8 1 11 lmodsubid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( -g ‘ 𝑊 ) 𝑥 ) = 0 )
13 7 10 12 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( -g ‘ 𝑊 ) 𝑥 ) = 0 )
14 11 2 lssvsubcl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) ) → ( 𝑥 ( -g ‘ 𝑊 ) 𝑥 ) ∈ 𝑈 )
15 14 anabsan2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( -g ‘ 𝑊 ) 𝑥 ) ∈ 𝑈 )
16 15 3impa ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( -g ‘ 𝑊 ) 𝑥 ) ∈ 𝑈 )
17 13 16 eqeltrrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → 0 ∈ 𝑈 )
18 17 3expia ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑈 → 0 ∈ 𝑈 ) )
19 18 exlimdv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ∃ 𝑥 𝑥 ∈ 𝑈 → 0 ∈ 𝑈 ) )
20 6 19 mpd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 0 ∈ 𝑈 )