Metamath Proof Explorer

Theorem lnopmul

Description: Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopmul ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⋅ ℎ T ⁡ B

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
2 lnopl ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ 0 ℎ ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ T ⁡ B + ℎ T ⁡ 0 ℎ
3 1 2 mpanr2 ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ T ⁡ B + ℎ T ⁡ 0 ℎ
4 3 3impa ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ T ⁡ B + ℎ T ⁡ 0 ℎ
5 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
6 ax-hvaddid ⊢ A ⋅ ℎ B ∈ ℋ → A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ B
7 5 6 syl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ B
8 7 3adant1 ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ B
9 8 fveq2d ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = T ⁡ A ⋅ ℎ B
10 lnop0 ⊢ T ∈ LinOp → T ⁡ 0 ℎ = 0 ℎ
11 10 oveq2d ⊢ T ∈ LinOp → A ⋅ ℎ T ⁡ B + ℎ T ⁡ 0 ℎ = A ⋅ ℎ T ⁡ B + ℎ 0 ℎ
12 11 3ad2ant1 ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ T ⁡ B + ℎ T ⁡ 0 ℎ = A ⋅ ℎ T ⁡ B + ℎ 0 ℎ
13 lnopf ⊢ T ∈ LinOp → T : ℋ ⟶ ℋ
14 13 ffvelrnda ⊢ T ∈ LinOp ∧ B ∈ ℋ → T ⁡ B ∈ ℋ
15 hvmulcl ⊢ A ∈ ℂ ∧ T ⁡ B ∈ ℋ → A ⋅ ℎ T ⁡ B ∈ ℋ
16 14 15 sylan2 ⊢ A ∈ ℂ ∧ T ∈ LinOp ∧ B ∈ ℋ → A ⋅ ℎ T ⁡ B ∈ ℋ
17 16 3impb ⊢ A ∈ ℂ ∧ T ∈ LinOp ∧ B ∈ ℋ → A ⋅ ℎ T ⁡ B ∈ ℋ
18 17 3com12 ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ T ⁡ B ∈ ℋ
19 ax-hvaddid ⊢ A ⋅ ℎ T ⁡ B ∈ ℋ → A ⋅ ℎ T ⁡ B + ℎ 0 ℎ = A ⋅ ℎ T ⁡ B
20 18 19 syl ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ T ⁡ B + ℎ 0 ℎ = A ⋅ ℎ T ⁡ B
21 12 20 eqtrd ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ T ⁡ B + ℎ T ⁡ 0 ℎ = A ⋅ ℎ T ⁡ B
22 4 9 21 3eqtr3d ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⋅ ℎ T ⁡ B