hmops

Description: The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hmops	$⊢ (T \in HrmOp \land U \in HrmOp) \to T +_{op} U \in HrmOp$

Proof

Step	Hyp	Ref	Expression
1		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
2		hmopf	$⊢ U \in HrmOp \to U : ℋ ⟶ ℋ$
3		hoaddcl	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T +_{op} U) : ℋ ⟶ ℋ$
4	1 2 3	syl2an	$⊢ (T \in HrmOp \land U \in HrmOp) \to (T +_{op} U) : ℋ ⟶ ℋ$
5		hmop	$⊢ (T \in HrmOp \land x \in ℋ \land y \in ℋ) \to x \cdot_{ih} T (y) = T (x) \cdot_{ih} y$
6	5	3expb	$⊢ (T \in HrmOp \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} T (y) = T (x) \cdot_{ih} y$
7		hmop	$⊢ (U \in HrmOp \land x \in ℋ \land y \in ℋ) \to x \cdot_{ih} U (y) = U (x) \cdot_{ih} y$
8	7	3expb	$⊢ (U \in HrmOp \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} U (y) = U (x) \cdot_{ih} y$
9	6 8	oveqan12d	$⊢ ((T \in HrmOp \land (x \in ℋ \land y \in ℋ)) \land (U \in HrmOp \land (x \in ℋ \land y \in ℋ))) \to (x \cdot_{ih} T (y)) + (x \cdot_{ih} U (y)) = (T (x) \cdot_{ih} y) + (U (x) \cdot_{ih} y)$
10	9	anandirs	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to (x \cdot_{ih} T (y)) + (x \cdot_{ih} U (y)) = (T (x) \cdot_{ih} y) + (U (x) \cdot_{ih} y)$
11	1 2	anim12i	$⊢ (T \in HrmOp \land U \in HrmOp) \to (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)$
12		hosval	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land y \in ℋ) \to (T +_{op} U) (y) = T (y) +_{ℎ} U (y)$
13	12	oveq2d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land y \in ℋ) \to x \cdot_{ih} (T +_{op} U) (y) = x \cdot_{ih} (T (y) +_{ℎ} U (y))$
14	13	3expa	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land y \in ℋ) \to x \cdot_{ih} (T +_{op} U) (y) = x \cdot_{ih} (T (y) +_{ℎ} U (y))$
15	14	adantrl	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T +_{op} U) (y) = x \cdot_{ih} (T (y) +_{ℎ} U (y))$
16		simprl	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to x \in ℋ$
17		ffvelcdm	$⊢ (T : ℋ ⟶ ℋ \land y \in ℋ) \to T (y) \in ℋ$
18	17	ad2ant2rl	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to T (y) \in ℋ$
19		ffvelcdm	$⊢ (U : ℋ ⟶ ℋ \land y \in ℋ) \to U (y) \in ℋ$
20	19	ad2ant2l	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to U (y) \in ℋ$
21		his7	$⊢ (x \in ℋ \land T (y) \in ℋ \land U (y) \in ℋ) \to x \cdot_{ih} (T (y) +_{ℎ} U (y)) = (x \cdot_{ih} T (y)) + (x \cdot_{ih} U (y))$
22	16 18 20 21	syl3anc	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T (y) +_{ℎ} U (y)) = (x \cdot_{ih} T (y)) + (x \cdot_{ih} U (y))$
23	15 22	eqtrd	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T +_{op} U) (y) = (x \cdot_{ih} T (y)) + (x \cdot_{ih} U (y))$
24	11 23	sylan	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T +_{op} U) (y) = (x \cdot_{ih} T (y)) + (x \cdot_{ih} U (y))$
25		hosval	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land x \in ℋ) \to (T +_{op} U) (x) = T (x) +_{ℎ} U (x)$
26	25	oveq1d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land x \in ℋ) \to (T +_{op} U) (x) \cdot_{ih} y = (T (x) +_{ℎ} U (x)) \cdot_{ih} y$
27	26	3expa	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (T +_{op} U) (x) \cdot_{ih} y = (T (x) +_{ℎ} U (x)) \cdot_{ih} y$
28	27	adantrr	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to (T +_{op} U) (x) \cdot_{ih} y = (T (x) +_{ℎ} U (x)) \cdot_{ih} y$
29		ffvelcdm	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to T (x) \in ℋ$
30	29	ad2ant2r	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to T (x) \in ℋ$
31		ffvelcdm	$⊢ (U : ℋ ⟶ ℋ \land x \in ℋ) \to U (x) \in ℋ$
32	31	ad2ant2lr	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to U (x) \in ℋ$
33		simprr	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to y \in ℋ$
34		ax-his2	$⊢ (T (x) \in ℋ \land U (x) \in ℋ \land y \in ℋ) \to (T (x) +_{ℎ} U (x)) \cdot_{ih} y = (T (x) \cdot_{ih} y) + (U (x) \cdot_{ih} y)$
35	30 32 33 34	syl3anc	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to (T (x) +_{ℎ} U (x)) \cdot_{ih} y = (T (x) \cdot_{ih} y) + (U (x) \cdot_{ih} y)$
36	28 35	eqtrd	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land (x \in ℋ \land y \in ℋ)) \to (T +_{op} U) (x) \cdot_{ih} y = (T (x) \cdot_{ih} y) + (U (x) \cdot_{ih} y)$
37	11 36	sylan	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to (T +_{op} U) (x) \cdot_{ih} y = (T (x) \cdot_{ih} y) + (U (x) \cdot_{ih} y)$
38	10 24 37	3eqtr4d	$⊢ ((T \in HrmOp \land U \in HrmOp) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} (T +_{op} U) (y) = (T +_{op} U) (x) \cdot_{ih} y$
39	38	ralrimivva	$⊢ (T \in HrmOp \land U \in HrmOp) \to \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} (T +_{op} U) (y) = (T +_{op} U) (x) \cdot_{ih} y$
40		elhmop	$⊢ T +_{op} U \in HrmOp \leftrightarrow ((T +_{op} U) : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} (T +_{op} U) (y) = (T +_{op} U) (x) \cdot_{ih} y)$
41	4 39 40	sylanbrc	$⊢ (T \in HrmOp \land U \in HrmOp) \to T +_{op} U \in HrmOp$

Metamath Proof Explorer

Theorem hmops

Proof