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

Metamath Proof Explorer

Theorem lsatcv0

Description: An atom covers the zero subspace. ( atcv0 analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lsatcv0.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsatcv0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcv0.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lsatcv0.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatcv0.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion lsatcv0 ( 𝜑 → { 0 } 𝐶 𝑄 )

Proof

Step Hyp Ref Expression
1 lsatcv0.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsatcv0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsatcv0.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
4 lsatcv0.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lsatcv0.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
6 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
7 4 6 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 8 2 7 5 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
10 1 8 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ 𝑄 )
11 7 9 10 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ 𝑄 )
12 1 2 7 5 lsatn0 ⊢ ( 𝜑 → 𝑄 ≠ { 0 } )
13 12 necomd ⊢ ( 𝜑 → { 0 } ≠ 𝑄 )
14 df-pss ⊢ ( { 0 } ⊊ 𝑄 ↔ ( { 0 } ⊆ 𝑄 ∧ { 0 } ≠ 𝑄 ) )
15 11 13 14 sylanbrc ⊢ ( 𝜑 → { 0 } ⊊ 𝑄 )
16 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
17 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
18 16 17 1 2 islsat ⊢ ( 𝑊 ∈ LMod → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
19 7 18 syl ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
20 5 19 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑊 ∈ LVec )
22 eldifi ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
24 16 1 8 17 21 23 lspsncv0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
25 24 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
26 psseq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( 𝑠 ⊊ 𝑄 ↔ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) )
27 26 anbi2d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ↔ ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
28 27 rexbidv ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ↔ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
29 28 notbid ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ↔ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) ) )
30 29 biimprcd ⊢ ( ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) )
31 25 30 syl6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) ) )
32 31 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) )
33 20 32 mpd ⊢ ( 𝜑 → ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) )
34 1 8 lsssn0 ⊢ ( 𝑊 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
35 7 34 syl ⊢ ( 𝜑 → { 0 } ∈ ( LSubSp ‘ 𝑊 ) )
36 8 3 4 35 9 lcvbr ⊢ ( 𝜑 → ( { 0 } 𝐶 𝑄 ↔ ( { 0 } ⊊ 𝑄 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ( { 0 } ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑄 ) ) ) )
37 15 33 36 mpbir2and ⊢ ( 𝜑 → { 0 } 𝐶 𝑄 )