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⋅ihB=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⋅ihA=0
6 5 imp ⊢H∈Sℋ∧B∈H∧A∈⊥⁡H→B⋅ihA=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⋅ihA=0↔A⋅ihB=0
14 12 13 syl ⊢H∈Sℋ∧B∈H∧A∈⊥⁡H→B⋅ihA=0↔A⋅ihB=0
15 6 14 mpbid ⊢H∈Sℋ∧B∈H∧A∈⊥⁡H→A⋅ihB=0
16 4 15 sylan2 ⊢H∈Sℋ∧G⊆⊥⁡H∧A∈G∧B∈H→A⋅ihB=0
17 16 exp32 ⊢H∈Sℋ→G⊆⊥⁡H→A∈G∧B∈H→A⋅ihB=0