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