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