Metamath Proof Explorer


Theorem atordi

Description: An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1
|- A e. CH
Assertion atordi
|- ( ( B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) )

Proof

Step Hyp Ref Expression
1 atoml.1
 |-  A e. CH
2 atelch
 |-  ( B e. HAtoms -> B e. CH )
3 1 choccli
 |-  ( _|_ ` A ) e. CH
4 chincl
 |-  ( ( ( _|_ ` A ) e. CH /\ B e. CH ) -> ( ( _|_ ` A ) i^i B ) e. CH )
5 3 4 mpan
 |-  ( B e. CH -> ( ( _|_ ` A ) i^i B ) e. CH )
6 chj0
 |-  ( ( ( _|_ ` A ) i^i B ) e. CH -> ( ( ( _|_ ` A ) i^i B ) vH 0H ) = ( ( _|_ ` A ) i^i B ) )
7 5 6 syl
 |-  ( B e. CH -> ( ( ( _|_ ` A ) i^i B ) vH 0H ) = ( ( _|_ ` A ) i^i B ) )
8 incom
 |-  ( ( _|_ ` A ) i^i B ) = ( B i^i ( _|_ ` A ) )
9 7 8 eqtrdi
 |-  ( B e. CH -> ( ( ( _|_ ` A ) i^i B ) vH 0H ) = ( B i^i ( _|_ ` A ) ) )
10 h0elch
 |-  0H e. CH
11 chjcom
 |-  ( ( ( ( _|_ ` A ) i^i B ) e. CH /\ 0H e. CH ) -> ( ( ( _|_ ` A ) i^i B ) vH 0H ) = ( 0H vH ( ( _|_ ` A ) i^i B ) ) )
12 5 10 11 sylancl
 |-  ( B e. CH -> ( ( ( _|_ ` A ) i^i B ) vH 0H ) = ( 0H vH ( ( _|_ ` A ) i^i B ) ) )
13 9 12 eqtr3d
 |-  ( B e. CH -> ( B i^i ( _|_ ` A ) ) = ( 0H vH ( ( _|_ ` A ) i^i B ) ) )
14 incom
 |-  ( ( _|_ ` A ) i^i A ) = ( A i^i ( _|_ ` A ) )
15 1 chocini
 |-  ( A i^i ( _|_ ` A ) ) = 0H
16 14 15 eqtri
 |-  ( ( _|_ ` A ) i^i A ) = 0H
17 16 oveq1i
 |-  ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) = ( 0H vH ( ( _|_ ` A ) i^i B ) )
18 13 17 eqtr4di
 |-  ( B e. CH -> ( B i^i ( _|_ ` A ) ) = ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) )
19 18 adantr
 |-  ( ( B e. CH /\ A C_H B ) -> ( B i^i ( _|_ ` A ) ) = ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) )
20 1 cmidi
 |-  A C_H A
21 1 1 20 cmcm2ii
 |-  A C_H ( _|_ ` A )
22 fh2
 |-  ( ( ( ( _|_ ` A ) e. CH /\ A e. CH /\ B e. CH ) /\ ( A C_H ( _|_ ` A ) /\ A C_H B ) ) -> ( ( _|_ ` A ) i^i ( A vH B ) ) = ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) )
23 21 22 mpanr1
 |-  ( ( ( ( _|_ ` A ) e. CH /\ A e. CH /\ B e. CH ) /\ A C_H B ) -> ( ( _|_ ` A ) i^i ( A vH B ) ) = ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) )
24 1 23 mp3anl2
 |-  ( ( ( ( _|_ ` A ) e. CH /\ B e. CH ) /\ A C_H B ) -> ( ( _|_ ` A ) i^i ( A vH B ) ) = ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) )
25 3 24 mpanl1
 |-  ( ( B e. CH /\ A C_H B ) -> ( ( _|_ ` A ) i^i ( A vH B ) ) = ( ( ( _|_ ` A ) i^i A ) vH ( ( _|_ ` A ) i^i B ) ) )
26 19 25 eqtr4d
 |-  ( ( B e. CH /\ A C_H B ) -> ( B i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( A vH B ) ) )
27 2 26 sylan
 |-  ( ( B e. HAtoms /\ A C_H B ) -> ( B i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( A vH B ) ) )
28 incom
 |-  ( ( _|_ ` A ) i^i ( A vH B ) ) = ( ( A vH B ) i^i ( _|_ ` A ) )
29 27 28 eqtrdi
 |-  ( ( B e. HAtoms /\ A C_H B ) -> ( B i^i ( _|_ ` A ) ) = ( ( A vH B ) i^i ( _|_ ` A ) ) )
30 29 adantr
 |-  ( ( ( B e. HAtoms /\ A C_H B ) /\ -. B C_ A ) -> ( B i^i ( _|_ ` A ) ) = ( ( A vH B ) i^i ( _|_ ` A ) ) )
31 1 atoml2i
 |-  ( ( B e. HAtoms /\ -. B C_ A ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms )
32 31 adantlr
 |-  ( ( ( B e. HAtoms /\ A C_H B ) /\ -. B C_ A ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms )
33 30 32 eqeltrd
 |-  ( ( ( B e. HAtoms /\ A C_H B ) /\ -. B C_ A ) -> ( B i^i ( _|_ ` A ) ) e. HAtoms )
34 atssma
 |-  ( ( B e. HAtoms /\ ( _|_ ` A ) e. CH ) -> ( B C_ ( _|_ ` A ) <-> ( B i^i ( _|_ ` A ) ) e. HAtoms ) )
35 3 34 mpan2
 |-  ( B e. HAtoms -> ( B C_ ( _|_ ` A ) <-> ( B i^i ( _|_ ` A ) ) e. HAtoms ) )
36 35 ad2antrr
 |-  ( ( ( B e. HAtoms /\ A C_H B ) /\ -. B C_ A ) -> ( B C_ ( _|_ ` A ) <-> ( B i^i ( _|_ ` A ) ) e. HAtoms ) )
37 33 36 mpbird
 |-  ( ( ( B e. HAtoms /\ A C_H B ) /\ -. B C_ A ) -> B C_ ( _|_ ` A ) )
38 37 ex
 |-  ( ( B e. HAtoms /\ A C_H B ) -> ( -. B C_ A -> B C_ ( _|_ ` A ) ) )
39 38 orrd
 |-  ( ( B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) )