Theorem orthin

Description: The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	orthin	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )

Proof

Step	Hyp	Ref	Expression
1		ssrin	⊢ ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( ⊥ ‘ 𝐵 ) ∩ 𝐵 ) )
2		incom	⊢ ( ( ⊥ ‘ 𝐵 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( ⊥ ‘ 𝐵 ) )
3	1 2	sseqtrdi	⊢ ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐵 ∩ ( ⊥ ‘ 𝐵 ) ) )
4		ocin	⊢ ( 𝐵 ∈ Sℋ → ( 𝐵 ∩ ( ⊥ ‘ 𝐵 ) ) = 0ℋ )
5	4	sseq2d	⊢ ( 𝐵 ∈ Sℋ → ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐵 ∩ ( ⊥ ‘ 𝐵 ) ) ↔ ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ) )
6	3 5	syl5ib	⊢ ( 𝐵 ∈ Sℋ → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ) )
7	6	adantl	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ) )
8		shincl	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Sℋ )
9		sh0le	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ Sℋ → 0ℋ ⊆ ( 𝐴 ∩ 𝐵 ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 0ℋ ⊆ ( 𝐴 ∩ 𝐵 ) )
11	7 10	jctird	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ∧ 0ℋ ⊆ ( 𝐴 ∩ 𝐵 ) ) ) )
12		eqss	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 0ℋ ∧ 0ℋ ⊆ ( 𝐴 ∩ 𝐵 ) ) )
13	11 12	syl6ibr	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )