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 𝑆 = ( LSubSp ‘ 𝑊 )
lssats.n 𝑁 = ( LSpan ‘ 𝑊 )
lssats.a 𝐴 = ( LSAtoms ‘ 𝑊 )
Assertion lssats ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → 𝑈 = ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )

Proof

Step Hyp Ref Expression
1 lssats.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lssats.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lssats.a 𝐴 = ( LSAtoms ‘ 𝑊 )
4 eleq1 ( 𝑦 = ( 0g𝑊 ) → ( 𝑦 ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ↔ ( 0g𝑊 ) ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ) )
5 simplll ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑊 ∈ LMod )
6 simpllr ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑈𝑆 )
7 simplr ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑦𝑈 )
8 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9 8 1 lssel ( ( 𝑈𝑆𝑦𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
10 6 7 9 syl2anc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
11 8 1 2 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 )
12 5 10 11 syl2anc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 )
13 1 2 lspid ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) = ( 𝑁 ‘ { 𝑦 } ) )
14 5 12 13 syl2anc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) = ( 𝑁 ‘ { 𝑦 } ) )
15 1 3 lsatlss ( 𝑊 ∈ LMod → 𝐴𝑆 )
16 15 adantr ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → 𝐴𝑆 )
17 rabss2 ( 𝐴𝑆 → { 𝑥𝐴𝑥𝑈 } ⊆ { 𝑥𝑆𝑥𝑈 } )
18 uniss ( { 𝑥𝐴𝑥𝑈 } ⊆ { 𝑥𝑆𝑥𝑈 } → { 𝑥𝐴𝑥𝑈 } ⊆ { 𝑥𝑆𝑥𝑈 } )
19 16 17 18 3syl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → { 𝑥𝐴𝑥𝑈 } ⊆ { 𝑥𝑆𝑥𝑈 } )
20 unimax ( 𝑈𝑆 { 𝑥𝑆𝑥𝑈 } = 𝑈 )
21 8 1 lssss ( 𝑈𝑆𝑈 ⊆ ( Base ‘ 𝑊 ) )
22 20 21 eqsstrd ( 𝑈𝑆 { 𝑥𝑆𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) )
23 22 adantl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → { 𝑥𝑆𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) )
24 19 23 sstrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → { 𝑥𝐴𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) )
25 24 ad2antrr ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → { 𝑥𝐴𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) )
26 simpr ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑦 ≠ ( 0g𝑊 ) )
27 eqid ( 0g𝑊 ) = ( 0g𝑊 )
28 8 2 27 3 lsatlspsn2 ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝐴 )
29 5 10 26 28 syl3anc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝐴 )
30 1 2 5 6 7 lspsnel5a ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑈 )
31 sseq1 ( 𝑥 = ( 𝑁 ‘ { 𝑦 } ) → ( 𝑥𝑈 ↔ ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑈 ) )
32 31 elrab ( ( 𝑁 ‘ { 𝑦 } ) ∈ { 𝑥𝐴𝑥𝑈 } ↔ ( ( 𝑁 ‘ { 𝑦 } ) ∈ 𝐴 ∧ ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑈 ) )
33 29 30 32 sylanbrc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ { 𝑥𝐴𝑥𝑈 } )
34 elssuni ( ( 𝑁 ‘ { 𝑦 } ) ∈ { 𝑥𝐴𝑥𝑈 } → ( 𝑁 ‘ { 𝑦 } ) ⊆ { 𝑥𝐴𝑥𝑈 } )
35 33 34 syl ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ { 𝑥𝐴𝑥𝑈 } )
36 8 2 lspss ( ( 𝑊 ∈ LMod ∧ { 𝑥𝐴𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑦 } ) ⊆ { 𝑥𝐴𝑥𝑈 } ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) ⊆ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
37 5 25 35 36 syl3anc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) ⊆ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
38 14 37 eqsstrrd ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
39 8 2 lspsnid ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) )
40 5 10 39 syl2anc ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) )
41 38 40 sseldd ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) ∧ 𝑦 ≠ ( 0g𝑊 ) ) → 𝑦 ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
42 simpll ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) → 𝑊 ∈ LMod )
43 8 1 2 lspcl ( ( 𝑊 ∈ LMod ∧ { 𝑥𝐴𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ∈ 𝑆 )
44 24 43 syldan ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ∈ 𝑆 )
45 44 adantr ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) → ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ∈ 𝑆 )
46 27 1 lss0cl ( ( 𝑊 ∈ LMod ∧ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ∈ 𝑆 ) → ( 0g𝑊 ) ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
47 42 45 46 syl2anc ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) → ( 0g𝑊 ) ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
48 4 41 47 pm2.61ne ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) ∧ 𝑦𝑈 ) → 𝑦 ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
49 48 ex ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑦𝑈𝑦 ∈ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ) )
50 49 ssrdv ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → 𝑈 ⊆ ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )
51 simpl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → 𝑊 ∈ LMod )
52 8 2 lspss ( ( 𝑊 ∈ LMod ∧ { 𝑥𝑆𝑥𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ { 𝑥𝐴𝑥𝑈 } ⊆ { 𝑥𝑆𝑥𝑈 } ) → ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ⊆ ( 𝑁 { 𝑥𝑆𝑥𝑈 } ) )
53 51 23 19 52 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ⊆ ( 𝑁 { 𝑥𝑆𝑥𝑈 } ) )
54 20 adantl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → { 𝑥𝑆𝑥𝑈 } = 𝑈 )
55 54 fveq2d ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁 { 𝑥𝑆𝑥𝑈 } ) = ( 𝑁𝑈 ) )
56 1 2 lspid ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁𝑈 ) = 𝑈 )
57 55 56 eqtrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁 { 𝑥𝑆𝑥𝑈 } ) = 𝑈 )
58 53 57 sseqtrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) ⊆ 𝑈 )
59 50 58 eqssd ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → 𝑈 = ( 𝑁 { 𝑥𝐴𝑥𝑈 } ) )