Metamath Proof Explorer

Theorem lnopl

Description: Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ellnop ⊢ T ∈ LinOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
2 1 simprbi ⊢ T ∈ LinOp → ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z
3 oveq1 ⊢ x = A → x ⋅ ℎ y = A ⋅ ℎ y
4 3 fvoveq1d ⊢ x = A → T ⁡ x ⋅ ℎ y + ℎ z = T ⁡ A ⋅ ℎ y + ℎ z
5 oveq1 ⊢ x = A → x ⋅ ℎ T ⁡ y = A ⋅ ℎ T ⁡ y
6 5 oveq1d ⊢ x = A → x ⋅ ℎ T ⁡ y + ℎ T ⁡ z = A ⋅ ℎ T ⁡ y + ℎ T ⁡ z
7 4 6 eqeq12d ⊢ x = A → T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z ↔ T ⁡ A ⋅ ℎ y + ℎ z = A ⋅ ℎ T ⁡ y + ℎ T ⁡ z
8 oveq2 ⊢ y = B → A ⋅ ℎ y = A ⋅ ℎ B
9 8 fvoveq1d ⊢ y = B → T ⁡ A ⋅ ℎ y + ℎ z = T ⁡ A ⋅ ℎ B + ℎ z
10 fveq2 ⊢ y = B → T ⁡ y = T ⁡ B
11 10 oveq2d ⊢ y = B → A ⋅ ℎ T ⁡ y = A ⋅ ℎ T ⁡ B
12 11 oveq1d ⊢ y = B → A ⋅ ℎ T ⁡ y + ℎ T ⁡ z = A ⋅ ℎ T ⁡ B + ℎ T ⁡ z
13 9 12 eqeq12d ⊢ y = B → T ⁡ A ⋅ ℎ y + ℎ z = A ⋅ ℎ T ⁡ y + ℎ T ⁡ z ↔ T ⁡ A ⋅ ℎ B + ℎ z = A ⋅ ℎ T ⁡ B + ℎ T ⁡ z
14 oveq2 ⊢ z = C → A ⋅ ℎ B + ℎ z = A ⋅ ℎ B + ℎ C
15 14 fveq2d ⊢ z = C → T ⁡ A ⋅ ℎ B + ℎ z = T ⁡ A ⋅ ℎ B + ℎ C
16 fveq2 ⊢ z = C → T ⁡ z = T ⁡ C
17 16 oveq2d ⊢ z = C → A ⋅ ℎ T ⁡ B + ℎ T ⁡ z = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C
18 15 17 eqeq12d ⊢ z = C → T ⁡ A ⋅ ℎ B + ℎ z = A ⋅ ℎ T ⁡ B + ℎ T ⁡ z ↔ T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C
19 7 13 18 rspc3v ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⋅ ℎ T ⁡ y + ℎ T ⁡ z → T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C
20 2 19 syl5 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ∈ LinOp → T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C
21 20 3expb ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ∈ LinOp → T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C
22 21 impcom ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C
23 22 anassrs ⊢ T ∈ LinOp ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C