Theorem lnfnmul

Description: Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	lnfnmul	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 ·ℎ 𝐵 ) ) )
2		fveq1	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝐵 ) = ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) )
3	2	oveq2d	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) )
4	1 3	eqeq12d	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) ↔ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) ) )
5	4	imbi2d	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) ) ) )
6		0lnfn	⊢ ( ℋ × { 0 } ) ∈ LinFn
7	6	elimel	⊢ if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
8	7	lnfnmuli	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) )
9	5 8	dedth	⊢ ( 𝑇 ∈ LinFn → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) ) )
10	9	3impib	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )