lsatcv0

Description: An atom covers the zero subspace. ( atcv0 analog.) (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	lsatcv0.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsatcv0.a	$⊢ A = LSAtoms (W)$
	lsatcv0.c	$⊢ C = ⋖_{L} (W)$
	lsatcv0.w	$⊢ φ \to W \in LVec$
	lsatcv0.q	$⊢ φ \to Q \in A$
Assertion	lsatcv0	$⊢ φ \to \{\underset{˙}{0}\} C Q$

Proof

Step	Hyp	Ref	Expression
1		lsatcv0.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsatcv0.a	$⊢ A = LSAtoms (W)$
3		lsatcv0.c	$⊢ C = ⋖_{L} (W)$
4		lsatcv0.w	$⊢ φ \to W \in LVec$
5		lsatcv0.q	$⊢ φ \to Q \in A$
6		lveclmod	$⊢ W \in LVec \to W \in LMod$
7	4 6	syl	$⊢ φ \to W \in LMod$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9	8 2 7 5	lsatlssel	$⊢ φ \to Q \in LSubSp (W)$
10	1 8	lss0ss	$⊢ (W \in LMod \land Q \in LSubSp (W)) \to \{\underset{˙}{0}\} \subseteq Q$
11	7 9 10	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq Q$
12	1 2 7 5	lsatn0	$⊢ φ \to Q \neq \{\underset{˙}{0}\}$
13	12	necomd	$⊢ φ \to \{\underset{˙}{0}\} \neq Q$
14		df-pss	$⊢ \{\underset{˙}{0}\} \subset Q \leftrightarrow (\{\underset{˙}{0}\} \subseteq Q \land \{\underset{˙}{0}\} \neq Q)$
15	11 13 14	sylanbrc	$⊢ φ \to \{\underset{˙}{0}\} \subset Q$
16		eqid	$⊢ {Base}_{W} = {Base}_{W}$
17		eqid	$⊢ LSpan (W) = LSpan (W)$
18	16 17 1 2	islsat	$⊢ W \in LMod \to (Q \in A \leftrightarrow \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{x\}))$
19	7 18	syl	$⊢ φ \to (Q \in A \leftrightarrow \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{x\}))$
20	5 19	mpbid	$⊢ φ \to \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{x\})$
21	4	adantr	$⊢ (φ \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to W \in LVec$
22		eldifi	$⊢ x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to x \in {Base}_{W}$
23	22	adantl	$⊢ (φ \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to x \in {Base}_{W}$
24	16 1 8 17 21 23	lspsncv0	$⊢ (φ \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset LSpan (W) (\{x\}))$
25	24	ex	$⊢ φ \to (x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset LSpan (W) (\{x\})))$
26		psseq2	$⊢ Q = LSpan (W) (\{x\}) \to (s \subset Q \leftrightarrow s \subset LSpan (W) (\{x\}))$
27	26	anbi2d	$⊢ Q = LSpan (W) (\{x\}) \to ((\{\underset{˙}{0}\} \subset s \land s \subset Q) \leftrightarrow (\{\underset{˙}{0}\} \subset s \land s \subset LSpan (W) (\{x\})))$
28	27	rexbidv	$⊢ Q = LSpan (W) (\{x\}) \to (\exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q) \leftrightarrow \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset LSpan (W) (\{x\})))$
29	28	notbid	$⊢ Q = LSpan (W) (\{x\}) \to (\neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q) \leftrightarrow \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset LSpan (W) (\{x\})))$
30	29	biimprcd	$⊢ \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset LSpan (W) (\{x\})) \to (Q = LSpan (W) (\{x\}) \to \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q))$
31	25 30	syl6	$⊢ φ \to (x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to (Q = LSpan (W) (\{x\}) \to \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q)))$
32	31	rexlimdv	$⊢ φ \to (\exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{x\}) \to \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q))$
33	20 32	mpd	$⊢ φ \to \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q)$
34	1 8	lsssn0	$⊢ W \in LMod \to \{\underset{˙}{0}\} \in LSubSp (W)$
35	7 34	syl	$⊢ φ \to \{\underset{˙}{0}\} \in LSubSp (W)$
36	8 3 4 35 9	lcvbr	$⊢ φ \to (\{\underset{˙}{0}\} C Q \leftrightarrow (\{\underset{˙}{0}\} \subset Q \land \neg \exists s \in LSubSp (W) (\{\underset{˙}{0}\} \subset s \land s \subset Q)))$
37	15 33 36	mpbir2and	$⊢ φ \to \{\underset{˙}{0}\} C Q$

Metamath Proof Explorer

Theorem lsatcv0

Proof