hmoplin

Description: A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hmoplin	$⊢ T \in HrmOp \to T \in LinOp$

Proof

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

Metamath Proof Explorer

Theorem hmoplin

Proof