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 TLinFn
Assertion lnfnaddi ABTA+B=TA+TB

Proof

Step Hyp Ref Expression
1 lnfnl.1 TLinFn
2 ax-1cn 1
3 1 lnfnli 1ABT1A+B=1TA+TB
4 2 3 mp3an1 ABT1A+B=1TA+TB
5 ax-hvmulid A1A=A
6 5 fvoveq1d AT1A+B=TA+B
7 6 adantr ABT1A+B=TA+B
8 1 lnfnfi T:
9 8 ffvelrni ATA
10 9 mulid2d A1TA=TA
11 10 adantr AB1TA=TA
12 11 oveq1d AB1TA+TB=TA+TB
13 4 7 12 3eqtr3d ABTA+B=TA+TB