Theorem lcv2

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

	Ref	Expression
Hypotheses	lcv2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lcv2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lcv2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lcv2.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lcv2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lcv2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lcv2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	lcv2	⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcv2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lcv2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
3		lcv2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lcv2.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5		lcv2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lcv2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		lcv2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9	5 8	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
10	1	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
11	9 10	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
12	11 6	sseldd	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
13	1 3 9 7	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
14	11 13	sseldd	⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
15	2 12 14	lssnle	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) ) )
16	1 2 3 4 5 6 7	lcv1	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )
17	15 16	bitr3d	⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )