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

Metamath Proof Explorer

Theorem lsatcveq0

Description: A subspace covered by an atom must be the zero subspace. ( atcveq0 analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lsatcveq0.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsatcveq0.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsatcveq0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcveq0.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lsatcveq0.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatcveq0.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lsatcveq0.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion lsatcveq0 ( 𝜑 → ( 𝑈 𝐶 𝑄 ↔ 𝑈 = { 0 } ) )

Proof

Step Hyp Ref Expression
1 lsatcveq0.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsatcveq0.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsatcveq0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lsatcveq0.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5 lsatcveq0.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lsatcveq0.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lsatcveq0.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 5 adantr ⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑊 ∈ LVec )
9 6 adantr ⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑈 ∈ 𝑆 )
10 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 5 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 2 3 11 7 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑄 ∈ 𝑆 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑈 𝐶 𝑄 )
15 2 4 8 9 13 14 lcvpss ⊢ ( ( 𝜑 ∧ 𝑈 𝐶 𝑄 ) → 𝑈 ⊊ 𝑄 )
16 15 ex ⊢ ( 𝜑 → ( 𝑈 𝐶 𝑄 → 𝑈 ⊊ 𝑄 ) )
17 1 3 4 5 7 lsatcv0 ⊢ ( 𝜑 → { 0 } 𝐶 𝑄 )
18 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑊 ∈ LVec )
19 1 2 lsssn0 ⊢ ( 𝑊 ∈ LMod → { 0 } ∈ 𝑆 )
20 11 19 syl ⊢ ( 𝜑 → { 0 } ∈ 𝑆 )
21 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → { 0 } ∈ 𝑆 )
22 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑄 ∈ 𝑆 )
23 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑈 ∈ 𝑆 )
24 simp2 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → { 0 } 𝐶 𝑄 )
25 1 2 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → { 0 } ⊆ 𝑈 )
26 11 6 25 syl2anc ⊢ ( 𝜑 → { 0 } ⊆ 𝑈 )
27 26 3ad2ant1 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → { 0 } ⊆ 𝑈 )
28 simp3 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑈 ⊊ 𝑄 )
29 2 4 18 21 22 23 24 27 28 lcvnbtwn3 ⊢ ( ( 𝜑 ∧ { 0 } 𝐶 𝑄 ∧ 𝑈 ⊊ 𝑄 ) → 𝑈 = { 0 } )
30 29 3exp ⊢ ( 𝜑 → ( { 0 } 𝐶 𝑄 → ( 𝑈 ⊊ 𝑄 → 𝑈 = { 0 } ) ) )
31 17 30 mpd ⊢ ( 𝜑 → ( 𝑈 ⊊ 𝑄 → 𝑈 = { 0 } ) )
32 16 31 syld ⊢ ( 𝜑 → ( 𝑈 𝐶 𝑄 → 𝑈 = { 0 } ) )
33 breq1 ⊢ ( 𝑈 = { 0 } → ( 𝑈 𝐶 𝑄 ↔ { 0 } 𝐶 𝑄 ) )
34 17 33 syl5ibrcom ⊢ ( 𝜑 → ( 𝑈 = { 0 } → 𝑈 𝐶 𝑄 ) )
35 32 34 impbid ⊢ ( 𝜑 → ( 𝑈 𝐶 𝑄 ↔ 𝑈 = { 0 } ) )