Metamath Proof Explorer

Theorem lnfnl

Description: Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfnl ⊢ T ∈ LinFn ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C

Proof

Step Hyp Ref Expression
1 ellnfn ⊢ T ∈ LinFn ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z
2 1 simprbi ⊢ T ∈ LinFn → ∀ 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 ∈ LinFn → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C
21 20 3expb ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ∈ LinFn → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C
22 21 impcom ⊢ T ∈ LinFn ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C
23 22 anassrs ⊢ T ∈ LinFn ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C