Theorem 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{\dot{}}{0}=0_W$$
	lsatcveq0.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lsatcveq0.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatcveq0.c	$$⊢C={⋖}_L\left(W\right)$$
	lsatcveq0.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatcveq0.u	$$⊢\phi \to U\in S$$
	lsatcveq0.q	$$⊢\phi \to Q\in A$$
Assertion	lsatcveq0	$$⊢\phi \to \left(UCQ\leftrightarrow U=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

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