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 = ( LSubSp ` W )
lssats2.n
|- N = ( LSpan ` W )
lssats2.w
|- ( ph -> W e. LMod )
lssats2.u
|- ( ph -> U e. S )
Assertion lssats2
|- ( ph -> U = U_ x e. U ( N ` { x } ) )

Proof

Step Hyp Ref Expression
1 lssats2.s
 |-  S = ( LSubSp ` W )
2 lssats2.n
 |-  N = ( LSpan ` W )
3 lssats2.w
 |-  ( ph -> W e. LMod )
4 lssats2.u
 |-  ( ph -> U e. S )
5 simpr
 |-  ( ( ph /\ y e. U ) -> y e. U )
6 3 adantr
 |-  ( ( ph /\ y e. U ) -> W e. LMod )
7 eqid
 |-  ( Base ` W ) = ( Base ` W )
8 7 1 lssel
 |-  ( ( U e. S /\ y e. U ) -> y e. ( Base ` W ) )
9 4 8 sylan
 |-  ( ( ph /\ y e. U ) -> y e. ( Base ` W ) )
10 7 2 lspsnid
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) ) -> y e. ( N ` { y } ) )
11 6 9 10 syl2anc
 |-  ( ( ph /\ y e. U ) -> y e. ( N ` { y } ) )
12 sneq
 |-  ( x = y -> { x } = { y } )
13 12 fveq2d
 |-  ( x = y -> ( N ` { x } ) = ( N ` { y } ) )
14 13 eleq2d
 |-  ( x = y -> ( y e. ( N ` { x } ) <-> y e. ( N ` { y } ) ) )
15 14 rspcev
 |-  ( ( y e. U /\ y e. ( N ` { y } ) ) -> E. x e. U y e. ( N ` { x } ) )
16 5 11 15 syl2anc
 |-  ( ( ph /\ y e. U ) -> E. x e. U y e. ( N ` { x } ) )
17 16 ex
 |-  ( ph -> ( y e. U -> E. x e. U y e. ( N ` { x } ) ) )
18 3 adantr
 |-  ( ( ph /\ x e. U ) -> W e. LMod )
19 4 adantr
 |-  ( ( ph /\ x e. U ) -> U e. S )
20 simpr
 |-  ( ( ph /\ x e. U ) -> x e. U )
21 1 2 18 19 20 lspsnel5a
 |-  ( ( ph /\ x e. U ) -> ( N ` { x } ) C_ U )
22 21 sseld
 |-  ( ( ph /\ x e. U ) -> ( y e. ( N ` { x } ) -> y e. U ) )
23 22 rexlimdva
 |-  ( ph -> ( E. x e. U y e. ( N ` { x } ) -> y e. U ) )
24 17 23 impbid
 |-  ( ph -> ( y e. U <-> E. x e. U y e. ( N ` { x } ) ) )
25 eliun
 |-  ( y e. U_ x e. U ( N ` { x } ) <-> E. x e. U y e. ( N ` { x } ) )
26 24 25 bitr4di
 |-  ( ph -> ( y e. U <-> y e. U_ x e. U ( N ` { x } ) ) )
27 26 eqrdv
 |-  ( ph -> U = U_ x e. U ( N ` { x } ) )