Theorem lcvp

Description: Covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lcvp.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lcvp.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lcvp.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lcvp.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lcvp.c	$$⊢C={⋖}_L\left(W\right)$$
	lcvp.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lcvp.u	$$⊢\phi \to U\in S$$
	lcvp.q	$$⊢\phi \to Q\in A$$
Assertion	lcvp	$$⊢\phi \to \left(U\cap Q=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow UC\left(U\underset{\dot{}}{\oplus }Q\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcvp.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lcvp.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lcvp.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		lcvp.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		lcvp.c	$$⊢C={⋖}_L\left(W\right)$$
6		lcvp.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lcvp.u	$$⊢\phi \to U\in S$$
8		lcvp.q	$$⊢\phi \to Q\in A$$
9		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
10	6 9	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
11	1 4 10 8	lsatlssel	$$⊢\phi \to Q\in S$$
12	1	lssincl	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\wedge Q\in S\right)\to U\cap Q\in S$$
13	10 7 11 12	syl3anc	$$⊢\phi \to U\cap Q\in S$$
14	3 1 4 5 6 13 8	lsatcveq0	$$⊢\phi \to \left(\left(U\cap Q\right)CQ\leftrightarrow U\cap Q=\left\{\underset{\dot{}}{0}\right\}\right)$$
15	1 2 5 10 7 11	lcvexch	$$⊢\phi \to \left(\left(U\cap Q\right)CQ\leftrightarrow UC\left(U\underset{\dot{}}{\oplus }Q\right)\right)$$
16	14 15	bitr3d	$$⊢\phi \to \left(U\cap Q=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow UC\left(U\underset{\dot{}}{\oplus }Q\right)\right)$$