Metamath Proof Explorer


Theorem atcveq0

Description: A Hilbert lattice element covered by an atom must be the zero subspace. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcveq0 ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 𝐵𝐴 = 0 ) )

Proof

Step Hyp Ref Expression
1 atelch ( 𝐵 ∈ HAtoms → 𝐵C )
2 cvpss ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵𝐴𝐵 ) )
3 1 2 sylan2 ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 𝐵𝐴𝐵 ) )
4 ch0le ( 𝐴C → 0𝐴 )
5 4 adantr ( ( 𝐴C𝐵 ∈ HAtoms ) → 0𝐴 )
6 3 5 jctild ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 𝐵 → ( 0𝐴𝐴𝐵 ) ) )
7 atcv0 ( 𝐵 ∈ HAtoms → 0 𝐵 )
8 7 adantr ( ( 𝐵 ∈ HAtoms ∧ 𝐴C ) → 0 𝐵 )
9 h0elch 0C
10 cvnbtwn3 ( ( 0C𝐵C𝐴C ) → ( 0 𝐵 → ( ( 0𝐴𝐴𝐵 ) → 𝐴 = 0 ) ) )
11 9 10 mp3an1 ( ( 𝐵C𝐴C ) → ( 0 𝐵 → ( ( 0𝐴𝐴𝐵 ) → 𝐴 = 0 ) ) )
12 1 11 sylan ( ( 𝐵 ∈ HAtoms ∧ 𝐴C ) → ( 0 𝐵 → ( ( 0𝐴𝐴𝐵 ) → 𝐴 = 0 ) ) )
13 8 12 mpd ( ( 𝐵 ∈ HAtoms ∧ 𝐴C ) → ( ( 0𝐴𝐴𝐵 ) → 𝐴 = 0 ) )
14 13 ancoms ( ( 𝐴C𝐵 ∈ HAtoms ) → ( ( 0𝐴𝐴𝐵 ) → 𝐴 = 0 ) )
15 6 14 syld ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 𝐵𝐴 = 0 ) )
16 breq1 ( 𝐴 = 0 → ( 𝐴 𝐵 ↔ 0 𝐵 ) )
17 7 16 syl5ibrcom ( 𝐵 ∈ HAtoms → ( 𝐴 = 0𝐴 𝐵 ) )
18 17 adantl ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 = 0𝐴 𝐵 ) )
19 15 18 impbid ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 𝐵𝐴 = 0 ) )