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	|- A e. CH
	chpssat.2	|- B e. CH
Assertion	cvati	|- ( A E. x e. HAtoms ( A vH x ) = B )

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	|- A e. CH
2		chpssat.2	|- B e. CH
3		cvpss	|- ( ( A e. CH /\ B e. CH ) -> ( A A C. B ) )
4	1 2 3	mp2an	|- ( A A C. B )
5	1 2	chrelati	|- ( A C. B -> E. x e. HAtoms ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) )
6	4 5	syl	|- ( A E. x e. HAtoms ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) )
7		cvnbtwn2	|- ( ( A e. CH /\ B e. CH /\ ( A vH x ) e. CH ) -> ( A ( ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) -> ( A vH x ) = B ) ) )
8	1 2 7	mp3an12	|- ( ( A vH x ) e. CH -> ( A ( ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) -> ( A vH x ) = B ) ) )
9		atelch	|- ( x e. HAtoms -> x e. CH )
10		chjcl	|- ( ( A e. CH /\ x e. CH ) -> ( A vH x ) e. CH )
11	1 9 10	sylancr	|- ( x e. HAtoms -> ( A vH x ) e. CH )
12	8 11	syl11	|- ( A ( x e. HAtoms -> ( ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) -> ( A vH x ) = B ) ) )
13	12	reximdvai	|- ( A ( E. x e. HAtoms ( A C. ( A vH x ) /\ ( A vH x ) C_ B ) -> E. x e. HAtoms ( A vH x ) = B ) )
14	6 13	mpd	|- ( A E. x e. HAtoms ( A vH x ) = B )