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	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )

Metamath Proof Explorer

Theorem lpssat

Proof