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 UniOp \to T \in LinOp$

Proof

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

Metamath Proof Explorer

Theorem unoplin

Proof