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	syl5bi	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) → ( ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 ) )
35	34	con3dimp	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ ¬ 𝑉 ⊆ 𝑈 ) → ¬ ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
36		dfrex2	⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) ↔ ¬ ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
37	35 36	sylibr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ ¬ 𝑉 ⊆ 𝑈 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )
38	4 37	sylan2	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆 ) ∧ 𝑈 ⊊ 𝑉 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈 ) )

Metamath Proof Explorer

Theorem lssat

Proof