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 nesym ⊢ ( { 0 } ≠ 𝑦 ↔ ¬ 𝑦 = { 0 } )
9 8 bilani ⊢ ( ( { 0 } ⊆ 𝑦 ∧ { 0 } ≠ 𝑦 ) → ¬ 𝑦 = { 0 } )
10 7 9 sylbi ⊢ ( { 0 } ⊊ 𝑦 → ¬ 𝑦 = { 0 } )
11 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑊 ∈ LVec )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑦 ∈ 𝑆 )
13 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋 ∈ 𝑉 )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) )
15 1 2 3 4 lspsnat ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑦 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑦 = { 0 } ) )
16 11 12 13 14 15 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑦 = { 0 } ) )
17 16 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑦 = { 0 } ∨ 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) )
18 17 ord ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ¬ 𝑦 = { 0 } → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) )
19 18 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) → ( ¬ 𝑦 = { 0 } → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) ) )
20 19 com23 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ¬ 𝑦 = { 0 } → ( 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) ) )
21 npss ⊢ ( ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ↔ ( 𝑦 ⊆ ( 𝑁 ‘ { 𝑋 } ) → 𝑦 = ( 𝑁 ‘ { 𝑋 } ) ) )
22 20 21 imbitrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ¬ 𝑦 = { 0 } → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
23 10 22 syl5 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
25 ralinexa ⊢ ( ∀ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 → ¬ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ¬ ∃ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )
26 24 25 sylib ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ 𝑆 ( { 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) )