Metamath Proof Explorer


Theorem lnopaddi

Description: Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

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

Proof

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