Metamath Proof Explorer

Theorem l1cvpat

Description: A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. ( 1cvrjat analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses l1cvpat.v ⊢ V = Base W
l1cvpat.s ⊢ S = LSubSp ⁡ W
l1cvpat.p ⊢ ⊕ ˙ = LSSum ⁡ W
l1cvpat.a ⊢ A = LSAtoms ⁡ W
l1cvpat.c ⊢ C = ⋖ L ⁡ W
l1cvpat.w ⊢ φ → W ∈ LVec
l1cvpat.u ⊢ φ → U ∈ S
l1cvpat.q ⊢ φ → Q ∈ A
l1cvpat.l ⊢ φ → U C V
l1cvpat.m ⊢ φ → ¬ Q ⊆ U
Assertion l1cvpat ⊢ φ → U ⊕ ˙ Q = V

Proof

Step Hyp Ref Expression
1 l1cvpat.v ⊢ V = Base W
2 l1cvpat.s ⊢ S = LSubSp ⁡ W
3 l1cvpat.p ⊢ ⊕ ˙ = LSSum ⁡ W
4 l1cvpat.a ⊢ A = LSAtoms ⁡ W
5 l1cvpat.c ⊢ C = ⋖ L ⁡ W
6 l1cvpat.w ⊢ φ → W ∈ LVec
7 l1cvpat.u ⊢ φ → U ∈ S
8 l1cvpat.q ⊢ φ → Q ∈ A
9 l1cvpat.l ⊢ φ → U C V
10 l1cvpat.m ⊢ φ → ¬ Q ⊆ U
11 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
12 eqid ⊢ 0 W = 0 W
13 1 11 12 4 islsat ⊢ W ∈ LVec → Q ∈ A ↔ ∃ v ∈ V ∖ 0 W Q = LSpan ⁡ W ⁡ v
14 6 13 syl ⊢ φ → Q ∈ A ↔ ∃ v ∈ V ∖ 0 W Q = LSpan ⁡ W ⁡ v
15 8 14 mpbid ⊢ φ → ∃ v ∈ V ∖ 0 W Q = LSpan ⁡ W ⁡ v
16 eldifi ⊢ v ∈ V ∖ 0 W → v ∈ V
17 lveclmod ⊢ W ∈ LVec → W ∈ LMod
18 6 17 syl ⊢ φ → W ∈ LMod
19 18 3ad2ant1 ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → W ∈ LMod
20 7 3ad2ant1 ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → U ∈ S
21 simp2 ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → v ∈ V
22 1 2 11 19 20 21 ellspsn5b ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → v ∈ U ↔ LSpan ⁡ W ⁡ v ⊆ U
23 22 notbid ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → ¬ v ∈ U ↔ ¬ LSpan ⁡ W ⁡ v ⊆ U
24 eqid ⊢ LSHyp ⁡ W = LSHyp ⁡ W
25 6 3ad2ant1 ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → W ∈ LVec
26 1 2 24 5 6 islshpcv ⊢ φ → U ∈ LSHyp ⁡ W ↔ U ∈ S ∧ U C V
27 7 9 26 mpbir2and ⊢ φ → U ∈ LSHyp ⁡ W
28 27 3ad2ant1 ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → U ∈ LSHyp ⁡ W
29 1 11 3 24 25 28 21 lshpnelb ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → ¬ v ∈ U ↔ U ⊕ ˙ LSpan ⁡ W ⁡ v = V
30 29 biimpd ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → ¬ v ∈ U → U ⊕ ˙ LSpan ⁡ W ⁡ v = V
31 23 30 sylbird ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → ¬ LSpan ⁡ W ⁡ v ⊆ U → U ⊕ ˙ LSpan ⁡ W ⁡ v = V
32 sseq1 ⊢ Q = LSpan ⁡ W ⁡ v → Q ⊆ U ↔ LSpan ⁡ W ⁡ v ⊆ U
33 32 notbid ⊢ Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U ↔ ¬ LSpan ⁡ W ⁡ v ⊆ U
34 oveq2 ⊢ Q = LSpan ⁡ W ⁡ v → U ⊕ ˙ Q = U ⊕ ˙ LSpan ⁡ W ⁡ v
35 34 eqeq1d ⊢ Q = LSpan ⁡ W ⁡ v → U ⊕ ˙ Q = V ↔ U ⊕ ˙ LSpan ⁡ W ⁡ v = V
36 33 35 imbi12d ⊢ Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U → U ⊕ ˙ Q = V ↔ ¬ LSpan ⁡ W ⁡ v ⊆ U → U ⊕ ˙ LSpan ⁡ W ⁡ v = V
37 36 3ad2ant3 ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U → U ⊕ ˙ Q = V ↔ ¬ LSpan ⁡ W ⁡ v ⊆ U → U ⊕ ˙ LSpan ⁡ W ⁡ v = V
38 31 37 mpbird ⊢ φ ∧ v ∈ V ∧ Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U → U ⊕ ˙ Q = V
39 38 3exp ⊢ φ → v ∈ V → Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U → U ⊕ ˙ Q = V
40 16 39 syl5 ⊢ φ → v ∈ V ∖ 0 W → Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U → U ⊕ ˙ Q = V
41 40 rexlimdv ⊢ φ → ∃ v ∈ V ∖ 0 W Q = LSpan ⁡ W ⁡ v → ¬ Q ⊆ U → U ⊕ ˙ Q = V
42 15 10 41 mp2d ⊢ φ → U ⊕ ˙ Q = V