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ℋ ) )