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