Theorem lssatle

Description: The ordering of two subspaces is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 29-Oct-2014)

	Ref	Expression
Hypotheses	lssatle.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssatle.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lssatle.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lssatle.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	lssatle.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion	lssatle	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lssatle.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lssatle.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3		lssatle.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lssatle.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5		lssatle.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		sstr	⊢ ( ( 𝑝 ⊆ 𝑇 ∧ 𝑇 ⊆ 𝑈 ) → 𝑝 ⊆ 𝑈 )
7	6	expcom	⊢ ( 𝑇 ⊆ 𝑈 → ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) )
8	7	ralrimivw	⊢ ( 𝑇 ⊆ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) )
9		ss2rab	⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) )
10	3	adantr	⊢ ( ( 𝜑 ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → 𝑊 ∈ LMod )
11	1 2	lsatlss	⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )
12		rabss2	⊢ ( 𝐴 ⊆ 𝑆 → { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
13		uniss	⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
14	3 11 12 13	4syl	⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
15		unimax	⊢ ( 𝑈 ∈ 𝑆 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } = 𝑈 )
16	5 15	syl	⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } = 𝑈 )
17		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
18	17 1	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
19	5 18	syl	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
20	16 19	eqsstrd	⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
21	14 20	sstrd	⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
23		uniss	⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } )
24	23	adantl	⊢ ( ( 𝜑 ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } )
25		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
26	17 25	lspss	⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
27	10 22 24 26	syl3anc	⊢ ( ( 𝜑 ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
28	27	ex	⊢ ( 𝜑 → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) ) )
29	1 25 2	lssats	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) )
30	3 4 29	syl2anc	⊢ ( 𝜑 → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) )
31	1 25 2	lssats	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
32	3 5 31	syl2anc	⊢ ( 𝜑 → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
33	30 32	sseq12d	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) ) )
34	28 33	sylibrd	⊢ ( 𝜑 → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → 𝑇 ⊆ 𝑈 ) )
35	9 34	syl5bir	⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) → 𝑇 ⊆ 𝑈 ) )
36	8 35	impbid2	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) ) )