Theorem pjoi0i

Description: The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoi0.1	⊢ 𝐺 ∈ Cℋ
	pjoi0.2	⊢ 𝐻 ∈ Cℋ
	pjoi0.3	⊢ 𝐴 ∈ ℋ
Assertion	pjoi0i	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		pjoi0.1	⊢ 𝐺 ∈ Cℋ
2		pjoi0.2	⊢ 𝐻 ∈ Cℋ
3		pjoi0.3	⊢ 𝐴 ∈ ℋ
4	1 2 3	3pm3.2i	⊢ ( 𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ )
5		pjoi0	⊢ ( ( ( 𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 0 )
6	4 5	mpan	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 0 )