Metamath Proof Explorer

Theorem eigorth

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigorth 
|- ( ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. CC /\ D e. CC ) ) /\ ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( T ` A ) = ( T ` if ( A e. ~H , A , 0h ) ) )
2 oveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( C .h A ) = ( C .h if ( A e. ~H , A , 0h ) ) )
3 1 2 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( T ` A ) = ( C .h A ) <-> ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) ) )
4 3 anbi1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) <-> ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` B ) = ( D .h B ) ) ) )
5 4 anbi1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) <-> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) ) )
6 oveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A .ih ( T ` B ) ) = ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) )
7 1 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( T ` A ) .ih B ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) )
8 6 7 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) ) )
9 oveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A .ih B ) = ( if ( A e. ~H , A , 0h ) .ih B ) )
10 9 eqeq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A .ih B ) = 0 <-> ( if ( A e. ~H , A , 0h ) .ih B ) = 0 ) )
11 8 10 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) <-> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) <-> ( if ( A e. ~H , A , 0h ) .ih B ) = 0 ) ) )
12 5 11 imbi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) ) <-> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) <-> ( if ( A e. ~H , A , 0h ) .ih B ) = 0 ) ) ) )
13 fveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( T ` B ) = ( T ` if ( B e. ~H , B , 0h ) ) )
14 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( D .h B ) = ( D .h if ( B e. ~H , B , 0h ) ) )
15 13 14 eqeq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( T ` B ) = ( D .h B ) <-> ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) )
16 15 anbi2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` B ) = ( D .h B ) ) <-> ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) ) )
17 16 anbi1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) <-> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ C =/= ( * ` D ) ) ) )
18 13 oveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) )
19 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) )
20 18 19 eqeq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) <-> ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) ) )
21 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) .ih B ) = ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) )
22 21 eqeq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) .ih B ) = 0 <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) )
23 20 22 bibi12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) <-> ( if ( A e. ~H , A , 0h ) .ih B ) = 0 ) <-> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) ) )
24 17 23 imbi12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` B ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih B ) <-> ( if ( A e. ~H , A , 0h ) .ih B ) = 0 ) ) <-> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ C =/= ( * ` D ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) ) ) )
25 oveq1 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( C .h if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) )
26 25 eqeq2d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) <-> ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) ) )
27 26 anbi1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) <-> ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) ) )
28 neeq1 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( C =/= ( * ` D ) <-> if ( C e. CC , C , 0 ) =/= ( * ` D ) ) )
29 27 28 anbi12d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ C =/= ( * ` D ) ) <-> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` D ) ) ) )
30 29 imbi1d 
 |-  ( C = if ( C e. CC , C , 0 ) -> ( ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( C .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ C =/= ( * ` D ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) ) <-> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` D ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) ) ) )
31 oveq1 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( D .h if ( B e. ~H , B , 0h ) ) = ( if ( D e. CC , D , 0 ) .h if ( B e. ~H , B , 0h ) ) )
32 31 eqeq2d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) <-> ( T ` if ( B e. ~H , B , 0h ) ) = ( if ( D e. CC , D , 0 ) .h if ( B e. ~H , B , 0h ) ) ) )
33 32 anbi2d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) <-> ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( if ( D e. CC , D , 0 ) .h if ( B e. ~H , B , 0h ) ) ) ) )
34 fveq2 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( * ` D ) = ( * ` if ( D e. CC , D , 0 ) ) )
35 34 neeq2d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( if ( C e. CC , C , 0 ) =/= ( * ` D ) <-> if ( C e. CC , C , 0 ) =/= ( * ` if ( D e. CC , D , 0 ) ) ) )
36 33 35 anbi12d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` D ) ) <-> ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( if ( D e. CC , D , 0 ) .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` if ( D e. CC , D , 0 ) ) ) ) )
37 36 imbi1d 
 |-  ( D = if ( D e. CC , D , 0 ) -> ( ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( D .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` D ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) ) <-> ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( if ( D e. CC , D , 0 ) .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` if ( D e. CC , D , 0 ) ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) ) ) )
38 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
39 ifhvhv0 
 |-  if ( B e. ~H , B , 0h ) e. ~H
40 0cn 
 |-  0 e. CC
41 40 elimel 
 |-  if ( C e. CC , C , 0 ) e. CC
42 40 elimel 
 |-  if ( D e. CC , D , 0 ) e. CC
43 38 39 41 42 eigorthi 
 |-  ( ( ( ( T ` if ( A e. ~H , A , 0h ) ) = ( if ( C e. CC , C , 0 ) .h if ( A e. ~H , A , 0h ) ) /\ ( T ` if ( B e. ~H , B , 0h ) ) = ( if ( D e. CC , D , 0 ) .h if ( B e. ~H , B , 0h ) ) ) /\ if ( C e. CC , C , 0 ) =/= ( * ` if ( D e. CC , D , 0 ) ) ) -> ( ( if ( A e. ~H , A , 0h ) .ih ( T ` if ( B e. ~H , B , 0h ) ) ) = ( ( T ` if ( A e. ~H , A , 0h ) ) .ih if ( B e. ~H , B , 0h ) ) <-> ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) = 0 ) )
44 12 24 30 37 43 dedth4h 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) ) )
45 44 imp 
 |-  ( ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. CC /\ D e. CC ) ) /\ ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) )