Metamath Proof Explorer

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ℎ ‘ 𝐻 ) ‘ 𝐵 ) )