Metamath Proof Explorer


Theorem lnopl

Description: Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopl T LinOp A B C T A B + C = A T B + T C

Proof

Step Hyp Ref Expression
1 ellnop T LinOp T : x y z T x y + z = x T y + T z
2 1 simprbi T LinOp x y z T x y + z = x T y + T z
3 oveq1 x = A x y = A y
4 3 fvoveq1d x = A T x y + z = T A y + z
5 oveq1 x = A x T y = A T y
6 5 oveq1d x = A x T y + T z = A T y + T z
7 4 6 eqeq12d x = A T x y + z = x T y + T z T A y + z = A T y + T z
8 oveq2 y = B A y = A B
9 8 fvoveq1d y = B T A y + z = T A B + z
10 fveq2 y = B T y = T B
11 10 oveq2d y = B A T y = A T B
12 11 oveq1d y = B A T y + T z = A T B + T z
13 9 12 eqeq12d y = B T A y + z = A T y + T z T A B + z = A T B + T z
14 oveq2 z = C A B + z = A B + C
15 14 fveq2d z = C T A B + z = T A B + C
16 fveq2 z = C T z = T C
17 16 oveq2d z = C A T B + T z = A T B + T C
18 15 17 eqeq12d z = C T A B + z = A T B + T z T A B + C = A T B + T C
19 7 13 18 rspc3v A B C x y z T x y + z = x T y + T z T A B + C = A T B + T C
20 2 19 syl5 A B C T LinOp T A B + C = A T B + T C
21 20 3expb A B C T LinOp T A B + C = A T B + T C
22 21 impcom T LinOp A B C T A B + C = A T B + T C
23 22 anassrs T LinOp A B C T A B + C = A T B + T C