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

Metamath Proof Explorer

Theorem shorth

Description: Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shorth ( 𝐻 ∈ Sℋ → ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ·ih 𝐵 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( 𝐴 ∈ 𝐺 → 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) )
2 1 anim1d ⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐵 ∈ 𝐻 ) ) )
3 2 imp ⊢ ( ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ∧ ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐵 ∈ 𝐻 ) )
4 3 ancomd ⊢ ( ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ∧ ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) ) → ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) )
5 shocorth ⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐵 ·ih 𝐴 ) = 0 ) )
6 5 imp ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( 𝐵 ·ih 𝐴 ) = 0 )
7 shss ⊢ ( 𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ )
8 7 sseld ⊢ ( 𝐻 ∈ Sℋ → ( 𝐵 ∈ 𝐻 → 𝐵 ∈ ℋ ) )
9 shocss ⊢ ( 𝐻 ∈ Sℋ → ( ⊥ ‘ 𝐻 ) ⊆ ℋ )
10 9 sseld ⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) → 𝐴 ∈ ℋ ) )
11 8 10 anim12d ⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) ) )
12 11 imp ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) )
13 orthcom ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝐵 ·ih 𝐴 ) = 0 ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )
14 12 13 syl ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ( 𝐵 ·ih 𝐴 ) = 0 ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )
15 6 14 mpbid ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( 𝐵 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )
16 4 15 sylan2 ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ∧ ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )
17 16 exp32 ⊢ ( 𝐻 ∈ Sℋ → ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ·ih 𝐵 ) = 0 ) ) )