This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lssatomic

Description: The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. ( shatomici analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lssatomic.s ⊢ S = LSubSp ⁡ W
lssatomic.o ⊢ 0 ˙ = 0 W
lssatomic.a ⊢ A = LSAtoms ⁡ W
lssatomic.w ⊢ φ → W ∈ LMod
lssatomic.u ⊢ φ → U ∈ S
lssatomic.n ⊢ φ → U ≠ 0 ˙
Assertion lssatomic ⊢ φ → ∃ q ∈ A q ⊆ U

Proof

Step Hyp Ref Expression
1 lssatomic.s ⊢ S = LSubSp ⁡ W
2 lssatomic.o ⊢ 0 ˙ = 0 W
3 lssatomic.a ⊢ A = LSAtoms ⁡ W
4 lssatomic.w ⊢ φ → W ∈ LMod
5 lssatomic.u ⊢ φ → U ∈ S
6 lssatomic.n ⊢ φ → U ≠ 0 ˙
7 2 1 lssne0 ⊢ U ∈ S → U ≠ 0 ˙ ↔ ∃ x ∈ U x ≠ 0 ˙
8 5 7 syl ⊢ φ → U ≠ 0 ˙ ↔ ∃ x ∈ U x ≠ 0 ˙
9 6 8 mpbid ⊢ φ → ∃ x ∈ U x ≠ 0 ˙
10 4 3ad2ant1 ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → W ∈ LMod
11 5 3ad2ant1 ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → U ∈ S
12 simp2 ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → x ∈ U
13 eqid ⊢ Base W = Base W
14 13 1 lssel ⊢ U ∈ S ∧ x ∈ U → x ∈ Base W
15 11 12 14 syl2anc ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → x ∈ Base W
16 simp3 ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → x ≠ 0 ˙
17 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
18 13 17 2 3 lsatlspsn2 ⊢ W ∈ LMod ∧ x ∈ Base W ∧ x ≠ 0 ˙ → LSpan ⁡ W ⁡ x ∈ A
19 10 15 16 18 syl3anc ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → LSpan ⁡ W ⁡ x ∈ A
20 1 17 10 11 12 ellspsn5 ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → LSpan ⁡ W ⁡ x ⊆ U
21 sseq1 ⊢ q = LSpan ⁡ W ⁡ x → q ⊆ U ↔ LSpan ⁡ W ⁡ x ⊆ U
22 21 rspcev ⊢ LSpan ⁡ W ⁡ x ∈ A ∧ LSpan ⁡ W ⁡ x ⊆ U → ∃ q ∈ A q ⊆ U
23 19 20 22 syl2anc ⊢ φ ∧ x ∈ U ∧ x ≠ 0 ˙ → ∃ q ∈ A q ⊆ U
24 23 rexlimdv3a ⊢ φ → ∃ x ∈ U x ≠ 0 ˙ → ∃ q ∈ A q ⊆ U
25 9 24 mpd ⊢ φ → ∃ q ∈ A q ⊆ U