adjmul

Description: The adjoint of the scalar product of an operator. Theorem 3.11(ii) of Beran p. 106. (Contributed by NM, 21-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	adjmul	$⊢ (A \in ℂ \land T \in dom {adj}_{h}) \to {adj}_{h} (A \cdot_{op} T) = \overline{A} \cdot_{op} {adj}_{h} (T)$

Proof

Step	Hyp	Ref	Expression
1		dmadjop	$⊢ T \in dom {adj}_{h} \to T : ℋ ⟶ ℋ$
2		homulcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
3	1 2	sylan2	$⊢ (A \in ℂ \land T \in dom {adj}_{h}) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
4		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
5		dmadjrn	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) \in dom {adj}_{h}$
6		dmadjop	$⊢ {adj}_{h} (T) \in dom {adj}_{h} \to {adj}_{h} (T) : ℋ ⟶ ℋ$
7	5 6	syl	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) : ℋ ⟶ ℋ$
8		homulcl	$⊢ (\overline{A} \in ℂ \land {adj}_{h} (T) : ℋ ⟶ ℋ) \to (\overline{A} \cdot_{op} {adj}_{h} (T)) : ℋ ⟶ ℋ$
9	4 7 8	syl2an	$⊢ (A \in ℂ \land T \in dom {adj}_{h}) \to (\overline{A} \cdot_{op} {adj}_{h} (T)) : ℋ ⟶ ℋ$
10		adj2	$⊢ (T \in dom {adj}_{h} \land x \in ℋ \land y \in ℋ) \to T (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (T) (y)$
11	10	3expb	$⊢ (T \in dom {adj}_{h} \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (T) (y)$
12	11	adantll	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (T) (y)$
13	12	oveq2d	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to A (T (x) \cdot_{ih} y) = A (x \cdot_{ih} {adj}_{h} (T) (y))$
14	1	ffvelcdmda	$⊢ (T \in dom {adj}_{h} \land x \in ℋ) \to T (x) \in ℋ$
15		ax-his3	$⊢ (A \in ℂ \land T (x) \in ℋ \land y \in ℋ) \to (A \cdot_{ℎ} T (x)) \cdot_{ih} y = A (T (x) \cdot_{ih} y)$
16	14 15	syl3an2	$⊢ (A \in ℂ \land (T \in dom {adj}_{h} \land x \in ℋ) \land y \in ℋ) \to (A \cdot_{ℎ} T (x)) \cdot_{ih} y = A (T (x) \cdot_{ih} y)$
17	16	3exp	$⊢ A \in ℂ \to ((T \in dom {adj}_{h} \land x \in ℋ) \to (y \in ℋ \to (A \cdot_{ℎ} T (x)) \cdot_{ih} y = A (T (x) \cdot_{ih} y)))$
18	17	expd	$⊢ A \in ℂ \to (T \in dom {adj}_{h} \to (x \in ℋ \to (y \in ℋ \to (A \cdot_{ℎ} T (x)) \cdot_{ih} y = A (T (x) \cdot_{ih} y))))$
19	18	imp43	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (A \cdot_{ℎ} T (x)) \cdot_{ih} y = A (T (x) \cdot_{ih} y)$
20		simpll	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to A \in ℂ$
21		simprl	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \in ℋ$
22		adjcl	$⊢ (T \in dom {adj}_{h} \land y \in ℋ) \to {adj}_{h} (T) (y) \in ℋ$
23	22	ad2ant2l	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to {adj}_{h} (T) (y) \in ℋ$
24		his52	$⊢ (A \in ℂ \land x \in ℋ \land {adj}_{h} (T) (y) \in ℋ) \to x \cdot_{ih} (\overline{A} \cdot_{ℎ} {adj}_{h} (T) (y)) = A (x \cdot_{ih} {adj}_{h} (T) (y))$
25	20 21 23 24	syl3anc	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (\overline{A} \cdot_{ℎ} {adj}_{h} (T) (y)) = A (x \cdot_{ih} {adj}_{h} (T) (y))$
26	13 19 25	3eqtr4d	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (A \cdot_{ℎ} T (x)) \cdot_{ih} y = x \cdot_{ih} (\overline{A} \cdot_{ℎ} {adj}_{h} (T) (y))$
27		homval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
28	1 27	syl3an2	$⊢ (A \in ℂ \land T \in dom {adj}_{h} \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
29	28	3expa	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
30	29	adantrr	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
31	30	oveq1d	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (A \cdot_{op} T) (x) \cdot_{ih} y = (A \cdot_{ℎ} T (x)) \cdot_{ih} y$
32		id	$⊢ y \in ℋ \to y \in ℋ$
33		homval	$⊢ (\overline{A} \in ℂ \land {adj}_{h} (T) : ℋ ⟶ ℋ \land y \in ℋ) \to (\overline{A} \cdot_{op} {adj}_{h} (T)) (y) = \overline{A} \cdot_{ℎ} {adj}_{h} (T) (y)$
34	4 7 32 33	syl3an	$⊢ (A \in ℂ \land T \in dom {adj}_{h} \land y \in ℋ) \to (\overline{A} \cdot_{op} {adj}_{h} (T)) (y) = \overline{A} \cdot_{ℎ} {adj}_{h} (T) (y)$
35	34	3expa	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land y \in ℋ) \to (\overline{A} \cdot_{op} {adj}_{h} (T)) (y) = \overline{A} \cdot_{ℎ} {adj}_{h} (T) (y)$
36	35	adantrl	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (\overline{A} \cdot_{op} {adj}_{h} (T)) (y) = \overline{A} \cdot_{ℎ} {adj}_{h} (T) (y)$
37	36	oveq2d	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (\overline{A} \cdot_{op} {adj}_{h} (T)) (y) = x \cdot_{ih} (\overline{A} \cdot_{ℎ} {adj}_{h} (T) (y))$
38	26 31 37	3eqtr4d	$⊢ ((A \in ℂ \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (A \cdot_{op} T) (x) \cdot_{ih} y = x \cdot_{ih} (\overline{A} \cdot_{op} {adj}_{h} (T)) (y)$
39	38	ralrimivva	$⊢ (A \in ℂ \land T \in dom {adj}_{h}) \to \forall x \in ℋ \forall y \in ℋ (A \cdot_{op} T) (x) \cdot_{ih} y = x \cdot_{ih} (\overline{A} \cdot_{op} {adj}_{h} (T)) (y)$
40		adjeq	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (\overline{A} \cdot_{op} {adj}_{h} (T)) : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ (A \cdot_{op} T) (x) \cdot_{ih} y = x \cdot_{ih} (\overline{A} \cdot_{op} {adj}_{h} (T)) (y)) \to {adj}_{h} (A \cdot_{op} T) = \overline{A} \cdot_{op} {adj}_{h} (T)$
41	3 9 39 40	syl3anc	$⊢ (A \in ℂ \land T \in dom {adj}_{h}) \to {adj}_{h} (A \cdot_{op} T) = \overline{A} \cdot_{op} {adj}_{h} (T)$

Metamath Proof Explorer

Theorem adjmul

Proof