Metamath Proof Explorer

Theorem lpssat

Description: Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lpssat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lpssat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lpssat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lpssat.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lpssat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lpssat.l ⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )
Assertion lpssat ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lpssat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lpssat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lpssat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lpssat.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5 lpssat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 lpssat.l ⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )
7 dfpss3 ⊢ ( 𝑇 ⊊ 𝑈 ↔ ( 𝑇 ⊆ 𝑈 ∧ ¬ 𝑈 ⊆ 𝑇 ) )
8 7 simprbi ⊢ ( 𝑇 ⊊ 𝑈 → ¬ 𝑈 ⊆ 𝑇 )
9 6 8 syl ⊢ ( 𝜑 → ¬ 𝑈 ⊆ 𝑇 )
10 iman ⊢ ( ( 𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇 ) ↔ ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
11 10 ralbii ⊢ ( ∀ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇 ) ↔ ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
12 ss2rab ⊢ ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ↔ ∀ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇 ) )
13 1 2 lsatlss ⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )
14 rabss2 ⊢ ( 𝐴 ⊆ 𝑆 → { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } )
15 uniss ⊢ ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } )
16 3 13 14 15 4syl ⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } )
17 unimax ⊢ ( 𝑇 ∈ 𝑆 → ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } = 𝑇 )
18 4 17 syl ⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } = 𝑇 )
19 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
20 19 1 lssss ⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
21 4 20 syl ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
22 18 21 eqsstrd ⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) )
23 16 22 sstrd ⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) )
24 uniss ⊢ ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } )
25 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
26 19 25 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) ∧ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
27 3 23 24 26 syl2an3an ⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
28 1 25 2 lssats ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) )
29 3 5 28 syl2anc ⊢ ( 𝜑 → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) )
31 1 25 2 lssats ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
32 3 4 31 syl2anc ⊢ ( 𝜑 → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
34 27 30 33 3sstr4d ⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑈 ⊆ 𝑇 )
35 34 ex ⊢ ( 𝜑 → ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } → 𝑈 ⊆ 𝑇 ) )
36 12 35 biimtrrid ⊢ ( 𝜑 → ( ∀ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇 ) → 𝑈 ⊆ 𝑇 ) )
37 11 36 biimtrrid ⊢ ( 𝜑 → ( ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) → 𝑈 ⊆ 𝑇 ) )
38 9 37 mtod ⊢ ( 𝜑 → ¬ ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
39 dfrex2 ⊢ ( ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) ↔ ¬ ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
40 38 39 sylibr ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )