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

Metamath Proof Explorer

Theorem lssat

Description: Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 9-Apr-2014)

Ref Expression
Hypotheses lssat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
Assertion lssat ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ 𝑈 ⊊ 𝑉 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lssat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lssat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 dfpss3 ⊢ ( 𝑈 ⊊ 𝑉 ↔ ( 𝑈 ⊆ 𝑉 ∧ ¬ 𝑉 ⊆ 𝑈 ) )
4 3 simprbi ⊢ ( 𝑈 ⊊ 𝑉 → ¬ 𝑉 ⊆ 𝑈 )
5 ss2rab ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 → 𝑝 ⊆ 𝑈 ) )
6 iman ⊢ ( ( 𝑝 ⊆ 𝑉 → 𝑝 ⊆ 𝑈 ) ↔ ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
7 6 ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 → 𝑝 ⊆ 𝑈 ) ↔ ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
8 5 7 bitr2i ⊢ ( ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) ↔ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } )
9 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑊 ∈ LMod )
10 1 2 lsatlss ⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )
11 rabss2 ⊢ ( 𝐴 ⊆ 𝑆 → { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
12 uniss ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
13 9 10 11 12 4syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
14 simpl2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑈 ∈ 𝑆 )
15 unimax ⊢ ( 𝑈 ∈ 𝑆 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } = 𝑈 )
16 14 15 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } = 𝑈 )
17 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
18 17 1 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
19 14 18 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
20 16 19 eqsstrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
21 13 20 sstrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
22 uniss ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } )
23 22 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } )
24 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
25 17 24 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
26 9 21 23 25 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
27 simpl3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑉 ∈ 𝑆 )
28 1 24 2 lssats ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ∈ 𝑆 ) → 𝑉 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ) )
29 9 27 28 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑉 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ) )
30 1 24 2 lssats ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
31 9 14 30 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
32 26 29 31 3sstr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑉 ⊆ 𝑈 )
33 32 ex ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑉 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → 𝑉 ⊆ 𝑈 ) )
34 8 33 biimtrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) → ( ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 ) )
35 34 con3dimp ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ ¬ 𝑉 ⊆ 𝑈 ) → ¬ ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
36 dfrex2 ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) ↔ ¬ ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
37 35 36 sylibr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ ¬ 𝑉 ⊆ 𝑈 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
38 4 37 sylan2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ 𝑈 ⊊ 𝑉 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )