lsat0cv

Description: A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015)

	Ref	Expression
Hypotheses	lsat0cv.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsat0cv.s	$⊢ S = LSubSp (W)$
	lsat0cv.a	$⊢ A = LSAtoms (W)$
	lsat0cv.c	$⊢ C = ⋖_{L} (W)$
	lsat0cv.w	$⊢ φ \to W \in LVec$
	lsat0cv.u	$⊢ φ \to U \in S$
Assertion	lsat0cv	$⊢ φ \to (U \in A \leftrightarrow \{\underset{˙}{0}\} C U)$

Proof

Step	Hyp	Ref	Expression
1		lsat0cv.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsat0cv.s	$⊢ S = LSubSp (W)$
3		lsat0cv.a	$⊢ A = LSAtoms (W)$
4		lsat0cv.c	$⊢ C = ⋖_{L} (W)$
5		lsat0cv.w	$⊢ φ \to W \in LVec$
6		lsat0cv.u	$⊢ φ \to U \in S$
7	5	adantr	$⊢ (φ \land U \in A) \to W \in LVec$
8		simpr	$⊢ (φ \land U \in A) \to U \in A$
9	1 3 4 7 8	lsatcv0	$⊢ (φ \land U \in A) \to \{\underset{˙}{0}\} C U$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	5 10	syl	$⊢ φ \to W \in LMod$
12	11	adantr	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to W \in LMod$
13	1 2	lsssn0	$⊢ W \in LMod \to \{\underset{˙}{0}\} \in S$
14	11 13	syl	$⊢ φ \to \{\underset{˙}{0}\} \in S$
15	14	adantr	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to \{\underset{˙}{0}\} \in S$
16	6	adantr	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to U \in S$
17		simpr	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to \{\underset{˙}{0}\} C U$
18	2 4 12 15 16 17	lcvpss	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to \{\underset{˙}{0}\} \subset U$
19		pssnel	$⊢ \{\underset{˙}{0}\} \subset U \to \exists x (x \in U \land \neg x \in \{\underset{˙}{0}\})$
20	18 19	syl	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to \exists x (x \in U \land \neg x \in \{\underset{˙}{0}\})$
21	6	ad2antrr	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land (x \in U \land \neg x \in \{\underset{˙}{0}\})) \to U \in S$
22		simprl	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land (x \in U \land \neg x \in \{\underset{˙}{0}\})) \to x \in U$
23		eqid	$⊢ {Base}_{W} = {Base}_{W}$
24	23 2	lssel	$⊢ (U \in S \land x \in U) \to x \in {Base}_{W}$
25	21 22 24	syl2anc	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land (x \in U \land \neg x \in \{\underset{˙}{0}\})) \to x \in {Base}_{W}$
26		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
27	26	biimpri	$⊢ x = \underset{˙}{0} \to x \in \{\underset{˙}{0}\}$
28	27	necon3bi	$⊢ \neg x \in \{\underset{˙}{0}\} \to x \neq \underset{˙}{0}$
29	28	adantl	$⊢ (x \in U \land \neg x \in \{\underset{˙}{0}\}) \to x \neq \underset{˙}{0}$
30	29	adantl	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land (x \in U \land \neg x \in \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
31		eldifsn	$⊢ x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in {Base}_{W} \land x \neq \underset{˙}{0})$
32	25 30 31	sylanbrc	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land (x \in U \land \neg x \in \{\underset{˙}{0}\})) \to x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})$
33	32 22	jca	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land (x \in U \land \neg x \in \{\underset{˙}{0}\})) \to (x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land x \in U)$
34	33	ex	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to ((x \in U \land \neg x \in \{\underset{˙}{0}\}) \to (x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land x \in U))$
35	34	eximdv	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to (\exists x (x \in U \land \neg x \in \{\underset{˙}{0}\}) \to \exists x (x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land x \in U))$
36		df-rex	$⊢ \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) x \in U \leftrightarrow \exists x (x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land x \in U)$
37	35 36	imbitrrdi	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to (\exists x (x \in U \land \neg x \in \{\underset{˙}{0}\}) \to \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) x \in U)$
38	20 37	mpd	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) x \in U$
39		simpllr	$⊢ (((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \to \{\underset{˙}{0}\} C U$
40	2 4 5 14 6	lcvbr2	$⊢ φ \to (\{\underset{˙}{0}\} C U \leftrightarrow (\{\underset{˙}{0}\} \subset U \land \forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U)))$
41	40	adantr	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to (\{\underset{˙}{0}\} C U \leftrightarrow (\{\underset{˙}{0}\} \subset U \land \forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U)))$
42	41	ad2antrr	$⊢ (((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \to (\{\underset{˙}{0}\} C U \leftrightarrow (\{\underset{˙}{0}\} \subset U \land \forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U)))$
43	11	ad2antrr	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to W \in LMod$
44	43	ad2antrr	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to W \in LMod$
45		eldifi	$⊢ x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to x \in {Base}_{W}$
46	45	adantl	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to x \in {Base}_{W}$
47	46	ad2antrr	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to x \in {Base}_{W}$
48		eqid	$⊢ LSpan (W) = LSpan (W)$
49	23 2 48	lspsncl	$⊢ (W \in LMod \land x \in {Base}_{W}) \to LSpan (W) (\{x\}) \in S$
50	44 47 49	syl2anc	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to LSpan (W) (\{x\}) \in S$
51	1 2	lss0ss	$⊢ (W \in LMod \land LSpan (W) (\{x\}) \in S) \to \{\underset{˙}{0}\} \subseteq LSpan (W) (\{x\})$
52	44 50 51	syl2anc	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to \{\underset{˙}{0}\} \subseteq LSpan (W) (\{x\})$
53		eldifsni	$⊢ x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to x \neq \underset{˙}{0}$
54	53	adantl	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
55	54	ad2antrr	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to x \neq \underset{˙}{0}$
56	23 1 48	lspsneq0	$⊢ (W \in LMod \land x \in {Base}_{W}) \to (LSpan (W) (\{x\}) = \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0})$
57	44 47 56	syl2anc	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to (LSpan (W) (\{x\}) = \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0})$
58	57	necon3bid	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to (LSpan (W) (\{x\}) \neq \{\underset{˙}{0}\} \leftrightarrow x \neq \underset{˙}{0})$
59	55 58	mpbird	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to LSpan (W) (\{x\}) \neq \{\underset{˙}{0}\}$
60	59	necomd	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to \{\underset{˙}{0}\} \neq LSpan (W) (\{x\})$
61		df-pss	$⊢ \{\underset{˙}{0}\} \subset LSpan (W) (\{x\}) \leftrightarrow (\{\underset{˙}{0}\} \subseteq LSpan (W) (\{x\}) \land \{\underset{˙}{0}\} \neq LSpan (W) (\{x\}))$
62	52 60 61	sylanbrc	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to \{\underset{˙}{0}\} \subset LSpan (W) (\{x\})$
63	6	ad2antrr	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to U \in S$
64	63	ad2antrr	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to U \in S$
65		simplr	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to x \in U$
66	2 48 44 64 65	ellspsn5	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to LSpan (W) (\{x\}) \subseteq U$
67	62 66	jca	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to (\{\underset{˙}{0}\} \subset LSpan (W) (\{x\}) \land LSpan (W) (\{x\}) \subseteq U)$
68		psseq2	$⊢ s = LSpan (W) (\{x\}) \to (\{\underset{˙}{0}\} \subset s \leftrightarrow \{\underset{˙}{0}\} \subset LSpan (W) (\{x\}))$
69		sseq1	$⊢ s = LSpan (W) (\{x\}) \to (s \subseteq U \leftrightarrow LSpan (W) (\{x\}) \subseteq U)$
70	68 69	anbi12d	$⊢ s = LSpan (W) (\{x\}) \to ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \leftrightarrow (\{\underset{˙}{0}\} \subset LSpan (W) (\{x\}) \land LSpan (W) (\{x\}) \subseteq U))$
71		eqeq1	$⊢ s = LSpan (W) (\{x\}) \to (s = U \leftrightarrow LSpan (W) (\{x\}) = U)$
72	70 71	imbi12d	$⊢ s = LSpan (W) (\{x\}) \to (((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U) \leftrightarrow ((\{\underset{˙}{0}\} \subset LSpan (W) (\{x\}) \land LSpan (W) (\{x\}) \subseteq U) \to LSpan (W) (\{x\}) = U))$
73	72	rspcv	$⊢ LSpan (W) (\{x\}) \in S \to (\forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U) \to ((\{\underset{˙}{0}\} \subset LSpan (W) (\{x\}) \land LSpan (W) (\{x\}) \subseteq U) \to LSpan (W) (\{x\}) = U))$
74	50 73	syl	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to (\forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U) \to ((\{\underset{˙}{0}\} \subset LSpan (W) (\{x\}) \land LSpan (W) (\{x\}) \subseteq U) \to LSpan (W) (\{x\}) = U))$
75	67 74	mpid	$⊢ ((((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \land \{\underset{˙}{0}\} \subset U) \to (\forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U) \to LSpan (W) (\{x\}) = U)$
76	75	expimpd	$⊢ (((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \to ((\{\underset{˙}{0}\} \subset U \land \forall s \in S ((\{\underset{˙}{0}\} \subset s \land s \subseteq U) \to s = U)) \to LSpan (W) (\{x\}) = U)$
77	42 76	sylbid	$⊢ (((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \to (\{\underset{˙}{0}\} C U \to LSpan (W) (\{x\}) = U)$
78	39 77	mpd	$⊢ (((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \to LSpan (W) (\{x\}) = U$
79	78	eqcomd	$⊢ (((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land x \in U) \to U = LSpan (W) (\{x\})$
80	79	ex	$⊢ ((φ \land \{\underset{˙}{0}\} C U) \land x \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to (x \in U \to U = LSpan (W) (\{x\}))$
81	80	reximdva	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to (\exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) x \in U \to \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) U = LSpan (W) (\{x\}))$
82	38 81	mpd	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) U = LSpan (W) (\{x\})$
83	5	adantr	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to W \in LVec$
84	23 48 1 3	islsat	$⊢ W \in LVec \to (U \in A \leftrightarrow \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) U = LSpan (W) (\{x\}))$
85	83 84	syl	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to (U \in A \leftrightarrow \exists x \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) U = LSpan (W) (\{x\}))$
86	82 85	mpbird	$⊢ (φ \land \{\underset{˙}{0}\} C U) \to U \in A$
87	9 86	impbida	$⊢ φ \to (U \in A \leftrightarrow \{\underset{˙}{0}\} C U)$

Metamath Proof Explorer

Theorem lsat0cv

Proof