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	$⊢ S = LSubSp (W)$
	lssatle.a	$⊢ A = LSAtoms (W)$
	lssatle.w	$⊢ φ \to W \in LMod$
	lssatle.t	$⊢ φ \to T \in S$
	lssatle.u	$⊢ φ \to U \in S$
Assertion	lssatle	$⊢ φ \to (T \subseteq U \leftrightarrow \forall p \in A (p \subseteq T \to p \subseteq U))$

Proof

Step	Hyp	Ref	Expression
1		lssatle.s	$⊢ S = LSubSp (W)$
2		lssatle.a	$⊢ A = LSAtoms (W)$
3		lssatle.w	$⊢ φ \to W \in LMod$
4		lssatle.t	$⊢ φ \to T \in S$
5		lssatle.u	$⊢ φ \to U \in S$
6		sstr	$⊢ (p \subseteq T \land T \subseteq U) \to p \subseteq U$
7	6	expcom	$⊢ T \subseteq U \to (p \subseteq T \to p \subseteq U)$
8	7	ralrimivw	$⊢ T \subseteq U \to \forall p \in A (p \subseteq T \to p \subseteq U)$
9		ss2rab	$⊢ \{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\} \leftrightarrow \forall p \in A (p \subseteq T \to p \subseteq U)$
10	3	adantr	$⊢ (φ \land \{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\}) \to W \in LMod$
11	1 2	lsatlss	$⊢ W \in LMod \to A \subseteq S$
12		rabss2	$⊢ A \subseteq S \to \{p \in A \| p \subseteq U\} \subseteq \{p \in S \| p \subseteq U\}$
13		uniss	$⊢ \{p \in A \| p \subseteq U\} \subseteq \{p \in S \| p \subseteq U\} \to ⋃ \{p \in A \| p \subseteq U\} \subseteq ⋃ \{p \in S \| p \subseteq U\}$
14	3 11 12 13	4syl	$⊢ φ \to ⋃ \{p \in A \| p \subseteq U\} \subseteq ⋃ \{p \in S \| p \subseteq U\}$
15		unimax	$⊢ U \in S \to ⋃ \{p \in S \| p \subseteq U\} = U$
16	5 15	syl	$⊢ φ \to ⋃ \{p \in S \| p \subseteq U\} = U$
17		eqid	$⊢ {Base}_{W} = {Base}_{W}$
18	17 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
19	5 18	syl	$⊢ φ \to U \subseteq {Base}_{W}$
20	16 19	eqsstrd	$⊢ φ \to ⋃ \{p \in S \| p \subseteq U\} \subseteq {Base}_{W}$
21	14 20	sstrd	$⊢ φ \to ⋃ \{p \in A \| p \subseteq U\} \subseteq {Base}_{W}$
22	21	adantr	$⊢ (φ \land \{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\}) \to ⋃ \{p \in A \| p \subseteq U\} \subseteq {Base}_{W}$
23		uniss	$⊢ \{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\} \to ⋃ \{p \in A \| p \subseteq T\} \subseteq ⋃ \{p \in A \| p \subseteq U\}$
24	23	adantl	$⊢ (φ \land \{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\}) \to ⋃ \{p \in A \| p \subseteq T\} \subseteq ⋃ \{p \in A \| p \subseteq U\}$
25		eqid	$⊢ LSpan (W) = LSpan (W)$
26	17 25	lspss	$⊢ (W \in LMod \land ⋃ \{p \in A \| p \subseteq U\} \subseteq {Base}_{W} \land ⋃ \{p \in A \| p \subseteq T\} \subseteq ⋃ \{p \in A \| p \subseteq U\}) \to LSpan (W) (⋃ \{p \in A \| p \subseteq T\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
27	10 22 24 26	syl3anc	$⊢ (φ \land \{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\}) \to LSpan (W) (⋃ \{p \in A \| p \subseteq T\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
28	27	ex	$⊢ φ \to (\{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\} \to LSpan (W) (⋃ \{p \in A \| p \subseteq T\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\}))$
29	1 25 2	lssats	$⊢ (W \in LMod \land T \in S) \to T = LSpan (W) (⋃ \{p \in A \| p \subseteq T\})$
30	3 4 29	syl2anc	$⊢ φ \to T = LSpan (W) (⋃ \{p \in A \| p \subseteq T\})$
31	1 25 2	lssats	$⊢ (W \in LMod \land U \in S) \to U = LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
32	3 5 31	syl2anc	$⊢ φ \to U = LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
33	30 32	sseq12d	$⊢ φ \to (T \subseteq U \leftrightarrow LSpan (W) (⋃ \{p \in A \| p \subseteq T\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\}))$
34	28 33	sylibrd	$⊢ φ \to (\{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\} \to T \subseteq U)$
35	9 34	syl5bir	$⊢ φ \to (\forall p \in A (p \subseteq T \to p \subseteq U) \to T \subseteq U)$
36	8 35	impbid2	$⊢ φ \to (T \subseteq U \leftrightarrow \forall p \in A (p \subseteq T \to p \subseteq U))$

Metamath Proof Explorer

Theorem lssatle

Proof