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 ⊢ 𝑆 = ( 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 ellspsn5 ⊢ ( ( ( ( 𝑊 ∈ 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 ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) )