Theorem lssvancl2

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. (Contributed by NM, 20-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	lssvancl2	⊢ ( 𝜑 → ¬ ( 𝑌 + 𝑋 ) ∈ 𝑈 )

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	1 3	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
10	5 6 9	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11	1 2	lmodcom	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
12	4 10 7 11	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
13	1 2 3 4 5 6 7 8	lssvancl1	⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ 𝑈 )
14	12 13	eqneltrrd	⊢ ( 𝜑 → ¬ ( 𝑌 + 𝑋 ) ∈ 𝑈 )