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