This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )