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	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lcvp.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lcvp.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lcvp.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lcvp.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lcvp.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lcvp.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lcvp.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	lcvp	⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑄 ) = { 0 } ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcvp.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lcvp.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
3		lcvp.o	⊢ 0 = ( 0g ‘ 𝑊 )
4		lcvp.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		lcvp.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
6		lcvp.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
7		lcvp.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8		lcvp.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	6 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11	1 4 10 8	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
12	1	lssincl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆 ) → ( 𝑈 ∩ 𝑄 ) ∈ 𝑆 )
13	10 7 11 12	syl3anc	⊢ ( 𝜑 → ( 𝑈 ∩ 𝑄 ) ∈ 𝑆 )
14	3 1 4 5 6 13 8	lsatcveq0	⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑄 ) 𝐶 𝑄 ↔ ( 𝑈 ∩ 𝑄 ) = { 0 } ) )
15	1 2 5 10 7 11	lcvexch	⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑄 ) 𝐶 𝑄 ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )
16	14 15	bitr3d	⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑄 ) = { 0 } ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )