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 } ⊊ 𝑦 ∧ 𝑦 ⊊ ( 𝑁 ‘ { 𝑋 } ) ) ) |