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

Metamath Proof Explorer

Theorem chssoc

Description: A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chssoc ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 = 0ℋ ) )

Proof

Step Hyp Ref Expression
1 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
2 sslin ⊢ ( 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) → ( 𝐴 ∩ 𝐴 ) ⊆ ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) )
3 1 2 eqsstrrid ⊢ ( 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) → 𝐴 ⊆ ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) )
4 chocin ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )
5 4 sseq2d ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) ↔ 𝐴 ⊆ 0ℋ ) )
6 chle0 ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )
7 5 6 bitrd ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) ↔ 𝐴 = 0ℋ ) )
8 3 7 imbitrid ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) → 𝐴 = 0ℋ ) )
9 simpr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 = 0ℋ ) → 𝐴 = 0ℋ )
10 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
11 ch0le ⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ → 0ℋ ⊆ ( ⊥ ‘ 𝐴 ) )
12 10 11 syl ⊢ ( 𝐴 ∈ Cℋ → 0ℋ ⊆ ( ⊥ ‘ 𝐴 ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 = 0ℋ ) → 0ℋ ⊆ ( ⊥ ‘ 𝐴 ) )
14 9 13 eqsstrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 = 0ℋ ) → 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) )
15 14 ex ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 = 0ℋ → 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) ) )
16 8 15 impbid ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 = 0ℋ ) )