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 ⊢ S = LSubSp ⁡ W
lcv2.p ⊢ ⊕ ˙ = LSSum ⁡ W
lcv2.a ⊢ A = LSAtoms ⁡ W
lcv2.c ⊢ C = ⋖ L ⁡ W
lcv2.w ⊢ φ → W ∈ LVec
lcv2.u ⊢ φ → U ∈ S
lcv2.q ⊢ φ → Q ∈ A
Assertion lcv2 ⊢ φ → U ⊂ 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 = ⋖ L ⁡ W
5 lcv2.w ⊢ φ → W ∈ LVec
6 lcv2.u ⊢ φ → U ∈ S
7 lcv2.q ⊢ φ → Q ∈ A
8 lveclmod ⊢ W ∈ LVec → W ∈ LMod
9 5 8 syl ⊢ φ → W ∈ LMod
10 1 lsssssubg ⊢ W ∈ LMod → S ⊆ SubGrp ⁡ W
11 9 10 syl ⊢ φ → S ⊆ SubGrp ⁡ W
12 11 6 sseldd ⊢ φ → U ∈ SubGrp ⁡ W
13 1 3 9 7 lsatlssel ⊢ φ → Q ∈ S
14 11 13 sseldd ⊢ φ → Q ∈ SubGrp ⁡ W
15 2 12 14 lssnle ⊢ φ → ¬ Q ⊆ U ↔ U ⊂ U ⊕ ˙ Q
16 1 2 3 4 5 6 7 lcv1 ⊢ φ → ¬ Q ⊆ U ↔ U C U ⊕ ˙ Q
17 15 16 bitr3d ⊢ φ → U ⊂ U ⊕ ˙ Q ↔ U C U ⊕ ˙ Q