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	syl5ib	⊢ ( 𝐴 ∈ 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ℋ ) )