Metamath Proof Explorer


Theorem lnopmulsubi

Description: Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lnopl.1 โŠข ๐‘‡ โˆˆ LinOp
2 hvmulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ )
3 1 lnopsubi โŠข ( ( ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐ด ยทโ„Ž ๐ต ) โˆ’โ„Ž ๐ถ ) ) = ( ( ๐‘‡ โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) โˆ’โ„Ž ( ๐‘‡ โ€˜ ๐ถ ) ) )
4 2 3 stoic3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐ด ยทโ„Ž ๐ต ) โˆ’โ„Ž ๐ถ ) ) = ( ( ๐‘‡ โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) โˆ’โ„Ž ( ๐‘‡ โ€˜ ๐ถ ) ) )
5 1 lnopmuli โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐ต ) ) )
6 5 3adant3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐ต ) ) )
7 6 oveq1d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) โˆ’โ„Ž ( ๐‘‡ โ€˜ ๐ถ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐ต ) ) โˆ’โ„Ž ( ๐‘‡ โ€˜ ๐ถ ) ) )
8 4 7 eqtrd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐ด ยทโ„Ž ๐ต ) โˆ’โ„Ž ๐ถ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐ต ) ) โˆ’โ„Ž ( ๐‘‡ โ€˜ ๐ถ ) ) )