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