Theorem eigortht 9764

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.

Assertion

Ref	Expression
eigortht	|- ((((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 of Theorem eigortht

Step	Hyp	Ref	Expression
1		fveq2 3724	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (T` A) = (T` if(A e. H~, A, 0h)))
2		opreq2 3969	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (C .h A) = (C .h if(A e. H~, A, 0h)))
3	1, 2	eqeq12d 1489	. . . . . 6 |- (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 617	. . . . 5 |- (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 617	. . . 4 |- (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		opreq1 3968	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> (A .ih (T` B)) = (if(A e. H~, A, 0h) .ih (T` B)))
7	1	opreq1d 3975	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> ((T` A) .ih B) = ((T` if(A e. H~, A, 0h)) .ih B))
8	6, 7	eqeq12d 1489	. . . . 5 |- (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		opreq1 3968	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> (A .ih B) = (if(A e. H~, A, 0h) .ih B))
10	9	eqeq1d 1483	. . . . 5 |- (A = if(A e. H~, A, 0h) -> ((A .ih B) = 0 <-> (if(A e. H~, A, 0h) .ih B) = 0))
11	8, 10	bibi12d 629	. . . 4 |- (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 626	. . 3 |- (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 3724	. . . . . . 7 |- (B = if(B e. H~, B, 0h) -> (T` B) = (T` if(B e. H~, B, 0h)))
14		opreq2 3969	. . . . . . 7 |- (B = if(B e. H~, B, 0h) -> (D .h B) = (D .h if(B e. H~, B, 0h)))
15	13, 14	eqeq12d 1489	. . . . . 6 |- (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 616	. . . . 5 |- (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 617	. . . 4 |- (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	opreq2d 3976	. . . . . 6 |- (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		opreq2 3969	. . . . . 6 |- (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 1489	. . . . 5 |- (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		opreq2 3969	. . . . . 6 |- (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 1483	. . . . 5 |- (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 629	. . . 4 |- (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 626	. . 3 |- (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))