lspsncv0

Description: The span of a singleton covers the zero subspace, using Definition 3.2.18 of PtakPulmannova p. 68 for "covers".) (Contributed by NM, 12-Aug-2014) (Revised by AV, 13-Jul-2022)

	Ref	Expression
Hypotheses	lspsncv0.v	$⊢ V = {Base}_{W}$
	lspsncv0.z	$⊢ \underset{˙}{0} = 0_{W}$
	lspsncv0.s	$⊢ S = LSubSp (W)$
	lspsncv0.n	$⊢ N = LSpan (W)$
	lspsncv0.w	$⊢ φ \to W \in LVec$
	lspsncv0.x	$⊢ φ \to X \in V$
Assertion	lspsncv0	$⊢ φ \to \neg \exists y \in S (\{\underset{˙}{0}\} \subset y \land y \subset N (\{X\}))$

Proof

Step	Hyp	Ref	Expression
1		lspsncv0.v	$⊢ V = {Base}_{W}$
2		lspsncv0.z	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsncv0.s	$⊢ S = LSubSp (W)$
4		lspsncv0.n	$⊢ N = LSpan (W)$
5		lspsncv0.w	$⊢ φ \to W \in LVec$
6		lspsncv0.x	$⊢ φ \to X \in V$
7		df-pss	$⊢ \{\underset{˙}{0}\} \subset y \leftrightarrow (\{\underset{˙}{0}\} \subseteq y \land \{\underset{˙}{0}\} \neq y)$
8		simpr	$⊢ (\{\underset{˙}{0}\} \subseteq y \land \{\underset{˙}{0}\} \neq y) \to \{\underset{˙}{0}\} \neq y$
9		nesym	$⊢ \{\underset{˙}{0}\} \neq y \leftrightarrow \neg y = \{\underset{˙}{0}\}$
10	8 9	sylib	$⊢ (\{\underset{˙}{0}\} \subseteq y \land \{\underset{˙}{0}\} \neq y) \to \neg y = \{\underset{˙}{0}\}$
11	7 10	sylbi	$⊢ \{\underset{˙}{0}\} \subset y \to \neg y = \{\underset{˙}{0}\}$
12	5	ad2antrr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to W \in LVec$
13		simplr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to y \in S$
14	6	ad2antrr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to X \in V$
15		simpr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to y \subseteq N (\{X\})$
16	1 2 3 4	lspsnat	$⊢ ((W \in LVec \land y \in S \land X \in V) \land y \subseteq N (\{X\})) \to (y = N (\{X\}) \lor y = \{\underset{˙}{0}\})$
17	12 13 14 15 16	syl31anc	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to (y = N (\{X\}) \lor y = \{\underset{˙}{0}\})$
18	17	orcomd	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to (y = \{\underset{˙}{0}\} \lor y = N (\{X\}))$
19	18	ord	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to (\neg y = \{\underset{˙}{0}\} \to y = N (\{X\}))$
20	19	ex	$⊢ (φ \land y \in S) \to (y \subseteq N (\{X\}) \to (\neg y = \{\underset{˙}{0}\} \to y = N (\{X\})))$
21	20	com23	$⊢ (φ \land y \in S) \to (\neg y = \{\underset{˙}{0}\} \to (y \subseteq N (\{X\}) \to y = N (\{X\})))$
22		npss	$⊢ \neg y \subset N (\{X\}) \leftrightarrow (y \subseteq N (\{X\}) \to y = N (\{X\}))$
23	21 22	imbitrrdi	$⊢ (φ \land y \in S) \to (\neg y = \{\underset{˙}{0}\} \to \neg y \subset N (\{X\}))$
24	11 23	syl5	$⊢ (φ \land y \in S) \to (\{\underset{˙}{0}\} \subset y \to \neg y \subset N (\{X\}))$
25	24	ralrimiva	$⊢ φ \to \forall y \in S (\{\underset{˙}{0}\} \subset y \to \neg y \subset N (\{X\}))$
26		ralinexa	$⊢ \forall y \in S (\{\underset{˙}{0}\} \subset y \to \neg y \subset N (\{X\})) \leftrightarrow \neg \exists y \in S (\{\underset{˙}{0}\} \subset y \land y \subset N (\{X\}))$
27	25 26	sylib	$⊢ φ \to \neg \exists y \in S (\{\underset{˙}{0}\} \subset y \land y \subset N (\{X\}))$

Metamath Proof Explorer

Theorem lspsncv0

Proof