Metamath Proof Explorer

Theorem lsateln0

Description: A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses lsateln0.z ⊢ 0 ˙ = 0 W
lsateln0.a ⊢ A = LSAtoms ⁡ W
lsateln0.w ⊢ φ → W ∈ LMod
lsateln0.u ⊢ φ → U ∈ A
Assertion lsateln0 ⊢ φ → ∃ v ∈ U v ≠ 0 ˙

Proof

Step Hyp Ref Expression
1 lsateln0.z ⊢ 0 ˙ = 0 W
2 lsateln0.a ⊢ A = LSAtoms ⁡ W
3 lsateln0.w ⊢ φ → W ∈ LMod
4 lsateln0.u ⊢ φ → U ∈ A
5 eqid ⊢ Base W = Base W
6 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
7 5 6 1 2 islsat ⊢ W ∈ LMod → U ∈ A ↔ ∃ v ∈ Base W ∖ 0 ˙ U = LSpan ⁡ W ⁡ v
8 3 7 syl ⊢ φ → U ∈ A ↔ ∃ v ∈ Base W ∖ 0 ˙ U = LSpan ⁡ W ⁡ v
9 4 8 mpbid ⊢ φ → ∃ v ∈ Base W ∖ 0 ˙ U = LSpan ⁡ W ⁡ v
10 eldifi ⊢ v ∈ Base W ∖ 0 ˙ → v ∈ Base W
11 5 6 lspsnid ⊢ W ∈ LMod ∧ v ∈ Base W → v ∈ LSpan ⁡ W ⁡ v
12 3 10 11 syl2an ⊢ φ ∧ v ∈ Base W ∖ 0 ˙ → v ∈ LSpan ⁡ W ⁡ v
13 eleq2 ⊢ U = LSpan ⁡ W ⁡ v → v ∈ U ↔ v ∈ LSpan ⁡ W ⁡ v
14 12 13 syl5ibrcom ⊢ φ ∧ v ∈ Base W ∖ 0 ˙ → U = LSpan ⁡ W ⁡ v → v ∈ U
15 14 reximdva ⊢ φ → ∃ v ∈ Base W ∖ 0 ˙ U = LSpan ⁡ W ⁡ v → ∃ v ∈ Base W ∖ 0 ˙ v ∈ U
16 9 15 mpd ⊢ φ → ∃ v ∈ Base W ∖ 0 ˙ v ∈ U
17 eldifsn ⊢ v ∈ Base W ∖ 0 ˙ ↔ v ∈ Base W ∧ v ≠ 0 ˙
18 17 anbi1i ⊢ v ∈ Base W ∖ 0 ˙ ∧ v ∈ U ↔ v ∈ Base W ∧ v ≠ 0 ˙ ∧ v ∈ U
19 anass ⊢ v ∈ Base W ∧ v ≠ 0 ˙ ∧ v ∈ U ↔ v ∈ Base W ∧ v ≠ 0 ˙ ∧ v ∈ U
20 18 19 bitri ⊢ v ∈ Base W ∖ 0 ˙ ∧ v ∈ U ↔ v ∈ Base W ∧ v ≠ 0 ˙ ∧ v ∈ U
21 20 simprbi ⊢ v ∈ Base W ∖ 0 ˙ ∧ v ∈ U → v ≠ 0 ˙ ∧ v ∈ U
22 21 ancomd ⊢ v ∈ Base W ∖ 0 ˙ ∧ v ∈ U → v ∈ U ∧ v ≠ 0 ˙
23 22 reximi2 ⊢ ∃ v ∈ Base W ∖ 0 ˙ v ∈ U → ∃ v ∈ U v ≠ 0 ˙
24 16 23 syl ⊢ φ → ∃ v ∈ U v ≠ 0 ˙