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	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A A = 0H ) )

Proof

Step	Hyp	Ref	Expression
1		atelch	|- ( B e. HAtoms -> B e. CH )
2		cvpss	|- ( ( A e. CH /\ B e. CH ) -> ( A A C. B ) )
3	1 2	sylan2	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A A C. B ) )
4		ch0le	|- ( A e. CH -> 0H C_ A )
5	4	adantr	|- ( ( A e. CH /\ B e. HAtoms ) -> 0H C_ A )
6	3 5	jctild	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A ( 0H C_ A /\ A C. B ) ) )
7		atcv0	|- ( B e. HAtoms -> 0H
8	7	adantr	|- ( ( B e. HAtoms /\ A e. CH ) -> 0H
9		h0elch	|- 0H e. CH
10		cvnbtwn3	|- ( ( 0H e. CH /\ B e. CH /\ A e. CH ) -> ( 0H ( ( 0H C_ A /\ A C. B ) -> A = 0H ) ) )
11	9 10	mp3an1	|- ( ( B e. CH /\ A e. CH ) -> ( 0H ( ( 0H C_ A /\ A C. B ) -> A = 0H ) ) )
12	1 11	sylan	|- ( ( B e. HAtoms /\ A e. CH ) -> ( 0H ( ( 0H C_ A /\ A C. B ) -> A = 0H ) ) )
13	8 12	mpd	|- ( ( B e. HAtoms /\ A e. CH ) -> ( ( 0H C_ A /\ A C. B ) -> A = 0H ) )
14	13	ancoms	|- ( ( A e. CH /\ B e. HAtoms ) -> ( ( 0H C_ A /\ A C. B ) -> A = 0H ) )
15	6 14	syld	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A A = 0H ) )
16		breq1	|- ( A = 0H -> ( A 0H
17	7 16	syl5ibrcom	|- ( B e. HAtoms -> ( A = 0H -> A
18	17	adantl	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A = 0H -> A
19	15 18	impbid	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A A = 0H ) )