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

Metamath Proof Explorer

Theorem lssvancl1

Description: Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 . Can it be used along with lspsnne1 , lspsnne2 to shorten this proof? (Contributed by NM, 14-May-2015)

Ref Expression
Hypotheses lssvancl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lssvancl.p ⊢ + = ( +g ‘ 𝑊 )
lssvancl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssvancl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lssvancl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lssvancl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
lssvancl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lssvancl.n ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝑈 )
Assertion lssvancl1 ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lssvancl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lssvancl.p ⊢ + = ( +g ‘ 𝑊 )
3 lssvancl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4 lssvancl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lssvancl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 lssvancl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
7 lssvancl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 lssvancl.n ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝑈 )
9 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
10 4 9 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
11 1 3 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
12 5 6 11 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
14 1 2 13 ablpncan2 ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) 𝑋 ) = 𝑌 )
15 10 12 7 14 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) 𝑋 ) = 𝑌 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) 𝑋 ) = 𝑌 )
17 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → 𝑊 ∈ LMod )
18 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
19 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → ( 𝑋 + 𝑌 ) ∈ 𝑈 )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
21 13 3 lssvsubcl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( ( 𝑋 + 𝑌 ) ∈ 𝑈 ∧ 𝑋 ∈ 𝑈 ) ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
22 17 18 19 20 21 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → ( ( 𝑋 + 𝑌 ) ( -g ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
23 16 22 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
24 8 23 mtand ⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ 𝑈 )