Metamath Proof Explorer


Theorem 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 = ( 0g𝑊 )
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 = ( 0g𝑊 )
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 syl6ibr ( ( 𝜑𝑦𝑆 ) → ( ¬ 𝑦 = { 0 } → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
24 11 23 syl5 ( ( 𝜑𝑦𝑆 ) → ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
25 24 ralrimiva ( 𝜑 → ∀ 𝑦𝑆 ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
26 ralinexa ( ∀ 𝑦𝑆 ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ¬ ∃ 𝑦𝑆 ( { 0 } ⊊ 𝑦𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
27 25 26 sylib ( 𝜑 → ¬ ∃ 𝑦𝑆 ( { 0 } ⊊ 𝑦𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )