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	⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ 𝑈 )