Theorem unopf1ot 9831

Description: A unitary operator in Hilbert space is one-to-one and onto.

Assertion

Ref	Expression
unopf1ot	|- (T e. UniOp -> T:H~-1-1-onto->H~)

Proof of Theorem unopf1ot

Step	Hyp	Ref	Expression
1		elunopt 9790	. . . . . . 7 |- (T e. UniOp <-> (T:H~-onto->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih (T` y)) = (x .ih y)))
2	1	pm3.26bi 322	. . . . . 6 |- (T e. UniOp -> T:H~-onto->H~)
3		fof 3669	. . . . . 6 |- (T:H~-onto->H~ -> T:H~-->H~)
4	2, 3	syl 10	. . . . 5 |- (T e. UniOp -> T:H~-->H~)
5		unopt 9830	. . . . . . . . . . . . . . . 16 |- ((T e. UniOp /\ x e. H~ /\ x e. H~) -> ((T` x) .ih (T` x)) = (x .ih x))
6	5	3anidm23 883	. . . . . . . . . . . . . . 15 |- ((T e. UniOp /\ x e. H~) -> ((T` x) .ih (T` x)) = (x .ih x))
7	6	3adant3 798	. . . . . . . . . . . . . 14 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> ((T` x) .ih (T` x)) = (x .ih x))
8		unopt 9830	. . . . . . . . . . . . . . . 16 |- ((T e. UniOp /\ y e. H~ /\ y e. H~) -> ((T` y) .ih (T` y)) = (y .ih y))
9	8	3anidm23 883	. . . . . . . . . . . . . . 15 |- ((T e. UniOp /\ y e. H~) -> ((T` y) .ih (T` y)) = (y .ih y))
10	9	3adant2 797	. . . . . . . . . . . . . 14 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> ((T` y) .ih (T` y)) = (y .ih y))
11	7, 10	opreq12d 3975	. . . . . . . . . . . . 13 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> (((T` x) .ih (T` x)) + ((T` y) .ih (T` y))) = ((x .ih x) + (y .ih y)))
12		unopt 9830	. . . . . . . . . . . . . 14 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> ((T` x) .ih (T` y)) = (x .ih y))
13		unopt 9830	. . . . . . . . . . . . . . 15 |- ((T e. UniOp /\ y e. H~ /\ x e. H~) -> ((T` y) .ih (T` x)) = (y .ih x))
14	13	3com23 838	. . . . . . . . . . . . . 14 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> ((T` y) .ih (T` x)) = (y .ih x))
15	12, 14	opreq12d 3975	. . . . . . . . . . . . 13 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> (((T` x) .ih (T` y)) + ((T` y) .ih (T` x))) = ((x .ih y) + (y .ih x)))
16	11, 15	opreq12d 3975	. . . . . . . . . . . 12 |- ((T e. UniOp /\ x e. H~ /\ y e. H~) -> ((((T` x) .ih (T` x)) + ((T` y) .ih (T` y))) - (((T` x) .ih (T` y)) + ((T` y) .ih (T` x)))) = (((x .ih x) + (y .ih y)) - ((x .ih y) + (y .ih x))))
17	16	3expb 833	. . . . . . . . . . 11 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((((T` x) .ih (T` x)) + ((T` y) .ih (T` y))) - (((T` x) .ih (T` y)) + ((T` y) .ih (T` x)))) = (((x .ih x) + (y .ih y)) - ((x .ih y) + (y .ih x))))
18		ffvelrn 3811	. . . . . . . . . . . . . . 15 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
19		ffvelrn 3811	. . . . . . . . . . . . . . 15 |- ((T:H~-->H~ /\ y e. H~) -> (T` y) e. H~)
20	18, 19	anim12i 333	. . . . . . . . . . . . . 14 |- (((T:H~-->H~ /\ x e. H~) /\ (T:H~-->H~ /\ y e. H~)) -> ((T` x) e. H~ /\ (T` y) e. H~))
21	20	anandis 512	. . . . . . . . . . . . 13 |- ((T:H~-->H~ /\ (x e. H~ /\ y e. H~)) -> ((T` x) e. H~ /\ (T` y) e. H~))
22	21, 4	sylan 448	. . . . . . . . . . . 12 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((T` x) e. H~ /\ (T` y) e. H~))
23		normlem9at 8971	. . . . . . . . . . . 12 |- (((T` x) e. H~ /\ (T` y) e. H~) -> (((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = ((((T` x) .ih (T` x)) + ((T` y) .ih (T` y))) - (((T` x) .ih (T` y)) + ((T` y) .ih (T` x)))))
24	22, 23	syl 10	. . . . . . . . . . 11 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> (((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = ((((T` x) .ih (T` x)) + ((T` y) .ih (T` y))) - (((T` x) .ih (T` y)) + ((T` y) .ih (T` x)))))
25		normlem9at 8971	. . . . . . . . . . . 12 |- ((x e. H~ /\ y e. H~) -> ((x -h y) .ih (x -h y)) = (((x .ih x) + (y .ih y)) - ((x .ih y) + (y .ih x))))
26	25	adantl 388	. . . . . . . . . . 11 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((x -h y) .ih (x -h y)) = (((x .ih x) + (y .ih y)) - ((x .ih y) + (y .ih x))))
27	17, 24, 26	3eqtr4rd 1517	. . . . . . . . . 10 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((x -h y) .ih (x -h y)) = (((T` x) -h (T` y)) .ih ((T` x) -h (T` y))))
28	27	eqeq1d 1482	. . . . . . . . 9 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> (((x -h y) .ih (x -h y)) = 0 <-> (((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = 0))
29		hvsubclt 8871	. . . . . . . . . . . 12 |- ((x e. H~ /\ y e. H~) -> (x -h y) e. H~)
30		his6t 8949	. . . . . . . . . . . 12 |- ((x -h y) e. H~ -> (((x -h y) .ih (x -h y)) = 0 <-> (x -h y) = 0h))
31	29, 30	syl 10	. . . . . . . . . . 11 |- ((x e. H~ /\ y e. H~) -> (((x -h y) .ih (x -h y)) = 0 <-> (x -h y) = 0h))
32		hvsubeq0t 8919	. . . . . . . . . . 11 |- ((x e. H~ /\ y e. H~) -> ((x -h y) = 0h <-> x = y))
33	31, 32	bitrd 527	. . . . . . . . . 10 |- ((x e. H~ /\ y e. H~) -> (((x -h y) .ih (x -h y)) = 0 <-> x = y))
34	33	adantl 388	. . . . . . . . 9 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> (((x -h y) .ih (x -h y)) = 0 <-> x = y))
35		hvsubclt 8871	. . . . . . . . . . . 12 |- (((T` x) e. H~ /\ (T` y) e. H~) -> ((T` x) -h (T` y)) e. H~)
36		his6t 8949	. . . . . . . . . . . 12 |- (((T` x) -h (T` y)) e. H~ -> ((((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = 0 <-> ((T` x) -h (T` y)) = 0h))
37	35, 36	syl 10	. . . . . . . . . . 11 |- (((T` x) e. H~ /\ (T` y) e. H~) -> ((((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = 0 <-> ((T` x) -h (T` y)) = 0h))
38		hvsubeq0t 8919	. . . . . . . . . . 11 |- (((T` x) e. H~ /\ (T` y) e. H~) -> (((T` x) -h (T` y)) = 0h <-> (T` x) = (T` y)))
39	37, 38	bitrd 527	. . . . . . . . . 10 |- (((T` x) e. H~ /\ (T` y) e. H~) -> ((((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = 0 <-> (T` x) = (T` y)))
40	22, 39	syl 10	. . . . . . . . 9 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((((T` x) -h (T` y)) .ih ((T` x) -h (T` y))) = 0 <-> (T` x) = (T` y)))
41	28, 34, 40	3bitr3rd 548	. . . . . . . 8 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((T` x) = (T` y) <-> x = y))
42	41	biimpd 153	. . . . . . 7 |- ((T e. UniOp /\ (x e. H~ /\ y e. H~)) -> ((T` x) = (T` y) -> x = y))
43	42	ex 373	. . . . . 6 |- (T e. UniOp -> ((x e. H~ /\ y e. H~) -> ((T` x) = (T` y) -> x = y)))
44	43	r19.21aivv 1719	. . . . 5 |- (T e. UniOp -> A.x e. H~ A.y e. H~ ((T` x) = (T` y) -> x = y))
45	4, 44	jca 288	. . . 4 |- (T e. UniOp -> (T:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) = (T