# Metamath Proof Explorer

## Theorem hmoplin

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

Ref Expression
Assertion hmoplin $⊢ T ∈ HrmOp → T ∈ LinOp$

### Proof

Step Hyp Ref Expression
1 hmopf $⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ$
2 simplll $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ∈ HrmOp$
3 hvmulcl $⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ y ∈ ℋ$
4 hvaddcl $⊢ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ$
5 3 4 sylan $⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ$
6 5 adantll $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ$
7 6 adantr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ$
8 simpr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → w ∈ ℋ$
9 hmop $⊢ T ∈ HrmOp ∧ x ⋅ ℎ y + ℎ z ∈ ℋ ∧ w ∈ ℋ → x ⋅ ℎ y + ℎ z ⋅ ih T ⁡ w = T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w$
10 9 eqcomd $⊢ T ∈ HrmOp ∧ x ⋅ ℎ y + ℎ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ y + ℎ z ⋅ ih T ⁡ w$
11 2 7 8 10 syl3anc $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ y + ℎ z ⋅ ih T ⁡ w$
12 simprl $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ → x ∈ ℂ$
13 12 ad2antrr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ∈ ℂ$
14 simprr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ → y ∈ ℋ$
15 14 ad2antrr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → y ∈ ℋ$
16 simplr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → z ∈ ℋ$
17 1 ffvelrnda $⊢ T ∈ HrmOp ∧ w ∈ ℋ → T ⁡ w ∈ ℋ$
18 17 adantlr $⊢ T ∈ HrmOp ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ w ∈ ℋ$
19 18 adantllr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ w ∈ ℋ$
20 hiassdi $⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ T ⁡ w ∈ ℋ → x ⋅ ℎ y + ℎ z ⋅ ih T ⁡ w = x ⁢ y ⋅ ih T ⁡ w + z ⋅ ih T ⁡ w$
21 13 15 16 19 20 syl22anc $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ⋅ ℎ y + ℎ z ⋅ ih T ⁡ w = x ⁢ y ⋅ ih T ⁡ w + z ⋅ ih T ⁡ w$
22 1 ffvelrnda $⊢ T ∈ HrmOp ∧ y ∈ ℋ → T ⁡ y ∈ ℋ$
23 22 adantrl $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ$
24 23 ad2antrr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ y ∈ ℋ$
25 1 ffvelrnda $⊢ T ∈ HrmOp ∧ z ∈ ℋ → T ⁡ z ∈ ℋ$
26 25 adantr $⊢ T ∈ HrmOp ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ z ∈ ℋ$
27 26 adantllr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ z ∈ ℋ$
28 hiassdi $⊢ x ∈ ℂ ∧ T ⁡ y ∈ ℋ ∧ T ⁡ z ∈ ℋ ∧ w ∈ ℋ → x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w = x ⁢ T ⁡ y ⋅ ih w + T ⁡ z ⋅ ih w$
29 13 24 27 8 28 syl22anc $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w = x ⁢ T ⁡ y ⋅ ih w + T ⁡ z ⋅ ih w$
30 hmop $⊢ T ∈ HrmOp ∧ y ∈ ℋ ∧ w ∈ ℋ → y ⋅ ih T ⁡ w = T ⁡ y ⋅ ih w$
31 30 eqcomd $⊢ T ∈ HrmOp ∧ y ∈ ℋ ∧ w ∈ ℋ → T ⁡ y ⋅ ih w = y ⋅ ih T ⁡ w$
32 31 3expa $⊢ T ∈ HrmOp ∧ y ∈ ℋ ∧ w ∈ ℋ → T ⁡ y ⋅ ih w = y ⋅ ih T ⁡ w$
33 32 oveq2d $⊢ T ∈ HrmOp ∧ y ∈ ℋ ∧ w ∈ ℋ → x ⁢ T ⁡ y ⋅ ih w = x ⁢ y ⋅ ih T ⁡ w$
34 33 adantlrl $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ w ∈ ℋ → x ⁢ T ⁡ y ⋅ ih w = x ⁢ y ⋅ ih T ⁡ w$
35 34 adantlr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ⁢ T ⁡ y ⋅ ih w = x ⁢ y ⋅ ih T ⁡ w$
36 hmop $⊢ T ∈ HrmOp ∧ z ∈ ℋ ∧ w ∈ ℋ → z ⋅ ih T ⁡ w = T ⁡ z ⋅ ih w$
37 36 eqcomd $⊢ T ∈ HrmOp ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ z ⋅ ih w = z ⋅ ih T ⁡ w$
38 37 3expa $⊢ T ∈ HrmOp ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ z ⋅ ih w = z ⋅ ih T ⁡ w$
39 38 adantllr $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ z ⋅ ih w = z ⋅ ih T ⁡ w$
40 35 39 oveq12d $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ⁢ T ⁡ y ⋅ ih w + T ⁡ z ⋅ ih w = x ⁢ y ⋅ ih T ⁡ w + z ⋅ ih T ⁡ w$
41 29 40 eqtr2d $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → x ⁢ y ⋅ ih T ⁡ w + z ⋅ ih T ⁡ w = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w$
42 11 21 41 3eqtrd $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ ∧ w ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w$
43 42 ralrimiva $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → ∀ w ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w$
44 ffvelrn $⊢ T : ℋ ⟶ ℋ ∧ x ⋅ ℎ y + ℎ z ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z ∈ ℋ$
45 5 44 sylan2 $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z ∈ ℋ$
46 45 anassrs $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z ∈ ℋ$
47 ffvelrn $⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ$
48 hvmulcl $⊢ x ∈ ℂ ∧ T ⁡ y ∈ ℋ → x ⋅ ℎ T ⁡ y ∈ ℋ$
49 47 48 sylan2 $⊢ x ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → x ⋅ ℎ T ⁡ y ∈ ℋ$
50 49 an12s $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ T ⁡ y ∈ ℋ$
51 50 adantr $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ T ⁡ y ∈ ℋ$
52 ffvelrn $⊢ T : ℋ ⟶ ℋ ∧ z ∈ ℋ → T ⁡ z ∈ ℋ$
53 52 adantlr $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → T ⁡ z ∈ ℋ$
54 hvaddcl $⊢ x ⋅ ℎ T ⁡ y ∈ ℋ ∧ T ⁡ z ∈ ℋ → x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ∈ ℋ$
55 51 53 54 syl2anc $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ∈ ℋ$
56 hial2eq $⊢ T ⁡ x ⋅ ℎ y + ℎ z ∈ ℋ ∧ x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ∈ ℋ → ∀ w ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w ↔ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
57 46 55 56 syl2anc $⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → ∀ w ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w ↔ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
58 1 57 sylanl1 $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → ∀ w ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z ⋅ ih w = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ⋅ ih w ↔ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
59 43 58 mpbid $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
60 59 ralrimiva $⊢ T ∈ HrmOp ∧ x ∈ ℂ ∧ y ∈ ℋ → ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
61 60 ralrimivva $⊢ T ∈ HrmOp → ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
62 ellnop $⊢ T ∈ LinOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z$
63 1 61 62 sylanbrc $⊢ T ∈ HrmOp → T ∈ LinOp$