Metamath Proof Explorer


Theorem lnfnaddi

Description: Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 โŠข ๐‘‡ โˆˆ LinFn
Assertion lnfnaddi ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ๐ด +โ„Ž ๐ต ) ) = ( ( ๐‘‡ โ€˜ ๐ด ) + ( ๐‘‡ โ€˜ ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 lnfnl.1 โŠข ๐‘‡ โˆˆ LinFn
2 ax-1cn โŠข 1 โˆˆ โ„‚
3 1 lnfnli โŠข ( ( 1 โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ๐ต ) ) = ( ( 1 ยท ( ๐‘‡ โ€˜ ๐ด ) ) + ( ๐‘‡ โ€˜ ๐ต ) ) )
4 2 3 mp3an1 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ๐ต ) ) = ( ( 1 ยท ( ๐‘‡ โ€˜ ๐ด ) ) + ( ๐‘‡ โ€˜ ๐ต ) ) )
5 ax-hvmulid โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( 1 ยทโ„Ž ๐ด ) = ๐ด )
6 5 fvoveq1d โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐‘‡ โ€˜ ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ๐ต ) ) = ( ๐‘‡ โ€˜ ( ๐ด +โ„Ž ๐ต ) ) )
7 6 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( 1 ยทโ„Ž ๐ด ) +โ„Ž ๐ต ) ) = ( ๐‘‡ โ€˜ ( ๐ด +โ„Ž ๐ต ) ) )
8 1 lnfnfi โŠข ๐‘‡ : โ„‹ โŸถ โ„‚
9 8 ffvelrni โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐‘‡ โ€˜ ๐ด ) โˆˆ โ„‚ )
10 9 mulid2d โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( 1 ยท ( ๐‘‡ โ€˜ ๐ด ) ) = ( ๐‘‡ โ€˜ ๐ด ) )
11 10 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( 1 ยท ( ๐‘‡ โ€˜ ๐ด ) ) = ( ๐‘‡ โ€˜ ๐ด ) )
12 11 oveq1d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( 1 ยท ( ๐‘‡ โ€˜ ๐ด ) ) + ( ๐‘‡ โ€˜ ๐ต ) ) = ( ( ๐‘‡ โ€˜ ๐ด ) + ( ๐‘‡ โ€˜ ๐ต ) ) )
13 4 7 12 3eqtr3d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ๐ด +โ„Ž ๐ต ) ) = ( ( ๐‘‡ โ€˜ ๐ด ) + ( ๐‘‡ โ€˜ ๐ต ) ) )