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 𝐴C
Assertion atordi ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) → ( 𝐵𝐴𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 atoml.1 𝐴C
2 atelch ( 𝐵 ∈ HAtoms → 𝐵C )
3 1 choccli ( ⊥ ‘ 𝐴 ) ∈ C
4 chincl ( ( ( ⊥ ‘ 𝐴 ) ∈ C𝐵C ) → ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ C )
5 3 4 mpan ( 𝐵C → ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ C )
6 chj0 ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ C → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ 0 ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
7 5 6 syl ( 𝐵C → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ 0 ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
8 incom ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) )
9 7 8 eqtrdi ( 𝐵C → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ 0 ) = ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) )
10 h0elch 0C
11 chjcom ( ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ C ∧ 0C ) → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ 0 ) = ( 0 ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
12 5 10 11 sylancl ( 𝐵C → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ 0 ) = ( 0 ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
13 9 12 eqtr3d ( 𝐵C → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( 0 ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
14 incom ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) )
15 1 chocini ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0
16 14 15 eqtri ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) = 0
17 16 oveq1i ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = ( 0 ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
18 13 17 eqtr4di ( 𝐵C → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
19 18 adantr ( ( 𝐵C𝐴 𝐶 𝐵 ) → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
20 1 cmidi 𝐴 𝐶 𝐴
21 1 1 20 cmcm2ii 𝐴 𝐶 ( ⊥ ‘ 𝐴 )
22 fh2 ( ( ( ( ⊥ ‘ 𝐴 ) ∈ C𝐴C𝐵C ) ∧ ( 𝐴 𝐶 ( ⊥ ‘ 𝐴 ) ∧ 𝐴 𝐶 𝐵 ) ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
23 21 22 mpanr1 ( ( ( ( ⊥ ‘ 𝐴 ) ∈ C𝐴C𝐵C ) ∧ 𝐴 𝐶 𝐵 ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
24 1 23 mp3anl2 ( ( ( ( ⊥ ‘ 𝐴 ) ∈ C𝐵C ) ∧ 𝐴 𝐶 𝐵 ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
25 3 24 mpanl1 ( ( 𝐵C𝐴 𝐶 𝐵 ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐴 ) ∨ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
26 19 25 eqtr4d ( ( 𝐵C𝐴 𝐶 𝐵 ) → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) )
27 2 26 sylan ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) )
28 incom ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) )
29 27 28 eqtrdi ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
30 29 adantr ( ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) ∧ ¬ 𝐵𝐴 ) → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
31 1 atoml2i ( ( 𝐵 ∈ HAtoms ∧ ¬ 𝐵𝐴 ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )
32 31 adantlr ( ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) ∧ ¬ 𝐵𝐴 ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )
33 30 32 eqeltrd ( ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) ∧ ¬ 𝐵𝐴 ) → ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )
34 atssma ( ( 𝐵 ∈ HAtoms ∧ ( ⊥ ‘ 𝐴 ) ∈ C ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ↔ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
35 3 34 mpan2 ( 𝐵 ∈ HAtoms → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ↔ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
36 35 ad2antrr ( ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) ∧ ¬ 𝐵𝐴 ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ↔ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
37 33 36 mpbird ( ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) ∧ ¬ 𝐵𝐴 ) → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
38 37 ex ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) → ( ¬ 𝐵𝐴𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )
39 38 orrd ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶 𝐵 ) → ( 𝐵𝐴𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )