adjlnop

Description: The adjoint of an operator is linear. Proposition 1 of AkhiezerGlazman p. 80. (Contributed by NM, 17-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	adjlnop	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) \in LinOp$

Proof

Step	Hyp	Ref	Expression
1		dmadjrn	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) \in dom {adj}_{h}$
2		dmadjop	$⊢ {adj}_{h} (T) \in dom {adj}_{h} \to {adj}_{h} (T) : ℋ ⟶ ℋ$
3	1 2	syl	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) : ℋ ⟶ ℋ$
4		simp2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to w \in ℋ$
5		adjcl	$⊢ (T \in dom {adj}_{h} \land y \in ℋ) \to {adj}_{h} (T) (y) \in ℋ$
6		hvmulcl	$⊢ (x \in ℂ \land {adj}_{h} (T) (y) \in ℋ) \to x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ$
7	5 6	sylan2	$⊢ (x \in ℂ \land (T \in dom {adj}_{h} \land y \in ℋ)) \to x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ$
8	7	an12s	$⊢ (T \in dom {adj}_{h} \land (x \in ℂ \land y \in ℋ)) \to x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ$
9	8	adantrr	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ$
10	9	3adant2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ$
11		adjcl	$⊢ (T \in dom {adj}_{h} \land z \in ℋ) \to {adj}_{h} (T) (z) \in ℋ$
12	11	adantrl	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to {adj}_{h} (T) (z) \in ℋ$
13	12	3adant2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to {adj}_{h} (T) (z) \in ℋ$
14		his7	$⊢ (w \in ℋ \land x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ \land {adj}_{h} (T) (z) \in ℋ) \to w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)) = (w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y))) + (w \cdot_{ih} {adj}_{h} (T) (z))$
15	4 10 13 14	syl3anc	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)) = (w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y))) + (w \cdot_{ih} {adj}_{h} (T) (z))$
16		adj2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land y \in ℋ) \to T (w) \cdot_{ih} y = w \cdot_{ih} {adj}_{h} (T) (y)$
17	16	3adant3l	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to T (w) \cdot_{ih} y = w \cdot_{ih} {adj}_{h} (T) (y)$
18	17	oveq2d	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to \overline{x} (T (w) \cdot_{ih} y) = \overline{x} (w \cdot_{ih} {adj}_{h} (T) (y))$
19		simp3l	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to x \in ℂ$
20		dmadjop	$⊢ T \in dom {adj}_{h} \to T : ℋ ⟶ ℋ$
21	20	ffvelcdmda	$⊢ (T \in dom {adj}_{h} \land w \in ℋ) \to T (w) \in ℋ$
22	21	3adant3	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to T (w) \in ℋ$
23		simp3r	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to y \in ℋ$
24		his5	$⊢ (x \in ℂ \land T (w) \in ℋ \land y \in ℋ) \to T (w) \cdot_{ih} (x \cdot_{ℎ} y) = \overline{x} (T (w) \cdot_{ih} y)$
25	19 22 23 24	syl3anc	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to T (w) \cdot_{ih} (x \cdot_{ℎ} y) = \overline{x} (T (w) \cdot_{ih} y)$
26		simp2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to w \in ℋ$
27	5	adantrl	$⊢ (T \in dom {adj}_{h} \land (x \in ℂ \land y \in ℋ)) \to {adj}_{h} (T) (y) \in ℋ$
28	27	3adant2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to {adj}_{h} (T) (y) \in ℋ$
29		his5	$⊢ (x \in ℂ \land w \in ℋ \land {adj}_{h} (T) (y) \in ℋ) \to w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y)) = \overline{x} (w \cdot_{ih} {adj}_{h} (T) (y))$
30	19 26 28 29	syl3anc	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y)) = \overline{x} (w \cdot_{ih} {adj}_{h} (T) (y))$
31	18 25 30	3eqtr4d	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \in ℂ \land y \in ℋ)) \to T (w) \cdot_{ih} (x \cdot_{ℎ} y) = w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y))$
32	31	3adant3r	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to T (w) \cdot_{ih} (x \cdot_{ℎ} y) = w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y))$
33		adj2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land z \in ℋ) \to T (w) \cdot_{ih} z = w \cdot_{ih} {adj}_{h} (T) (z)$
34	33	3adant3l	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to T (w) \cdot_{ih} z = w \cdot_{ih} {adj}_{h} (T) (z)$
35	32 34	oveq12d	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to (T (w) \cdot_{ih} (x \cdot_{ℎ} y)) + (T (w) \cdot_{ih} z) = (w \cdot_{ih} (x \cdot_{ℎ} {adj}_{h} (T) (y))) + (w \cdot_{ih} {adj}_{h} (T) (z))$
36	21	3adant3	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to T (w) \in ℋ$
37		hvmulcl	$⊢ (x \in ℂ \land y \in ℋ) \to x \cdot_{ℎ} y \in ℋ$
38	37	adantr	$⊢ ((x \in ℂ \land y \in ℋ) \land z \in ℋ) \to x \cdot_{ℎ} y \in ℋ$
39	38	3ad2ant3	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to x \cdot_{ℎ} y \in ℋ$
40		simp3r	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to z \in ℋ$
41		his7	$⊢ (T (w) \in ℋ \land x \cdot_{ℎ} y \in ℋ \land z \in ℋ) \to T (w) \cdot_{ih} ((x \cdot_{ℎ} y) +_{ℎ} z) = (T (w) \cdot_{ih} (x \cdot_{ℎ} y)) + (T (w) \cdot_{ih} z)$
42	36 39 40 41	syl3anc	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to T (w) \cdot_{ih} ((x \cdot_{ℎ} y) +_{ℎ} z) = (T (w) \cdot_{ih} (x \cdot_{ℎ} y)) + (T (w) \cdot_{ih} z)$
43		hvaddcl	$⊢ (x \cdot_{ℎ} y \in ℋ \land z \in ℋ) \to (x \cdot_{ℎ} y) +_{ℎ} z \in ℋ$
44	37 43	sylan	$⊢ ((x \in ℂ \land y \in ℋ) \land z \in ℋ) \to (x \cdot_{ℎ} y) +_{ℎ} z \in ℋ$
45		adj2	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land (x \cdot_{ℎ} y) +_{ℎ} z \in ℋ) \to T (w) \cdot_{ih} ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z)$
46	44 45	syl3an3	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to T (w) \cdot_{ih} ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z)$
47	42 46	eqtr3d	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to (T (w) \cdot_{ih} (x \cdot_{ℎ} y)) + (T (w) \cdot_{ih} z) = w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z)$
48	15 35 47	3eqtr2rd	$⊢ (T \in dom {adj}_{h} \land w \in ℋ \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
49	48	3com23	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ) \land w \in ℋ) \to w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
50	49	3expa	$⊢ ((T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \land w \in ℋ) \to w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
51	50	ralrimiva	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to \forall w \in ℋ w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
52		adjcl	$⊢ (T \in dom {adj}_{h} \land (x \cdot_{ℎ} y) +_{ℎ} z \in ℋ) \to {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) \in ℋ$
53	44 52	sylan2	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) \in ℋ$
54		hvaddcl	$⊢ (x \cdot_{ℎ} {adj}_{h} (T) (y) \in ℋ \land {adj}_{h} (T) (z) \in ℋ) \to (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z) \in ℋ$
55	8 11 54	syl2an	$⊢ ((T \in dom {adj}_{h} \land (x \in ℂ \land y \in ℋ)) \land (T \in dom {adj}_{h} \land z \in ℋ)) \to (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z) \in ℋ$
56	55	anandis	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z) \in ℋ$
57		hial2eq2	$⊢ ({adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) \in ℋ \land (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z) \in ℋ) \to (\forall w \in ℋ w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)) \leftrightarrow {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
58	53 56 57	syl2anc	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to (\forall w \in ℋ w \cdot_{ih} {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = w \cdot_{ih} ((x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)) \leftrightarrow {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
59	51 58	mpbid	$⊢ (T \in dom {adj}_{h} \land ((x \in ℂ \land y \in ℋ) \land z \in ℋ)) \to {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)$
60	59	exp32	$⊢ T \in dom {adj}_{h} \to ((x \in ℂ \land y \in ℋ) \to (z \in ℋ \to {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)))$
61	60	ralrimdv	$⊢ T \in dom {adj}_{h} \to ((x \in ℂ \land y \in ℋ) \to \forall z \in ℋ {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
62	61	ralrimivv	$⊢ T \in dom {adj}_{h} \to \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z)$
63		ellnop	$⊢ {adj}_{h} (T) \in LinOp \leftrightarrow ({adj}_{h} (T) : ℋ ⟶ ℋ \land \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ {adj}_{h} (T) ((x \cdot_{ℎ} y) +_{ℎ} z) = (x \cdot_{ℎ} {adj}_{h} (T) (y)) +_{ℎ} {adj}_{h} (T) (z))$
64	3 62 63	sylanbrc	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) \in LinOp$

Metamath Proof Explorer

Theorem adjlnop

Proof