Theorem lspprat

Description: A proper subspace of the span of a pair of vectors is the span of a singleton (an atom) or the zero subspace (if z is zero). Proof suggested by Mario Carneiro, 28-Aug-2014. (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	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
Assertion	lspprat	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) )

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		ssdif0	⊢ ( 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ↔ ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) = ∅ )
10		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	4 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
13	1 12	lmod0vcl	⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
14	11 13	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } )
17	12 2	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → { ( 0g ‘ 𝑊 ) } ⊆ 𝑈 )
18	11 5 17	syl2anc	⊢ ( 𝜑 → { ( 0g ‘ 𝑊 ) } ⊆ 𝑈 )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → { ( 0g ‘ 𝑊 ) } ⊆ 𝑈 )
20	16 19	eqssd	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → 𝑈 = { ( 0g ‘ 𝑊 ) } )
21	12 3	lspsn0	⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑊 ) } ) = { ( 0g ‘ 𝑊 ) } )
22	11 21	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 0g ‘ 𝑊 ) } ) = { ( 0g ‘ 𝑊 ) } )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → ( 𝑁 ‘ { ( 0g ‘ 𝑊 ) } ) = { ( 0g ‘ 𝑊 ) } )
24	20 23	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → 𝑈 = ( 𝑁 ‘ { ( 0g ‘ 𝑊 ) } ) )
25		sneq	⊢ ( 𝑧 = ( 0g ‘ 𝑊 ) → { 𝑧 } = { ( 0g ‘ 𝑊 ) } )
26	25	fveq2d	⊢ ( 𝑧 = ( 0g ‘ 𝑊 ) → ( 𝑁 ‘ { 𝑧 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑊 ) } ) )
27	26	rspceeqv	⊢ ( ( ( 0g ‘ 𝑊 ) ∈ 𝑉 ∧ 𝑈 = ( 𝑁 ‘ { ( 0g ‘ 𝑊 ) } ) ) → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) )
28	15 24 27	syl2anc	⊢ ( ( 𝜑 ∧ 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } ) → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) )
29	28	ex	⊢ ( 𝜑 → ( 𝑈 ⊆ { ( 0g ‘ 𝑊 ) } → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) )
30	9 29	biimtrrid	⊢ ( 𝜑 → ( ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) = ∅ → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) )
31	1 2	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
32	5 31	syl	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
33	32	ssdifssd	⊢ ( 𝜑 → ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ 𝑉 )
34	33	sseld	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) → 𝑧 ∈ 𝑉 ) )
35	1 2 3 4 5 6 7 8 12	lsppratlem6	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) → 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) )
36	34 35	jcad	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) → ( 𝑧 ∈ 𝑉 ∧ 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) ) )
37	36	eximdv	⊢ ( 𝜑 → ( ∃ 𝑧 𝑧 ∈ ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) → ∃ 𝑧 ( 𝑧 ∈ 𝑉 ∧ 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) ) )
38		n0	⊢ ( ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) )
39		df-rex	⊢ ( ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑉 ∧ 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) )
40	37 38 39	3imtr4g	⊢ ( 𝜑 → ( ( 𝑈 ∖ { ( 0g ‘ 𝑊 ) } ) ≠ ∅ → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) ) )
41	30 40	pm2.61dne	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 𝑈 = ( 𝑁 ‘ { 𝑧 } ) )