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

Metamath Proof Explorer

Theorem atord

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

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) )
2 1 anbi2d ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵 ) ↔ ( 𝐵 ∈ HAtoms ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) ) )
3 sseq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) )
4 fveq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) )
5 4 sseq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ↔ 𝐵 ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) )
6 3 5 orbi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) ↔ ( 𝐵 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∨ 𝐵 ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) ) )
7 2 6 imbi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵 ) → ( 𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ↔ ( ( 𝐵 ∈ HAtoms ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) → ( 𝐵 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∨ 𝐵 ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) ) ) )
8 h0elch ⊢ 0ℋ ∈ Cℋ
9 8 elimel ⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
10 9 atordi ⊢ ( ( 𝐵 ∈ HAtoms ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) → ( 𝐵 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∨ 𝐵 ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) )
11 7 10 dedth ⊢ ( 𝐴 ∈ Cℋ → ( ( 𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵 ) → ( 𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) ) )
12 11 3impib ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵 ) → ( 𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )