Theorem lsppratlem1

Description: Lemma for lspprat . Let x e. ( U \ { 0 } ) (if there is no such x then U is the zero subspace), and let y e. ( U \ ( N{ x } ) ) (assuming the conclusion is false). The goal is to write X , Y in terms of x , y , which would normally be done by solving the system of linear equations. The span equivalent of this process is lspsolv (hence the name), which we use extensively below. In this lemma, we show that since x e. ( N{ X , Y } ) , either x e. ( N{ Y } ) or X e. ( N{ x , Y } ) . (Contributed by NM, 29-Aug-2014)

	Ref	Expression
Hypotheses	lspprat.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspprat.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspprat.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspprat.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspprat.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lspprat.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspprat.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspprat.p	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
	lsppratlem1.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsppratlem1.x2	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
	lsppratlem1.y2	⊢ ( 𝜑 → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
Assertion	lsppratlem1	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ∨ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lspprat.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspprat.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lspprat.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspprat.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lspprat.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		lspprat.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7		lspprat.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8		lspprat.p	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
9		lsppratlem1.o	⊢ 0 = ( 0g ‘ 𝑊 )
10		lsppratlem1.x2	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
11		lsppratlem1.y2	⊢ ( 𝜑 → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
12	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LVec )
13	7	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
14	13	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → { 𝑌 } ⊆ 𝑉 )
15	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ 𝑉 )
16	8	pssssd	⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
17	10	eldifad	⊢ ( 𝜑 → 𝑥 ∈ 𝑈 )
18	16 17	sseldd	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
19		prcom	⊢ { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
20		df-pr	⊢ { 𝑌 , 𝑋 } = ( { 𝑌 } ∪ { 𝑋 } )
21	19 20	eqtri	⊢ { 𝑋 , 𝑌 } = ( { 𝑌 } ∪ { 𝑋 } )
22	21	fveq2i	⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) )
23	18 22	eleqtrdi	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) ) )
24	23	anim1i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑥 ∈ ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
25		eldif	⊢ ( 𝑥 ∈ ( ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑥 ∈ ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
26	24 25	sylibr	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑥 ∈ ( ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ { 𝑌 } ) ) )
27	1 2 3	lspsolv	⊢ ( ( 𝑊 ∈ LVec ∧ ( { 𝑌 } ⊆ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑋 } ) ) ∖ ( 𝑁 ‘ { 𝑌 } ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑥 } ) ) )
28	12 14 15 26 27	syl13anc	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑥 } ) ) )
29		df-pr	⊢ { 𝑌 , 𝑥 } = ( { 𝑌 } ∪ { 𝑥 } )
30		prcom	⊢ { 𝑌 , 𝑥 } = { 𝑥 , 𝑌 }
31	29 30	eqtr3i	⊢ ( { 𝑌 } ∪ { 𝑥 } ) = { 𝑥 , 𝑌 }
32	31	fveq2i	⊢ ( 𝑁 ‘ ( { 𝑌 } ∪ { 𝑥 } ) ) = ( 𝑁 ‘ { 𝑥 , 𝑌 } )
33	28 32	eleqtrdi	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
34	33	ex	⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) )
35	34	orrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ∨ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) )