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 } 𝐶 𝑄 )