Metamath Proof Explorer

Theorem ellnfn

Description: Property defining a linear functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion 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)$

Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{t}={T}\to {t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
2 fveq1 ${⊢}{t}={T}\to {t}\left({y}\right)={T}\left({y}\right)$
3 2 oveq2d ${⊢}{t}={T}\to {x}{t}\left({y}\right)={x}{T}\left({y}\right)$
4 fveq1 ${⊢}{t}={T}\to {t}\left({z}\right)={T}\left({z}\right)$
5 3 4 oveq12d ${⊢}{t}={T}\to {x}{t}\left({y}\right)+{t}\left({z}\right)={x}{T}\left({y}\right)+{T}\left({z}\right)$
6 1 5 eqeq12d ${⊢}{t}={T}\to \left({t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={x}{t}\left({y}\right)+{t}\left({z}\right)↔{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={x}{T}\left({y}\right)+{T}\left({z}\right)\right)$
7 6 ralbidv ${⊢}{t}={T}\to \left(\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)↔\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)$
8 7 2ralbidv ${⊢}{t}={T}\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)↔\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)$
9 df-lnfn ${⊢}\mathrm{LinFn}=\left\{{t}\in \left({ℂ}^{ℋ}\right)|\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\}$
10 8 9 elrab2 ${⊢}{T}\in \mathrm{LinFn}↔\left({T}\in \left({ℂ}^{ℋ}\right)\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)$
11 cnex ${⊢}ℂ\in \mathrm{V}$
12 ax-hilex ${⊢}ℋ\in \mathrm{V}$
13 11 12 elmap ${⊢}{T}\in \left({ℂ}^{ℋ}\right)↔{T}:ℋ⟶ℂ$
14 13 anbi1i ${⊢}\left({T}\in \left({ℂ}^{ℋ}\right)\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)↔\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)$
15 10 14 bitri ${⊢}{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)$