Metamath Proof Explorer


Theorem lssats2

Description: A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015)

Ref Expression
Hypotheses lssats2.s S=LSubSpW
lssats2.n N=LSpanW
lssats2.w φWLMod
lssats2.u φUS
Assertion lssats2 φU=xUNx

Proof

Step Hyp Ref Expression
1 lssats2.s S=LSubSpW
2 lssats2.n N=LSpanW
3 lssats2.w φWLMod
4 lssats2.u φUS
5 simpr φyUyU
6 3 adantr φyUWLMod
7 eqid BaseW=BaseW
8 7 1 lssel USyUyBaseW
9 4 8 sylan φyUyBaseW
10 7 2 lspsnid WLModyBaseWyNy
11 6 9 10 syl2anc φyUyNy
12 sneq x=yx=y
13 12 fveq2d x=yNx=Ny
14 13 eleq2d x=yyNxyNy
15 14 rspcev yUyNyxUyNx
16 5 11 15 syl2anc φyUxUyNx
17 16 ex φyUxUyNx
18 3 adantr φxUWLMod
19 4 adantr φxUUS
20 simpr φxUxU
21 1 2 18 19 20 lspsnel5a φxUNxU
22 21 sseld φxUyNxyU
23 22 rexlimdva φxUyNxyU
24 17 23 impbid φyUxUyNx
25 eliun yxUNxxUyNx
26 24 25 bitr4di φyUyxUNx
27 26 eqrdv φU=xUNx