# 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 ( 𝑇 ∈ LinFn ↔ ( 𝑇 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )

### Proof

Step Hyp Ref Expression
1 fveq1 ( 𝑡 = 𝑇 → ( 𝑡 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) )
2 fveq1 ( 𝑡 = 𝑇 → ( 𝑡𝑦 ) = ( 𝑇𝑦 ) )
3 2 oveq2d ( 𝑡 = 𝑇 → ( 𝑥 · ( 𝑡𝑦 ) ) = ( 𝑥 · ( 𝑇𝑦 ) ) )
4 fveq1 ( 𝑡 = 𝑇 → ( 𝑡𝑧 ) = ( 𝑇𝑧 ) )
5 3 4 oveq12d ( 𝑡 = 𝑇 → ( ( 𝑥 · ( 𝑡𝑦 ) ) + ( 𝑡𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) )
6 1 5 eqeq12d ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑡𝑦 ) ) + ( 𝑡𝑧 ) ) ↔ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )
7 6 ralbidv ( 𝑡 = 𝑇 → ( ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑡𝑦 ) ) + ( 𝑡𝑧 ) ) ↔ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )
8 7 2ralbidv ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑡𝑦 ) ) + ( 𝑡𝑧 ) ) ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )
9 df-lnfn LinFn = { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑡𝑦 ) ) + ( 𝑡𝑧 ) ) }
10 8 9 elrab2 ( 𝑇 ∈ LinFn ↔ ( 𝑇 ∈ ( ℂ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )
11 cnex ℂ ∈ V
12 ax-hilex ℋ ∈ V
13 11 12 elmap ( 𝑇 ∈ ( ℂ ↑m ℋ ) ↔ 𝑇 : ℋ ⟶ ℂ )
14 13 anbi1i ( ( 𝑇 ∈ ( ℂ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )
15 10 14 bitri ( 𝑇 ∈ LinFn ↔ ( 𝑇 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 · 𝑦 ) + 𝑧 ) ) = ( ( 𝑥 · ( 𝑇𝑦 ) ) + ( 𝑇𝑧 ) ) ) )