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
|- H e. CH
pjidm.2
|- A e. ~H
pjadj.3
|- B e. ~H
Assertion pjadjii
|- ( ( ( projh ` H ) ` A ) .ih B ) = ( A .ih ( ( projh ` H ) ` B ) )

Proof

Step Hyp Ref Expression
1 pjidm.1
 |-  H e. CH
2 pjidm.2
 |-  A e. ~H
3 pjadj.3
 |-  B e. ~H
4 3 2 pjorthi
 |-  ( H e. CH -> ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 )
5 1 4 ax-mp
 |-  ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0
6 5 fveq2i
 |-  ( * ` ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) = ( * ` 0 )
7 cj0
 |-  ( * ` 0 ) = 0
8 6 7 eqtri
 |-  ( * ` ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) = 0
9 1 choccli
 |-  ( _|_ ` H ) e. CH
10 9 2 pjhclii
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H
11 1 3 pjhclii
 |-  ( ( projh ` H ) ` B ) e. ~H
12 10 11 his1i
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) = ( * ` ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
13 2 3 pjorthi
 |-  ( H e. CH -> ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) = 0 )
14 1 13 ax-mp
 |-  ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) = 0
15 8 12 14 3eqtr4ri
 |-  ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) = ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) )
16 15 oveq2i
 |-  ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) )
17 1 2 pjhclii
 |-  ( ( projh ` H ) ` A ) e. ~H
18 9 3 pjhclii
 |-  ( ( projh ` ( _|_ ` H ) ) ` B ) e. ~H
19 his7
 |-  ( ( ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` H ) ` B ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` B ) e. ~H ) -> ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) )
20 17 11 18 19 mp3an
 |-  ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) )
21 ax-his2
 |-  ( ( ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H /\ ( ( projh ` H ) ` B ) e. ~H ) -> ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) ) )
22 17 10 11 21 mp3an
 |-  ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) )
23 16 20 22 3eqtr4i
 |-  ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) )
24 1 3 pjpji
 |-  B = ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) )
25 24 oveq2i
 |-  ( ( ( projh ` H ) ` A ) .ih B ) = ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) )
26 1 2 pjpji
 |-  A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
27 26 oveq1i
 |-  ( A .ih ( ( projh ` H ) ` B ) ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) )
28 23 25 27 3eqtr4i
 |-  ( ( ( projh ` H ) ` A ) .ih B ) = ( A .ih ( ( projh ` H ) ` B ) )