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