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

Metamath Proof Explorer

Theorem lssats

Description: The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of MaedaMaeda p. 70. Hypothesis ( shatomistici analog.) (Contributed by NM, 9-Apr-2014)

Ref Expression
Hypotheses lssats.s 
|- S = ( LSubSp ` W )
lssats.n 
|- N = ( LSpan ` W )
lssats.a 
|- A = ( LSAtoms ` W )
Assertion lssats 
|- ( ( W e. LMod /\ U e. S ) -> U = ( N ` U. { x e. A | x C_ U } ) )

Proof

Step Hyp Ref Expression
1 lssats.s 
 |-  S = ( LSubSp ` W )
2 lssats.n 
 |-  N = ( LSpan ` W )
3 lssats.a 
 |-  A = ( LSAtoms ` W )
4 eleq1 
 |-  ( y = ( 0g ` W ) -> ( y e. ( N ` U. { x e. A | x C_ U } ) <-> ( 0g ` W ) e. ( N ` U. { x e. A | x C_ U } ) ) )
5 simplll 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> W e. LMod )
6 simpllr 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> U e. S )
7 simplr 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. U )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 8 1 lssel 
 |-  ( ( U e. S /\ y e. U ) -> y e. ( Base ` W ) )
10 6 7 9 syl2anc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. ( Base ` W ) )
11 8 1 2 lspsncl 
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) ) -> ( N ` { y } ) e. S )
12 5 10 11 syl2anc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. S )
13 1 2 lspid 
 |-  ( ( W e. LMod /\ ( N ` { y } ) e. S ) -> ( N ` ( N ` { y } ) ) = ( N ` { y } ) )
14 5 12 13 syl2anc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` ( N ` { y } ) ) = ( N ` { y } ) )
15 1 3 lsatlss 
 |-  ( W e. LMod -> A C_ S )
16 15 adantr 
 |-  ( ( W e. LMod /\ U e. S ) -> A C_ S )
17 rabss2 
 |-  ( A C_ S -> { x e. A | x C_ U } C_ { x e. S | x C_ U } )
18 uniss 
 |-  ( { x e. A | x C_ U } C_ { x e. S | x C_ U } -> U. { x e. A | x C_ U } C_ U. { x e. S | x C_ U } )
19 16 17 18 3syl 
 |-  ( ( W e. LMod /\ U e. S ) -> U. { x e. A | x C_ U } C_ U. { x e. S | x C_ U } )
20 unimax 
 |-  ( U e. S -> U. { x e. S | x C_ U } = U )
21 8 1 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
22 20 21 eqsstrd 
 |-  ( U e. S -> U. { x e. S | x C_ U } C_ ( Base ` W ) )
23 22 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> U. { x e. S | x C_ U } C_ ( Base ` W ) )
24 19 23 sstrd 
 |-  ( ( W e. LMod /\ U e. S ) -> U. { x e. A | x C_ U } C_ ( Base ` W ) )
25 24 ad2antrr 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> U. { x e. A | x C_ U } C_ ( Base ` W ) )
26 simpr 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y =/= ( 0g ` W ) )
27 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
28 8 2 27 3 lsatlspsn2 
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. A )
29 5 10 26 28 syl3anc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. A )
30 1 2 5 6 7 ellspsn5 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) C_ U )
31 sseq1 
 |-  ( x = ( N ` { y } ) -> ( x C_ U <-> ( N ` { y } ) C_ U ) )
32 31 elrab 
 |-  ( ( N ` { y } ) e. { x e. A | x C_ U } <-> ( ( N ` { y } ) e. A /\ ( N ` { y } ) C_ U ) )
33 29 30 32 sylanbrc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. { x e. A | x C_ U } )
34 elssuni 
 |-  ( ( N ` { y } ) e. { x e. A | x C_ U } -> ( N ` { y } ) C_ U. { x e. A | x C_ U } )
35 33 34 syl 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) C_ U. { x e. A | x C_ U } )
36 8 2 lspss 
 |-  ( ( W e. LMod /\ U. { x e. A | x C_ U } C_ ( Base ` W ) /\ ( N ` { y } ) C_ U. { x e. A | x C_ U } ) -> ( N ` ( N ` { y } ) ) C_ ( N ` U. { x e. A | x C_ U } ) )
37 5 25 35 36 syl3anc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` ( N ` { y } ) ) C_ ( N ` U. { x e. A | x C_ U } ) )
38 14 37 eqsstrrd 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) C_ ( N ` U. { x e. A | x C_ U } ) )
39 8 2 lspsnid 
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) ) -> y e. ( N ` { y } ) )
40 5 10 39 syl2anc 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. ( N ` { y } ) )
41 38 40 sseldd 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. ( N ` U. { x e. A | x C_ U } ) )
42 simpll 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> W e. LMod )
43 8 1 2 lspcl 
 |-  ( ( W e. LMod /\ U. { x e. A | x C_ U } C_ ( Base ` W ) ) -> ( N ` U. { x e. A | x C_ U } ) e. S )
44 24 43 syldan 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. A | x C_ U } ) e. S )
45 44 adantr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> ( N ` U. { x e. A | x C_ U } ) e. S )
46 27 1 lss0cl 
 |-  ( ( W e. LMod /\ ( N ` U. { x e. A | x C_ U } ) e. S ) -> ( 0g ` W ) e. ( N ` U. { x e. A | x C_ U } ) )
47 42 45 46 syl2anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> ( 0g ` W ) e. ( N ` U. { x e. A | x C_ U } ) )
48 4 41 47 pm2.61ne 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> y e. ( N ` U. { x e. A | x C_ U } ) )
49 48 ex 
 |-  ( ( W e. LMod /\ U e. S ) -> ( y e. U -> y e. ( N ` U. { x e. A | x C_ U } ) ) )
50 49 ssrdv 
 |-  ( ( W e. LMod /\ U e. S ) -> U C_ ( N ` U. { x e. A | x C_ U } ) )
51 simpl 
 |-  ( ( W e. LMod /\ U e. S ) -> W e. LMod )
52 8 2 lspss 
 |-  ( ( W e. LMod /\ U. { x e. S | x C_ U } C_ ( Base ` W ) /\ U. { x e. A | x C_ U } C_ U. { x e. S | x C_ U } ) -> ( N ` U. { x e. A | x C_ U } ) C_ ( N ` U. { x e. S | x C_ U } ) )
53 51 23 19 52 syl3anc 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. A | x C_ U } ) C_ ( N ` U. { x e. S | x C_ U } ) )
54 20 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> U. { x e. S | x C_ U } = U )
55 54 fveq2d 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. S | x C_ U } ) = ( N ` U ) )
56 1 2 lspid 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )
57 55 56 eqtrd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. S | x C_ U } ) = U )
58 53 57 sseqtrd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. A | x C_ U } ) C_ U )
59 50 58 eqssd 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( N ` U. { x e. A | x C_ U } ) )