Theorem unoplint 9783

Description: A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72.

Assertion

Ref	Expression
unoplint	|- (T e. UniOp -> T e. LinOp)

Proof of Theorem unoplint

Step	Hyp	Ref	Expression
1		unopf1ot 9779	. . . 4 |- (T e. UniOp -> T:H~-1-1-onto->H~)
2		f1of 3680	. . . 4 |- (T:H~-1-1-onto->H~ -> T:H~-->H~)
3	1, 2	syl 10	. . 3 |- (T e. UniOp -> T:H~-->H~)
4		unopadjt 9782	. . . . . . . . . 10 |- ((T e. UniOp /\ ((x .h y) +h z) e. H~ /\ w e. H~) -> ((T` ((x .h y) +h z)) .ih w) = (((x .h y) +h z) .ih (`'T` w)))
5		pm3.26 319	. . . . . . . . . . 11 |- ((T e. UniOp /\ (x e. CC /\ y e. H~)) -> T e. UniOp)
6	5	ad2antrr 404	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> T e. UniOp)
7		hvaddclt 8821	. . . . . . . . . . . . 13 |- (((x .h y) e. H~ /\ z e. H~) -> ((x .h y) +h z) e. H~)
8		hvmulclt 8822	. . . . . . . . . . . . 13 |- ((x e. CC /\ y e. H~) -> (x .h y) e. H~)
9	7, 8	sylan 448	. . . . . . . . . . . 12 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((x .h y) +h z) e. H~)
10	9	adantll 392	. . . . . . . . . . 11 |- (((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) -> ((x .h y) +h z) e. H~)
11	10	adantr 389	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((x .h y) +h z) e. H~)
12		pm3.27 323	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> w e. H~)
13	4, 6, 11, 12	syl3anc 857	. . . . . . . . 9 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((T` ((x .h y) +h z)) .ih w) = (((x .h y) +h z) .ih (`'T` w)))
14		hiassdit 8896	. . . . . . . . . 10 |- (((x e. CC /\ y e. H~) /\ (z e. H~ /\ (`'T` w) e. H~)) -> (((x .h y) +h z) .ih (`'T` w)) = ((x x. (y .ih (`'T` w))) + (z .ih (`'T` w))))
15		simprl 414	. . . . . . . . . . 11 |- ((T e. UniOp /\ (x e. CC /\ y e. H~)) -> x e. CC)
16	15	ad2antrr 404	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> x e. CC)
17		simprr 415	. . . . . . . . . . 11 |- ((T e. UniOp /\ (x e. CC /\ y e. H~)) -> y e. H~)
18	17	ad2antrr 404	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> y e. H~)
19		simplr 413	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> z e. H~)
20		ffvelrn 3805	. . . . . . . . . . . . 13 |- ((`'T:H~-->H~ /\ w e. H~) -> (`'T` w) e. H~)
21		cnvunopt 9781	. . . . . . . . . . . . . 14 |- (T e. UniOp -> `'T e. UniOp)
22		unopf1ot 9779	. . . . . . . . . . . . . 14 |- (`'T e. UniOp -> `'T:H~-1-1-onto->H~)
23		f1of 3680	. . . . . . . . . . . . . 14 |- (`'T:H~-1-1-onto->H~ -> `'T:H~-->H~)
24	21, 22, 23	3syl 20	. . . . . . . . . . . . 13 |- (T e. UniOp -> `'T:H~-->H~)
25	20, 24	sylan 448	. . . . . . . . . . . 12 |- ((T e. UniOp /\ w e. H~) -> (`'T` w) e. H~)
26	25	adantlr 393	. . . . . . . . . . 11 |- (((T e. UniOp /\ z e. H~) /\ w e. H~) -> (`'T` w) e. H~)
27	26	adantllr 397	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (`'T` w) e. H~)
28	14, 16, 18, 19, 27	syl2anc 472	. . . . . . . . 9 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (((x .h y) +h z) .ih (`'T` w)) = ((x x. (y .ih (`'T` w))) + (z .ih (`'T` w))))
29		hiassdit 8896	. . . . . . . . . . 11 |- (((x e. CC /\ (T` y) e. H~) /\ ((T` z) e. H~ /\ w e. H~)) -> (((x .h (T` y)) +h (T` z)) .ih w) = ((x x. ((T` y) .ih w)) + ((T` z) .ih w)))
30		ffvelrn 3805	. . . . . . . . . . . . . 14 |- ((T:H~-->H~ /\ y e. H~) -> (T` y) e. H~)
31	30, 3	sylan 448	. . . . . . . . . . . . 13 |- ((T e. UniOp /\ y e. H~) -> (T` y) e. H~)
32	31	adantrl 394	. . . . . . . . . . . 12 |- ((T e. UniOp /\ (x e. CC /\ y e. H~)) -> (T` y) e. H~)
33	32	ad2antrr 404	. . . . . . . . . . 11 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (T` y) e. H~)
34		ffvelrn 3805	. . . . . . . . . . . . . 14 |- ((T:H~-->H~ /\ z e. H~) -> (T` z) e. H~)
35	34, 3	sylan 448	. . . . . . . . . . . . 13 |- ((T e. UniOp /\ z e. H~) -> (T` z) e. H~)
36	35	adantr 389	. . . . . . . . . . . 12 |- (((T e. UniOp /\ z e. H~) /\ w e. H~) -> (T` z) e. H~)
37	36	adantllr 397	. . . . . . . . . . 11 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (T` z) e. H~)
38	29, 16, 33, 37, 12	syl2anc 472	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (((x .h (T` y)) +h (T` z)) .ih w) = ((x x. ((T` y) .ih w)) + ((T` z) .ih w)))
39		unopadjt 9782	. . . . . . . . . . . . . . 15 |- ((T e. UniOp /\ y e. H~ /\ w e. H~) -> ((T` y) .ih w) = (y .ih (`'T` w)))
40	39	3expa 832	. . . . . . . . . . . . . 14 |- (((T e. UniOp /\ y e. H~) /\ w e. H~) -> ((T` y) .ih w) = (y .ih (`'T` w)))
41	40	opreq2d 3967	. . . . . . . . . . . . 13 |- (((T e. UniOp /\ y e. H~) /\ w e. H~) -> (x x. ((T` y) .ih w)) = (x x. (y .ih (`'T` w))))
42	41	adantlrl 398	. . . . . . . . . . . 12 |- (((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ w e. H~) -> (x x. ((T` y) .ih w)) = (x x. (y .ih (`'T` w))))
43	42	adantlr 393	. . . . . . . . . . 11 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (x x. ((T` y) .ih w)) = (x x. (y .ih (`'T` w))))
44		unopadjt 9782	. . . . . . . . . . . . 13 |- ((T e. UniOp /\ z e. H~ /\ w e. H~) -> ((T` z) .ih w) = (z .ih (`'T` w)))
45	44	3expa 832	. . . . . . . . . . . 12 |- (((T e. UniOp /\ z e. H~) /\ w e. H~) -> ((T` z) .ih w) = (z .ih (`'T` w)))
46	45	adantllr 397	. . . . . . . . . . 11 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((T` z) .ih w) = (z .ih (`'T` w)))
47	43, 46	opreq12d 3969	. . . . . . . . . 10 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((x x. ((T` y) .ih w)) + ((T` z) .ih w)) = ((x x. (y .ih (`'T` w))) + (z .ih (`'T` w))))
48	38, 47	eqtr2d 1505	. . . . . . . . 9 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((x x. (y .ih (`'T` w))) + (z .ih (`'T` w))) = (((x .h (T` y)) +h (T` z)) .ih w))
49	13, 28, 48	3eqtrd 1508	. . . . . . . 8 |- ((((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((T` ((x .h y) +h z)) .ih w) = (((x .h (T` y)) +h (T` z)) .ih w))
50	49	r19.21aiva 1711	. . . . . . 7 |- (((T e. UniOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) -> A.w e. H~ ((T` ((x .h y) +h z)) .ih w) = (((x .h (T` y)) +h (T` z)) .ih w))
51		hial2eqt 8911	. . . . . . . . 9 |- (((T` ((x .h y) +h z)) e. H~ /\ ((x .h (T` y)) +h (T` z)) e. H~) -> (A.w e. H~ ((T` ((x .h y) +h z)) .ih w) = (((x .h (T` y)) +h (T` z)) .ih w) <-> (T` ((x .h y) +h z)) = ((x .h (T` y)) +h (T` z))))
52		ffvelrn 3805	. . . . . . . . . . 11 |- ((T:H~-->H~ /\ ((x .h y) +h z) e. H~) -> (T` ((x .h y) +h z)) e. H~)
53	52, 9	sylan2 451	. . . . . . . . . 10 |- ((T