Theorem pjadjii

Description: A projection is self-adjoint. Property (i) of Beran p. 109. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	⊢ 𝐻 ∈ Cℋ
	pjidm.2	⊢ 𝐴 ∈ ℋ
	pjadj.3	⊢ 𝐵 ∈ ℋ
Assertion	pjadjii	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	⊢ 𝐻 ∈ Cℋ
2		pjidm.2	⊢ 𝐴 ∈ ℋ
3		pjadj.3	⊢ 𝐵 ∈ ℋ
4	3 2	pjorthi	⊢ ( 𝐻 ∈ Cℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = 0 )
5	1 4	ax-mp	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = 0
6	5	fveq2i	⊢ ( ∗ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) = ( ∗ ‘ 0 )
7		cj0	⊢ ( ∗ ‘ 0 ) = 0
8	6 7	eqtri	⊢ ( ∗ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) = 0
9	1	choccli	⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
10	9 2	pjhclii	⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ
11	1 3	pjhclii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ ℋ
12	10 11	his1i	⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ∗ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
13	2 3	pjorthi	⊢ ( 𝐻 ∈ Cℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) = 0 )
14	1 13	ax-mp	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) = 0
15	8 12 14	3eqtr4ri	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) = ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )
16	15	oveq2i	⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) + ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) + ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
17	1 2	pjhclii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
18	9 3	pjhclii	⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ℋ
19		his7	⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ ℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) + ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) )
20	17 11 18 19	mp3an	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) + ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) )
21		ax-his2	⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) + ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ) )
22	17 10 11 21	mp3an	⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) + ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
23	16 20 22	3eqtr4i	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )
24	1 3	pjpji	⊢ 𝐵 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) )
25	24	oveq2i	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) )
26	1 2	pjpji	⊢ 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )
27	26	oveq1i	⊢ ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )
28	23 25 27	3eqtr4i	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )