Metamath Proof Explorer


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 โˆง ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ๐ด ยท ( ๐‘‡ โ€˜ ๐ต ) ) )