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