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 ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 )