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

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 ⊢ 0ℋ ∈ Cℋ
10 cvnbtwn3 ⊢ ( ( 0ℋ ∈ Cℋ ∧ 𝐵 ∈ 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ℋ ) )