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

Metamath Proof Explorer

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 imbitrid ⊢ ( 𝐵 ∈ 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 imbitrrdi ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )