Theorem elunop2t 9938

Description: An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse.

Assertion

Ref	Expression
elunop2t	|- (T e. UniOp <-> (T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)))

Distinct variable group:   x,T

Proof of Theorem elunop2t

Step	Hyp	Ref	Expression
1		unoplint 9844	. . 3 |- (T e. UniOp -> T e. LinOp)
2		elunopt 9799	. . . 4 |- (T e. UniOp <-> (T:H~-onto->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih (T` y)) = (x .ih y)))
3	2	pm3.26bi 322	. . 3 |- (T e. UniOp -> T:H~-onto->H~)
4		unopnormt 9841	. . . 4 |- ((T e. UniOp /\ x e. H~) -> (normh` (T` x)) = (normh` x))
5	4	r19.21aiva 1714	. . 3 |- (T e. UniOp -> A.x e. H~ (normh` (T` x)) = (normh` x))
6	1, 3, 5	3jca 819	. 2 |- (T e. UniOp -> (T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)))
7		eleq1 1534	. . 3 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (T e. UniOp <-> if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) e. UniOp))
8		eleq1 1534	. . . . . . 7 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (T e. LinOp <-> if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) e. LinOp))
9		foeq1 3668	. . . . . . 7 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (T:H~-onto->H~ <-> if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)):H~-onto->H~))
10		fveq1 3723	. . . . . . . . . . 11 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (T` y) = (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y))
11	10	fveq2d 3728	. . . . . . . . . 10 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (normh` (T` y)) = (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)))
12	11	eqeq1d 1483	. . . . . . . . 9 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> ((normh` (T` y)) = (normh` y) <-> (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)) = (normh` y)))
13	12	ralbidv 1663	. . . . . . . 8 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (A.y e. H~ (normh` (T` y)) = (normh` y) <-> A.y e. H~ (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)) = (normh` y)))
14		fveq2 3724	. . . . . . . . . . 11 |- (x = y -> (T` x) = (T` y))
15	14	fveq2d 3728	. . . . . . . . . 10 |- (x = y -> (normh` (T` x)) = (normh` (T` y)))
16		fveq2 3724	. . . . . . . . . 10 |- (x = y -> (normh` x) = (normh` y))
17	15, 16	eqeq12d 1489	. . . . . . . . 9 |- (x = y -> ((normh` (T` x)) = (normh` x) <-> (normh` (T` y)) = (normh` y)))
18	17	cbvralv 1800	. . . . . . . 8 |- (A.x e. H~ (normh` (T` x)) = (normh` x) <-> A.y e. H~ (normh` (T` y)) = (normh` y))
19	13, 18	syl5bb 532	. . . . . . 7 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (A.x e. H~ (normh` (T` x)) = (normh` x) <-> A.y e. H~ (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)) = (normh` y)))
20	8, 9, 19	3anbi123d 893	. . . . . 6 |- (T = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> ((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)) <-> (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) e. LinOp /\ if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)):H~-onto->H~ /\ A.y e. H~ (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)) = (normh` y))))
21		eleq1 1534	. . . . . . 7 |- ((I |` H~) = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> ((I |` H~) e. LinOp <-> if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) e. LinOp))
22		foeq1 3668	. . . . . . 7 |- ((I |` H~) = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> ((I |` H~):H~-onto->H~ <-> if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)):H~-onto->H~))
23		fveq1 3723	. . . . . . . . . 10 |- ((I |` H~) = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> ((I |` H~)` y) = (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y))
24	23	fveq2d 3728	. . . . . . . . 9 |- ((I |` H~) = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (normh` ((I |` H~)` y)) = (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)))
25	24	eqeq1d 1483	. . . . . . . 8 |- ((I |` H~) = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> ((normh` ((I |` H~)` y)) = (normh` y) <-> (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)) = (normh` y)))
26	25	ralbidv 1663	. . . . . . 7 |- ((I |` H~) = if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~)) -> (A.y e. H~ (normh` ((I |` H~)` y)) = (normh` y) <-> A.y e. H~ (normh` (if((T e. LinOp /\ T:H~-onto->H~ /\ A.x e. H~ (normh` (T` x)) = (normh` x)), T, (I |` H~))` y)) = (normh` y)))
27	21, 22, 26