hmopco

Description: The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hmopco	$⊢ (T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \to T \circ U \in HrmOp$

Proof

Step	Hyp	Ref	Expression
1		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
2		hmopf	$⊢ U \in HrmOp \to U : ℋ ⟶ ℋ$
3		fco	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T \circ U) : ℋ ⟶ ℋ$
4	1 2 3	syl2an	$⊢ (T \in HrmOp \land U \in HrmOp) \to (T \circ U) : ℋ ⟶ ℋ$
5	4	3adant3	$⊢ (T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \to (T \circ U) : ℋ ⟶ ℋ$
6		fvco3	$⊢ (U : ℋ ⟶ ℋ \land y \in ℋ) \to (T \circ U) (y) = T (U (y))$
7	2 6	sylan	$⊢ (U \in HrmOp \land y \in ℋ) \to (T \circ U) (y) = T (U (y))$
8	7	oveq2d	$⊢ (U \in HrmOp \land y \in ℋ) \to x \cdot_{ih} (T \circ U) (y) = x \cdot_{ih} T (U (y))$
9	8	ad2ant2l	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T \circ U) (y) = x \cdot_{ih} T (U (y))$
10		simpll	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to T \in HrmOp$
11		simprl	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \in ℋ$
12	2	ffvelrnda	$⊢ (U \in HrmOp \land y \in ℋ) \to U (y) \in ℋ$
13	12	ad2ant2l	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to U (y) \in ℋ$
14		hmop	$⊢ (T \in HrmOp \land x \in ℋ \land U (y) \in ℋ) \to x \cdot_{ih} T (U (y)) = T (x) \cdot_{ih} U (y)$
15	10 11 13 14	syl3anc	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} T (U (y)) = T (x) \cdot_{ih} U (y)$
16		simplr	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to U \in HrmOp$
17	1	ffvelrnda	$⊢ (T \in HrmOp \land x \in ℋ) \to T (x) \in ℋ$
18	17	ad2ant2r	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to T (x) \in ℋ$
19		simprr	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to y \in ℋ$
20		hmop	$⊢ (U \in HrmOp \land T (x) \in ℋ \land y \in ℋ) \to T (x) \cdot_{ih} U (y) = U (T (x)) \cdot_{ih} y$
21	16 18 19 20	syl3anc	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} U (y) = U (T (x)) \cdot_{ih} y$
22	9 15 21	3eqtrd	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T \circ U) (y) = U (T (x)) \cdot_{ih} y$
23		fvco3	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to (U \circ T) (x) = U (T (x))$
24	1 23	sylan	$⊢ (T \in HrmOp \land x \in ℋ) \to (U \circ T) (x) = U (T (x))$
25	24	oveq1d	$⊢ (T \in HrmOp \land x \in ℋ) \to (U \circ T) (x) \cdot_{ih} y = U (T (x)) \cdot_{ih} y$
26	25	ad2ant2r	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to (U \circ T) (x) \cdot_{ih} y = U (T (x)) \cdot_{ih} y$
27	22 26	eqtr4d	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T \circ U) (y) = (U \circ T) (x) \cdot_{ih} y$
28	27	3adantl3	$⊢ ((T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T \circ U) (y) = (U \circ T) (x) \cdot_{ih} y$
29		fveq1	$⊢ T \circ U = U \circ T \to (T \circ U) (x) = (U \circ T) (x)$
30	29	oveq1d	$⊢ T \circ U = U \circ T \to (T \circ U) (x) \cdot_{ih} y = (U \circ T) (x) \cdot_{ih} y$
31	30	3ad2ant3	$⊢ (T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \to (T \circ U) (x) \cdot_{ih} y = (U \circ T) (x) \cdot_{ih} y$
32	31	adantr	$⊢ ((T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \land (x \in ℋ \land y \in ℋ)) \to (T \circ U) (x) \cdot_{ih} y = (U \circ T) (x) \cdot_{ih} y$
33	28 32	eqtr4d	$⊢ ((T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T \circ U) (y) = (T \circ U) (x) \cdot_{ih} y$
34	33	ralrimivva	$⊢ (T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \to \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} (T \circ U) (y) = (T \circ U) (x) \cdot_{ih} y$
35		elhmop	$⊢ T \circ U \in HrmOp \leftrightarrow ((T \circ U) : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} (T \circ U) (y) = (T \circ U) (x) \cdot_{ih} y)$
36	5 34 35	sylanbrc	$⊢ (T \in HrmOp \land U \in HrmOp \land T \circ U = U \circ T) \to T \circ U \in HrmOp$

Metamath Proof Explorer

Theorem hmopco

Proof