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

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 ⊢ 0ℋ ∈ Cℋ
11 chjcom ⊢ ( ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ∧ 0ℋ ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ 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 ∧ 𝐴 𝐶ℋ 𝐵 ) → ( 𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )