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

Metamath Proof Explorer

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