Metamath Proof Explorer

Theorem lnfnl

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

Ref Expression
Assertion lnfnl ${⊢}\left(\left({T}\in \mathrm{LinFn}\wedge {A}\in ℂ\right)\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$

Proof

Step Hyp Ref Expression
1 ellnfn ${⊢}{T}\in \mathrm{LinFn}↔\left({T}:ℋ⟶ℂ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={x}{T}\left({y}\right)+{T}\left({z}\right)\right)$
2 1 simprbi ${⊢}{T}\in \mathrm{LinFn}\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={x}{T}\left({y}\right)+{T}\left({z}\right)$
3 oveq1 ${⊢}{x}={A}\to {x}{\cdot }_{ℎ}{y}={A}{\cdot }_{ℎ}{y}$
4 3 fvoveq1d ${⊢}{x}={A}\to {T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={T}\left(\left({A}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
5 oveq1 ${⊢}{x}={A}\to {x}{T}\left({y}\right)={A}{T}\left({y}\right)$
6 5 oveq1d ${⊢}{x}={A}\to {x}{T}\left({y}\right)+{T}\left({z}\right)={A}{T}\left({y}\right)+{T}\left({z}\right)$
7 4 6 eqeq12d ${⊢}{x}={A}\to \left({T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={x}{T}\left({y}\right)+{T}\left({z}\right)↔{T}\left(\left({A}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{T}\left({y}\right)+{T}\left({z}\right)\right)$
8 oveq2 ${⊢}{y}={B}\to {A}{\cdot }_{ℎ}{y}={A}{\cdot }_{ℎ}{B}$
9 8 fvoveq1d ${⊢}{y}={B}\to {T}\left(\left({A}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{z}\right)$
10 fveq2 ${⊢}{y}={B}\to {T}\left({y}\right)={T}\left({B}\right)$
11 10 oveq2d ${⊢}{y}={B}\to {A}{T}\left({y}\right)={A}{T}\left({B}\right)$
12 11 oveq1d ${⊢}{y}={B}\to {A}{T}\left({y}\right)+{T}\left({z}\right)={A}{T}\left({B}\right)+{T}\left({z}\right)$
13 9 12 eqeq12d ${⊢}{y}={B}\to \left({T}\left(\left({A}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={A}{T}\left({y}\right)+{T}\left({z}\right)↔{T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{z}\right)={A}{T}\left({B}\right)+{T}\left({z}\right)\right)$
14 oveq2 ${⊢}{z}={C}\to \left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{z}=\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}$
15 14 fveq2d ${⊢}{z}={C}\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{z}\right)={T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)$
16 fveq2 ${⊢}{z}={C}\to {T}\left({z}\right)={T}\left({C}\right)$
17 16 oveq2d ${⊢}{z}={C}\to {A}{T}\left({B}\right)+{T}\left({z}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$
18 15 17 eqeq12d ${⊢}{z}={C}\to \left({T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{z}\right)={A}{T}\left({B}\right)+{T}\left({z}\right)↔{T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)\right)$
19 7 13 18 rspc3v ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left(\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={x}{T}\left({y}\right)+{T}\left({z}\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)\right)$
20 2 19 syl5 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({T}\in \mathrm{LinFn}\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)\right)$
21 20 3expb ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to \left({T}\in \mathrm{LinFn}\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)\right)$
22 21 impcom ${⊢}\left({T}\in \mathrm{LinFn}\wedge \left({A}\in ℂ\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$
23 22 anassrs ${⊢}\left(\left({T}\in \mathrm{LinFn}\wedge {A}\in ℂ\right)\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$