lsatcveq0

Description: A subspace covered by an atom must be the zero subspace. ( atcveq0 analog.) (Contributed by NM, 7-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatcveq0.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsatcveq0.s	$⊢ S = LSubSp (W)$
3		lsatcveq0.a	$⊢ A = LSAtoms (W)$
4		lsatcveq0.c	$⊢ C = ⋖_{L} (W)$
5		lsatcveq0.w	$⊢ φ \to W \in LVec$
6		lsatcveq0.u	$⊢ φ \to U \in S$
7		lsatcveq0.q	$⊢ φ \to Q \in A$
8	5	adantr	$⊢ (φ \land U C Q) \to W \in LVec$
9	6	adantr	$⊢ (φ \land U C Q) \to U \in S$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	5 10	syl	$⊢ φ \to W \in LMod$
12	2 3 11 7	lsatlssel	$⊢ φ \to Q \in S$
13	12	adantr	$⊢ (φ \land U C Q) \to Q \in S$
14		simpr	$⊢ (φ \land U C Q) \to U C Q$
15	2 4 8 9 13 14	lcvpss	$⊢ (φ \land U C Q) \to U \subset Q$
16	15	ex	$⊢ φ \to (U C Q \to U \subset Q)$
17	1 3 4 5 7	lsatcv0	$⊢ φ \to \{\underset{˙}{0}\} C Q$
18	5	3ad2ant1	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to W \in LVec$
19	1 2	lsssn0	$⊢ W \in LMod \to \{\underset{˙}{0}\} \in S$
20	11 19	syl	$⊢ φ \to \{\underset{˙}{0}\} \in S$
21	20	3ad2ant1	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to \{\underset{˙}{0}\} \in S$
22	12	3ad2ant1	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to Q \in S$
23	6	3ad2ant1	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to U \in S$
24		simp2	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to \{\underset{˙}{0}\} C Q$
25	1 2	lss0ss	$⊢ (W \in LMod \land U \in S) \to \{\underset{˙}{0}\} \subseteq U$
26	11 6 25	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq U$
27	26	3ad2ant1	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to \{\underset{˙}{0}\} \subseteq U$
28		simp3	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to U \subset Q$
29	2 4 18 21 22 23 24 27 28	lcvnbtwn3	$⊢ (φ \land \{\underset{˙}{0}\} C Q \land U \subset Q) \to U = \{\underset{˙}{0}\}$
30	29	3exp	$⊢ φ \to (\{\underset{˙}{0}\} C Q \to (U \subset Q \to U = \{\underset{˙}{0}\}))$
31	17 30	mpd	$⊢ φ \to (U \subset Q \to U = \{\underset{˙}{0}\})$
32	16 31	syld	$⊢ φ \to (U C Q \to U = \{\underset{˙}{0}\})$
33		breq1	$⊢ U = \{\underset{˙}{0}\} \to (U C Q \leftrightarrow \{\underset{˙}{0}\} C Q)$
34	17 33	syl5ibrcom	$⊢ φ \to (U = \{\underset{˙}{0}\} \to U C Q)$
35	32 34	impbid	$⊢ φ \to (U C Q \leftrightarrow U = \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lsatcveq0

Proof