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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑈 ⊕ 𝑄 ) ↔ 𝑈 𝐶 ( 𝑈 ⊕ 𝑄 ) ) )