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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
l1cvpat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
l1cvpat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
l1cvpat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
l1cvpat.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
l1cvpat.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
l1cvpat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
l1cvpat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
l1cvpat.l ⊢ ( 𝜑 → 𝑈 𝐶 𝑉 )
l1cvpat.m ⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
Assertion l1cvpat ( 𝜑 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 l1cvpat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 l1cvpat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 l1cvpat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 l1cvpat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 l1cvpat.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
6 l1cvpat.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 l1cvpat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8 l1cvpat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9 l1cvpat.l ⊢ ( 𝜑 → 𝑈 𝐶 𝑉 )
10 l1cvpat.m ⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
11 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
12 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
13 1 11 12 4 islsat ⊢ ( 𝑊 ∈ LVec → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
14 6 13 syl ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
15 8 14 mpbid ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
16 eldifi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) → 𝑣 ∈ 𝑉 )
17 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
18 6 17 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
19 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑊 ∈ LMod )
20 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑈 ∈ 𝑆 )
21 simp2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑣 ∈ 𝑉 )
22 1 2 11 19 20 21 lspsnel5 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( 𝑣 ∈ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 ) )
23 22 notbid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ¬ 𝑣 ∈ 𝑈 ↔ ¬ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 ) )
24 eqid ⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
25 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑊 ∈ LVec )
26 1 2 24 5 6 islshpcv ⊢ ( 𝜑 → ( 𝑈 ∈ ( LSHyp ‘ 𝑊 ) ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) )
27 7 9 26 mpbir2and ⊢ ( 𝜑 → 𝑈 ∈ ( LSHyp ‘ 𝑊 ) )
28 27 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑈 ∈ ( LSHyp ‘ 𝑊 ) )
29 1 11 3 24 25 28 21 lshpnelb ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ¬ 𝑣 ∈ 𝑈 ↔ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
30 29 biimpd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ¬ 𝑣 ∈ 𝑈 → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
31 23 30 sylbird ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ¬ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
32 sseq1 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑄 ⊆ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 ) )
33 32 notbid ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ¬ 𝑄 ⊆ 𝑈 ↔ ¬ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 ) )
34 oveq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑈 ⊕ 𝑄 ) = ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
35 34 eqeq1d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( 𝑈 ⊕ 𝑄 ) = 𝑉 ↔ ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
36 33 35 imbi12d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( ¬ 𝑄 ⊆ 𝑈 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 ) ↔ ( ¬ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
37 36 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ( ¬ 𝑄 ⊆ 𝑈 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 ) ↔ ( ¬ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ⊆ 𝑈 → ( 𝑈 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
38 31 37 mpbird ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ¬ 𝑄 ⊆ 𝑈 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 ) )
39 38 3exp ⊢ ( 𝜑 → ( 𝑣 ∈ 𝑉 → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ¬ 𝑄 ⊆ 𝑈 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 ) ) ) )
40 16 39 syl5 ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ¬ 𝑄 ⊆ 𝑈 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 ) ) ) )
41 40 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑊 ) } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ¬ 𝑄 ⊆ 𝑈 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 ) ) )
42 15 10 41 mp2d ⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 )