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		nesym	$⊢ \{\underset{˙}{0}\} \neq y \leftrightarrow \neg y = \{\underset{˙}{0}\}$
9	8	bilani	$⊢ (\{\underset{˙}{0}\} \subseteq y \land \{\underset{˙}{0}\} \neq y) \to \neg y = \{\underset{˙}{0}\}$
10	7 9	sylbi	$⊢ \{\underset{˙}{0}\} \subset y \to \neg y = \{\underset{˙}{0}\}$
11	5	ad2antrr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to W \in LVec$
12		simplr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to y \in S$
13	6	ad2antrr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to X \in V$
14		simpr	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to y \subseteq N (\{X\})$
15	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}\})$
16	11 12 13 14 15	syl31anc	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to (y = N (\{X\}) \lor y = \{\underset{˙}{0}\})$
17	16	orcomd	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to (y = \{\underset{˙}{0}\} \lor y = N (\{X\}))$
18	17	ord	$⊢ ((φ \land y \in S) \land y \subseteq N (\{X\})) \to (\neg y = \{\underset{˙}{0}\} \to y = N (\{X\}))$
19	18	ex	$⊢ (φ \land y \in S) \to (y \subseteq N (\{X\}) \to (\neg y = \{\underset{˙}{0}\} \to y = N (\{X\})))$
20	19	com23	$⊢ (φ \land y \in S) \to (\neg y = \{\underset{˙}{0}\} \to (y \subseteq N (\{X\}) \to y = N (\{X\})))$
21		npss	$⊢ \neg y \subset N (\{X\}) \leftrightarrow (y \subseteq N (\{X\}) \to y = N (\{X\}))$
22	20 21	imbitrrdi	$⊢ (φ \land y \in S) \to (\neg y = \{\underset{˙}{0}\} \to \neg y \subset N (\{X\}))$
23	10 22	syl5	$⊢ (φ \land y \in S) \to (\{\underset{˙}{0}\} \subset y \to \neg y \subset N (\{X\}))$
24	23	ralrimiva	$⊢ φ \to \forall y \in S (\{\underset{˙}{0}\} \subset y \to \neg y \subset N (\{X\}))$
25		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\}))$
26	24 25	sylib	$⊢ φ \to \neg \exists y \in S (\{\underset{˙}{0}\} \subset y \land y \subset N (\{X\}))$

Metamath Proof Explorer

Theorem lspsncv0

Proof