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 = ( LSubSp ` W )
	lcv2.p	|- .(+) = ( LSSum ` W )
	lcv2.a	|- A = ( LSAtoms ` W )
	lcv2.c	|- C = (
	lcv2.w	|- ( ph -> W e. LVec )
	lcv2.u	|- ( ph -> U e. S )
	lcv2.q	|- ( ph -> Q e. A )
Assertion	lcv2	|- ( ph -> ( U C. ( U .(+) Q ) <-> U C ( U .(+) Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcv2.s	|- S = ( LSubSp ` W )
2		lcv2.p	|- .(+) = ( LSSum ` W )
3		lcv2.a	|- A = ( LSAtoms ` W )
4		lcv2.c	|- C = (
5		lcv2.w	|- ( ph -> W e. LVec )
6		lcv2.u	|- ( ph -> U e. S )
7		lcv2.q	|- ( ph -> Q e. A )
8		lveclmod	|- ( W e. LVec -> W e. LMod )
9	5 8	syl	|- ( ph -> W e. LMod )
10	1	lsssssubg	|- ( W e. LMod -> S C_ ( SubGrp ` W ) )
11	9 10	syl	|- ( ph -> S C_ ( SubGrp ` W ) )
12	11 6	sseldd	|- ( ph -> U e. ( SubGrp ` W ) )
13	1 3 9 7	lsatlssel	|- ( ph -> Q e. S )
14	11 13	sseldd	|- ( ph -> Q e. ( SubGrp ` W ) )
15	2 12 14	lssnle	|- ( ph -> ( -. Q C_ U <-> U C. ( U .(+) Q ) ) )
16	1 2 3 4 5 6 7	lcv1	|- ( ph -> ( -. Q C_ U <-> U C ( U .(+) Q ) ) )
17	15 16	bitr3d	|- ( ph -> ( U C. ( U .(+) Q ) <-> U C ( U .(+) Q ) ) )