lssat

Description: Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 9-Apr-2014)

	Ref	Expression
Hypotheses	lssat.s	$⊢ S = LSubSp (W)$
	lssat.a	$⊢ A = LSAtoms (W)$
Assertion	lssat	$⊢ ((W \in LMod \land U \in S \land V \in S) \land U \subset V) \to \exists p \in A (p \subseteq V \land \neg p \subseteq U)$

Proof

Step	Hyp	Ref	Expression
1		lssat.s	$⊢ S = LSubSp (W)$
2		lssat.a	$⊢ A = LSAtoms (W)$
3		dfpss3	$⊢ U \subset V \leftrightarrow (U \subseteq V \land \neg V \subseteq U)$
4	3	simprbi	$⊢ U \subset V \to \neg V \subseteq U$
5		ss2rab	$⊢ \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\} \leftrightarrow \forall p \in A (p \subseteq V \to p \subseteq U)$
6		iman	$⊢ (p \subseteq V \to p \subseteq U) \leftrightarrow \neg (p \subseteq V \land \neg p \subseteq U)$
7	6	ralbii	$⊢ \forall p \in A (p \subseteq V \to p \subseteq U) \leftrightarrow \forall p \in A \neg (p \subseteq V \land \neg p \subseteq U)$
8	5 7	bitr2i	$⊢ \forall p \in A \neg (p \subseteq V \land \neg p \subseteq U) \leftrightarrow \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}$
9		simpl1	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to W \in LMod$
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	9 10 11 12	4syl	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to ⋃ \{p \in A \| p \subseteq U\} \subseteq ⋃ \{p \in S \| p \subseteq U\}$
14		simpl2	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to U \in S$
15		unimax	$⊢ U \in S \to ⋃ \{p \in S \| p \subseteq U\} = U$
16	14 15	syl	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \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	14 18	syl	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to U \subseteq {Base}_{W}$
20	16 19	eqsstrd	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to ⋃ \{p \in S \| p \subseteq U\} \subseteq {Base}_{W}$
21	13 20	sstrd	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to ⋃ \{p \in A \| p \subseteq U\} \subseteq {Base}_{W}$
22		uniss	$⊢ \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\} \to ⋃ \{p \in A \| p \subseteq V\} \subseteq ⋃ \{p \in A \| p \subseteq U\}$
23	22	adantl	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to ⋃ \{p \in A \| p \subseteq V\} \subseteq ⋃ \{p \in A \| p \subseteq U\}$
24		eqid	$⊢ LSpan (W) = LSpan (W)$
25	17 24	lspss	$⊢ (W \in LMod \land ⋃ \{p \in A \| p \subseteq U\} \subseteq {Base}_{W} \land ⋃ \{p \in A \| p \subseteq V\} \subseteq ⋃ \{p \in A \| p \subseteq U\}) \to LSpan (W) (⋃ \{p \in A \| p \subseteq V\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
26	9 21 23 25	syl3anc	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to LSpan (W) (⋃ \{p \in A \| p \subseteq V\}) \subseteq LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
27		simpl3	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to V \in S$
28	1 24 2	lssats	$⊢ (W \in LMod \land V \in S) \to V = LSpan (W) (⋃ \{p \in A \| p \subseteq V\})$
29	9 27 28	syl2anc	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to V = LSpan (W) (⋃ \{p \in A \| p \subseteq V\})$
30	1 24 2	lssats	$⊢ (W \in LMod \land U \in S) \to U = LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
31	9 14 30	syl2anc	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to U = LSpan (W) (⋃ \{p \in A \| p \subseteq U\})$
32	26 29 31	3sstr4d	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\}) \to V \subseteq U$
33	32	ex	$⊢ (W \in LMod \land U \in S \land V \in S) \to (\{p \in A \| p \subseteq V\} \subseteq \{p \in A \| p \subseteq U\} \to V \subseteq U)$
34	8 33	syl5bi	$⊢ (W \in LMod \land U \in S \land V \in S) \to (\forall p \in A \neg (p \subseteq V \land \neg p \subseteq U) \to V \subseteq U)$
35	34	con3dimp	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \neg V \subseteq U) \to \neg \forall p \in A \neg (p \subseteq V \land \neg p \subseteq U)$
36		dfrex2	$⊢ \exists p \in A (p \subseteq V \land \neg p \subseteq U) \leftrightarrow \neg \forall p \in A \neg (p \subseteq V \land \neg p \subseteq U)$
37	35 36	sylibr	$⊢ ((W \in LMod \land U \in S \land V \in S) \land \neg V \subseteq U) \to \exists p \in A (p \subseteq V \land \neg p \subseteq U)$
38	4 37	sylan2	$⊢ ((W \in LMod \land U \in S \land V \in S) \land U \subset V) \to \exists p \in A (p \subseteq V \land \neg p \subseteq U)$

Metamath Proof Explorer

Theorem lssat

Proof