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	1 2	lsatlss	$⊢ W \in LMod \to A \subseteq S$
11		rabss2	$⊢ A \subseteq S \to \{p \in A \| p \subseteq U\} \subseteq \{p \in S \| p \subseteq U\}$
12		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\}$
13	3 10 11 12	4syl	$⊢ φ \to ⋃ \{p \in A \| p \subseteq U\} \subseteq ⋃ \{p \in S \| p \subseteq U\}$
14		unimax	$⊢ U \in S \to ⋃ \{p \in S \| p \subseteq U\} = U$
15	5 14	syl	$⊢ φ \to ⋃ \{p \in S \| p \subseteq U\} = U$
16		eqid	$⊢ {Base}_{W} = {Base}_{W}$
17	16 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
18	5 17	syl	$⊢ φ \to U \subseteq {Base}_{W}$
19	15 18	eqsstrd	$⊢ φ \to ⋃ \{p \in S \| p \subseteq U\} \subseteq {Base}_{W}$
20	13 19	sstrd	$⊢ φ \to ⋃ \{p \in A \| p \subseteq U\} \subseteq {Base}_{W}$
21		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\}$
22		eqid	$⊢ LSpan (W) = LSpan (W)$
23	16 22	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\})$
24	3 20 21 23	syl2an3an	$⊢ (φ \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\})$
25	24	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\}))$
26	1 22 2	lssats	$⊢ (W \in LMod \land T \in S) \to T = LSpan (W) (⋃ \{p \in A \| p \subseteq T\})$
27	3 4 26	syl2anc	$⊢ φ \to T = LSpan (W) (⋃ \{p \in A \| p \subseteq T\})$
28	1 22 2	lssats	$⊢ (W \in LMod \land U \in S) \to U = LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
29	3 5 28	syl2anc	$⊢ φ \to U = LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
30	27 29	sseq12d	$⊢ φ \to (T \subseteq U \leftrightarrow LSpan (W) (⋃ \{p \in A \| p \subseteq T\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\}))$
31	25 30	sylibrd	$⊢ φ \to (\{p \in A \| p \subseteq T\} \subseteq \{p \in A \| p \subseteq U\} \to T \subseteq U)$
32	9 31	biimtrrid	$⊢ φ \to (\forall p \in A (p \subseteq T \to p \subseteq U) \to T \subseteq U)$
33	8 32	impbid2	$⊢ φ \to (T \subseteq U \leftrightarrow \forall p \in A (p \subseteq T \to p \subseteq U))$

Metamath Proof Explorer

Theorem lssatle

Proof