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

Metamath Proof Explorer

Theorem islsat

Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lsatset.v ⊢ V = Base W
lsatset.n ⊢ N = LSpan ⁡ W
lsatset.z ⊢ 0 ˙ = 0 W
lsatset.a ⊢ A = LSAtoms ⁡ W
Assertion islsat ⊢ W ∈ X → U ∈ A ↔ ∃ x ∈ V ∖ 0 ˙ U = N ⁡ x

Proof

Step Hyp Ref Expression
1 lsatset.v ⊢ V = Base W
2 lsatset.n ⊢ N = LSpan ⁡ W
3 lsatset.z ⊢ 0 ˙ = 0 W
4 lsatset.a ⊢ A = LSAtoms ⁡ W
5 1 2 3 4 lsatset ⊢ W ∈ X → A = ran ⁡ x ∈ V ∖ 0 ˙ ⟼ N ⁡ x
6 5 eleq2d ⊢ W ∈ X → U ∈ A ↔ U ∈ ran ⁡ x ∈ V ∖ 0 ˙ ⟼ N ⁡ x
7 eqid ⊢ x ∈ V ∖ 0 ˙ ⟼ N ⁡ x = x ∈ V ∖ 0 ˙ ⟼ N ⁡ x
8 fvex ⊢ N ⁡ x ∈ V
9 7 8 elrnmpti ⊢ U ∈ ran ⁡ x ∈ V ∖ 0 ˙ ⟼ N ⁡ x ↔ ∃ x ∈ V ∖ 0 ˙ U = N ⁡ x
10 6 9 bitrdi ⊢ W ∈ X → U ∈ A ↔ ∃ x ∈ V ∖ 0 ˙ U = N ⁡ x