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	3	adantr	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑊 ∈ LMod )
14	1 2	lsatlss	⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )
15		rabss2	⊢ ( 𝐴 ⊆ 𝑆 → { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } )
16		uniss	⊢ ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } )
17	3 14 15 16	4syl	⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } )
18		unimax	⊢ ( 𝑇 ∈ 𝑆 → ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } = 𝑇 )
19	4 18	syl	⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } = 𝑇 )
20		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
21	20 1	lssss	⊢ ( 𝑇 ∈ 𝑆 → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
22	4 21	syl	⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
23	19 22	eqsstrd	⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) )
24	17 23	sstrd	⊢ ( 𝜑 → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) )
26		uniss	⊢ ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } )
27	26	adantl	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } )
28		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
29	20 28	lspss	⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ⊆ ( Base ‘ 𝑊 ) ∧ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
30	13 25 27 29	syl3anc	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
31	1 28 2	lssats	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) )
32	3 5 31	syl2anc	⊢ ( 𝜑 → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ) )
34	1 28 2	lssats	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
35	3 4 34	syl2anc	⊢ ( 𝜑 → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) )
37	30 33 36	3sstr4d	⊢ ( ( 𝜑 ∧ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } ) → 𝑈 ⊆ 𝑇 )
38	37	ex	⊢ ( 𝜑 → ( { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈 } ⊆ { 𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇 } → 𝑈 ⊆ 𝑇 ) )
39	12 38	syl5bir	⊢ ( 𝜑 → ( ∀ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇 ) → 𝑈 ⊆ 𝑇 ) )
40	11 39	syl5bir	⊢ ( 𝜑 → ( ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) → 𝑈 ⊆ 𝑇 ) )
41	9 40	mtod	⊢ ( 𝜑 → ¬ ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
42		dfrex2	⊢ ( ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) ↔ ¬ ∀ 𝑞 ∈ 𝐴 ¬ ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
43	41 42	sylibr	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )