Theorem lcv2

Description: Covering property of a subspace plus an atom. ( chcv2 analog.) (Contributed by NM, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcv2.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lcv2.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lcv2.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
4		lcv2.c	$$⊢C={⋖}_L\left(W\right)$$
5		lcv2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lcv2.u	$$⊢\phi \to U\in S$$
7		lcv2.q	$$⊢\phi \to Q\in A$$
8		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
9	5 8	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
10	1	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
11	9 10	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
12	11 6	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
13	1 3 9 7	lsatlssel	$$⊢\phi \to Q\in S$$
14	11 13	sseldd	$$⊢\phi \to Q\in \mathrm{SubGrp}\left(W\right)$$
15	2 12 14	lssnle	$$⊢\phi \to \left(\neg Q\subseteq U\leftrightarrow U\subset U\underset{\dot{}}{\oplus }Q\right)$$
16	1 2 3 4 5 6 7	lcv1	$$⊢\phi \to \left(\neg Q\subseteq U\leftrightarrow UC\left(U\underset{\dot{}}{\oplus }Q\right)\right)$$
17	15 16	bitr3d	$$⊢\phi \to \left(U\subset U\underset{\dot{}}{\oplus }Q\leftrightarrow UC\left(U\underset{\dot{}}{\oplus }Q\right)\right)$$