Metamath Proof Explorer

Theorem ellnfn

Description: Property defining a linear functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion ellnfn ⊢ T ∈ LinFn ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ t = T → t ⁡ x ⋅ ℎ y + ℎ z = T ⁡ x ⋅ ℎ y + ℎ z
2 fveq1 ⊢ t = T → t ⁡ y = T ⁡ y
3 2 oveq2d ⊢ t = T → x ⁢ t ⁡ y = x ⁢ T ⁡ y
4 fveq1 ⊢ t = T → t ⁡ z = T ⁡ z
5 3 4 oveq12d ⊢ t = T → x ⁢ t ⁡ y + t ⁡ z = x ⁢ T ⁡ y + T ⁡ z
6 1 5 eqeq12d ⊢ t = T → t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z ↔ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z
7 6 ralbidv ⊢ t = T → ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z ↔ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z
8 7 2ralbidv ⊢ t = T → ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z ↔ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z
9 df-lnfn ⊢ LinFn = t ∈ ℂ ℋ | ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ t ⁡ x ⋅ ℎ y + ℎ z = x ⁢ t ⁡ y + t ⁡ z
10 8 9 elrab2 ⊢ T ∈ LinFn ↔ T ∈ ℂ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z
11 cnex ⊢ ℂ ∈ V
12 ax-hilex ⊢ ℋ ∈ V
13 11 12 elmap ⊢ T ∈ ℂ ℋ ↔ T : ℋ ⟶ ℂ
14 13 anbi1i ⊢ T ∈ ℂ ℋ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z
15 10 14 bitri ⊢ T ∈ LinFn ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ℎ y + ℎ z = x ⁢ T ⁡ y + T ⁡ z