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 ⊢ H ∈ S ℋ → G ⊆ ⊥ ⁡ H → A ∈ G ∧ B ∈ H → A ⋅ ih B = 0

Proof

Step Hyp Ref Expression
1 ssel ⊢ G ⊆ ⊥ ⁡ H → A ∈ G → A ∈ ⊥ ⁡ H
2 1 anim1d ⊢ G ⊆ ⊥ ⁡ H → A ∈ G ∧ B ∈ H → A ∈ ⊥ ⁡ H ∧ B ∈ H
3 2 imp ⊢ G ⊆ ⊥ ⁡ H ∧ A ∈ G ∧ B ∈ H → A ∈ ⊥ ⁡ H ∧ B ∈ H
4 3 ancomd ⊢ G ⊆ ⊥ ⁡ H ∧ A ∈ G ∧ B ∈ H → B ∈ H ∧ A ∈ ⊥ ⁡ H
5 shocorth ⊢ H ∈ S ℋ → B ∈ H ∧ A ∈ ⊥ ⁡ H → B ⋅ ih A = 0
6 5 imp ⊢ H ∈ S ℋ ∧ B ∈ H ∧ A ∈ ⊥ ⁡ H → B ⋅ ih A = 0
7 shss ⊢ H ∈ S ℋ → H ⊆ ℋ
8 7 sseld ⊢ H ∈ S ℋ → B ∈ H → B ∈ ℋ
9 shocss ⊢ H ∈ S ℋ → ⊥ ⁡ H ⊆ ℋ
10 9 sseld ⊢ H ∈ S ℋ → A ∈ ⊥ ⁡ H → A ∈ ℋ
11 8 10 anim12d ⊢ H ∈ S ℋ → B ∈ H ∧ A ∈ ⊥ ⁡ H → B ∈ ℋ ∧ A ∈ ℋ
12 11 imp ⊢ H ∈ S ℋ ∧ B ∈ H ∧ A ∈ ⊥ ⁡ H → B ∈ ℋ ∧ A ∈ ℋ
13 orthcom ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A = 0 ↔ A ⋅ ih B = 0
14 12 13 syl ⊢ H ∈ S ℋ ∧ B ∈ H ∧ A ∈ ⊥ ⁡ H → B ⋅ ih A = 0 ↔ A ⋅ ih B = 0
15 6 14 mpbid ⊢ H ∈ S ℋ ∧ B ∈ H ∧ A ∈ ⊥ ⁡ H → A ⋅ ih B = 0
16 4 15 sylan2 ⊢ H ∈ S ℋ ∧ G ⊆ ⊥ ⁡ H ∧ A ∈ G ∧ B ∈ H → A ⋅ ih B = 0
17 16 exp32 ⊢ H ∈ S ℋ → G ⊆ ⊥ ⁡ H → A ∈ G ∧ B ∈ H → A ⋅ ih B = 0