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 ) ) )