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

Metamath Proof Explorer

Theorem cvati

Description: If a Hilbert lattice element covers another, it equals the other joined with some atom. This is a consequence of the relative atomicity of Hilbert space. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 ⊢ 𝐴 ∈ Cℋ
chpssat.2 ⊢ 𝐵 ∈ Cℋ
Assertion cvati ( 𝐴 ⋖ℋ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ 𝐴 ∈ Cℋ
2 chpssat.2 ⊢ 𝐵 ∈ Cℋ
3 cvpss ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵 ) )
4 1 2 3 mp2an ⊢ ( 𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵 )
5 1 2 chrelati ⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
6 4 5 syl ⊢ ( 𝐴 ⋖ℋ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
7 cvnbtwn2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) ) )
8 1 2 7 mp3an12 ⊢ ( ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) ) )
9 atelch ⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
10 chjcl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ )
11 1 9 10 sylancr ⊢ ( 𝑥 ∈ HAtoms → ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ )
12 8 11 syl11 ⊢ ( 𝐴 ⋖ℋ 𝐵 → ( 𝑥 ∈ HAtoms → ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) ) )
13 12 reximdvai ⊢ ( 𝐴 ⋖ℋ 𝐵 → ( ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) )
14 6 13 mpd ⊢ ( 𝐴 ⋖ℋ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 )