lspsncv0

Description: The span of a singleton covers the zero subspace, using Definition 3.2.18 of PtakPulmannova p. 68 for "covers".) (Contributed by NM, 12-Aug-2014) (Revised by AV, 13-Jul-2022)

	Ref	Expression
Hypotheses	lspsncv0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsncv0.z	⊢ 0 = ( 0_g ‘ 𝑊 )
	lspsncv0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspsncv0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspsncv0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspsncv0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lspsncv0	⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lspsncv0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsncv0.z	⊢ 0 = ( 0_g ‘ 𝑊 )
3		lspsncv0.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4		lspsncv0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5		lspsncv0.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lspsncv0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7		df-pss	⊢ ( { 0 } ⊊ 𝑦 ↔ ( { 0 } ⊆ 𝑦 ∧ { 0 } ≠ 𝑦 ) )
8		simpr	⊢ ( ( { 0 } ⊆ 𝑦 ∧ { 0 } ≠ 𝑦 ) → { 0 } ≠ 𝑦 )
9		nesym	⊢ ( { 0 } ≠ 𝑦 ↔ ¬ 𝑦 = { 0 } )
10	8 9	sylib	⊢ ( ( { 0 } ⊆ 𝑦 ∧ { 0 } ≠ 𝑦 ) → ¬ 𝑦 = { 0 } )
11	7 10	sylbi	⊢ ( { 0 } ⊊ 𝑦 → ¬ 𝑦 = { 0 } )
12	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑊 ∈ LVec )
13		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑦 ∈ 𝑆 )
14	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋 ∈ 𝑉 )
15		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) )
16	1 2 3 4	lspsnat	⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑦 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑦 = { 0 } ) )
17	12 13 14 15 16	syl31anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑦 = { 0 } ) )
18	17	orcomd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑦 = { 0 } ∨ 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) )
19	18	ord	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ¬ 𝑦 = { 0 } → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) )
20	19	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) → ( ¬ 𝑦 = { 0 } → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) ) )
21	20	com23	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ¬ 𝑦 = { 0 } → ( 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) ) )
22		npss	⊢ ( ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ↔ ( 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) )
23	21 22	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ¬ 𝑦 = { 0 } → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
24	11 23	syl5	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
25	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
26		ralinexa	⊢ ( ∀ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ¬ ∃ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
27	25 26	sylib	⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )

Metamath Proof Explorer

Theorem lspsncv0

Proof