# Metamath Proof Explorer

## Theorem unoplin

Description: A unitary operator is linear. Theorem in AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unoplin ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{LinOp}$

### Proof

Step Hyp Ref Expression
1 unopf1o ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{1-1 onto}{⟶}ℋ$
2 f1of ${⊢}{T}:ℋ\underset{1-1 onto}{⟶}ℋ\to {T}:ℋ⟶ℋ$
3 1 2 syl ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ⟶ℋ$
4 simplll ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\in \mathrm{UniOp}$
5 hvmulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{ℎ}{y}\in ℋ$
6 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{y}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
7 5 6 sylan ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
8 7 adantll ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
9 8 adantr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ$
10 simpr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {w}\in ℋ$
11 unopadj ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\wedge {w}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
12 4 9 10 11 syl3anc ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
13 simprl ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {x}\in ℂ$
14 13 ad2antrr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}\in ℂ$
15 simprr ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {y}\in ℋ$
16 15 ad2antrr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {y}\in ℋ$
17 simplr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {z}\in ℋ$
18 cnvunop ${⊢}{T}\in \mathrm{UniOp}\to {{T}}^{-1}\in \mathrm{UniOp}$
19 unopf1o ${⊢}{{T}}^{-1}\in \mathrm{UniOp}\to {{T}}^{-1}:ℋ\underset{1-1 onto}{⟶}ℋ$
20 f1of ${⊢}{{T}}^{-1}:ℋ\underset{1-1 onto}{⟶}ℋ\to {{T}}^{-1}:ℋ⟶ℋ$
21 18 19 20 3syl ${⊢}{T}\in \mathrm{UniOp}\to {{T}}^{-1}:ℋ⟶ℋ$
22 21 ffvelrnda ${⊢}\left({T}\in \mathrm{UniOp}\wedge {w}\in ℋ\right)\to {{T}}^{-1}\left({w}\right)\in ℋ$
23 22 adantlr ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {{T}}^{-1}\left({w}\right)\in ℋ$
24 23 adantllr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {{T}}^{-1}\left({w}\right)\in ℋ$
25 hiassdi ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge \left({z}\in ℋ\wedge {{T}}^{-1}\left({w}\right)\in ℋ\right)\right)\to \left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)={x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)+\left({z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)$
26 14 16 17 24 25 syl22anc ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)={x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)+\left({z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)$
27 3 ffvelrnda ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to {T}\left({y}\right)\in ℋ$
28 27 adantrl ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {T}\left({y}\right)\in ℋ$
29 28 ad2antrr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left({y}\right)\in ℋ$
30 3 ffvelrnda ${⊢}\left({T}\in \mathrm{UniOp}\wedge {z}\in ℋ\right)\to {T}\left({z}\right)\in ℋ$
31 30 adantr ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left({z}\right)\in ℋ$
32 31 adantllr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left({z}\right)\in ℋ$
33 hiassdi ${⊢}\left(\left({x}\in ℂ\wedge {T}\left({y}\right)\in ℋ\right)\wedge \left({T}\left({z}\right)\in ℋ\wedge {w}\in ℋ\right)\right)\to \left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}={x}\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{w}\right)$
34 14 29 32 10 33 syl22anc ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}={x}\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{w}\right)$
35 unopadj ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\wedge {w}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}={y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
36 35 3expa ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}={y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
37 36 oveq2d ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}\right)={x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)$
38 37 adantlrl ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {w}\in ℋ\right)\to {x}\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}\right)={x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)$
39 38 adantlr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}\right)={x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)$
40 unopadj ${⊢}\left({T}\in \mathrm{UniOp}\wedge {z}\in ℋ\wedge {w}\in ℋ\right)\to {T}\left({z}\right){\cdot }_{\mathrm{ih}}{w}={z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
41 40 3expa ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left({z}\right){\cdot }_{\mathrm{ih}}{w}={z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
42 41 adantllr ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left({z}\right){\cdot }_{\mathrm{ih}}{w}={z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)$
43 39 42 oveq12d ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{w}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{w}\right)={x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)+\left({z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)$
44 34 43 eqtr2d ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}\left({y}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)+\left({z}{\cdot }_{\mathrm{ih}}{{T}}^{-1}\left({w}\right)\right)=\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}$
45 12 26 44 3eqtrd ${⊢}\left(\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\wedge {w}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}$
46 45 ralrimiva ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to \forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}$
47 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\in ℋ$
48 7 47 sylan2 ${⊢}\left({T}:ℋ⟶ℋ\wedge \left(\left({x}\in ℂ\wedge {y}\in ℋ\right)\wedge {z}\in ℋ\right)\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\in ℋ$
49 48 anassrs ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\in ℋ$
50 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right)\in ℋ$
51 hvmulcl ${⊢}\left({x}\in ℂ\wedge {T}\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ$
52 50 51 sylan2 ${⊢}\left({x}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ$
53 52 an12s ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ$
54 53 adantr ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ$
55 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {z}\in ℋ\right)\to {T}\left({z}\right)\in ℋ$
56 55 adantlr ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {T}\left({z}\right)\in ℋ$
57 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\in ℋ\wedge {T}\left({z}\right)\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\in ℋ$
58 54 56 57 syl2anc ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\in ℋ$
59 hial2eq ${⊢}\left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)\in ℋ\wedge \left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\in ℋ\right)\to \left(\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}↔{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
60 49 58 59 syl2anc ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to \left(\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}↔{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
61 3 60 sylanl1 ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to \left(\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{w}=\left(\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{w}↔{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
62 46 61 mpbid ${⊢}\left(\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
63 62 ralrimiva ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℂ\wedge {y}\in ℋ\right)\right)\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
64 63 ralrimivva ${⊢}{T}\in \mathrm{UniOp}\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
65 ellnop ${⊢}{T}\in \mathrm{LinOp}↔\left({T}:ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
66 3 64 65 sylanbrc ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{LinOp}$