# Metamath Proof Explorer

## Theorem lnopunilem2

Description: Lemma for lnopunii . (Contributed by NM, 12-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses lnopunilem.1 ${⊢}{T}\in \mathrm{LinOp}$
lnopunilem.2 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)$
lnopunilem.3 ${⊢}{A}\in ℋ$
lnopunilem.4 ${⊢}{B}\in ℋ$
Assertion lnopunilem2 ${⊢}{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}$

### Proof

Step Hyp Ref Expression
1 lnopunilem.1 ${⊢}{T}\in \mathrm{LinOp}$
2 lnopunilem.2 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)$
3 lnopunilem.3 ${⊢}{A}\in ℋ$
4 lnopunilem.4 ${⊢}{B}\in ℋ$
5 fvoveq1 ${⊢}{y}=if\left({y}\in ℂ,{y},0\right)\to \Re \left({y}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left(if\left({y}\in ℂ,{y},0\right)\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)$
6 fvoveq1 ${⊢}{y}=if\left({y}\in ℂ,{y},0\right)\to \Re \left({y}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)=\Re \left(if\left({y}\in ℂ,{y},0\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)$
7 5 6 eqeq12d ${⊢}{y}=if\left({y}\in ℂ,{y},0\right)\to \left(\Re \left({y}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left({y}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)↔\Re \left(if\left({y}\in ℂ,{y},0\right)\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left(if\left({y}\in ℂ,{y},0\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)\right)$
8 0cn ${⊢}0\in ℂ$
9 8 elimel ${⊢}if\left({y}\in ℂ,{y},0\right)\in ℂ$
10 1 2 3 4 9 lnopunilem1 ${⊢}\Re \left(if\left({y}\in ℂ,{y},0\right)\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left(if\left({y}\in ℂ,{y},0\right)\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)$
11 7 10 dedth ${⊢}{y}\in ℂ\to \Re \left({y}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left({y}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)$
12 11 rgen ${⊢}\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}\Re \left({y}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left({y}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)$
13 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
14 13 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
15 3 14 ax-mp ${⊢}{T}\left({A}\right)\in ℋ$
16 13 ffvelrni ${⊢}{B}\in ℋ\to {T}\left({B}\right)\in ℋ$
17 4 16 ax-mp ${⊢}{T}\left({B}\right)\in ℋ$
18 15 17 hicli ${⊢}{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\in ℂ$
19 3 4 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
20 recan ${⊢}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{B}\in ℂ\right)\to \left(\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}\Re \left({y}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left({y}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}\right)$
21 18 19 20 mp2an ${⊢}\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}\Re \left({y}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left({y}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}$
22 12 21 mpbi ${⊢}{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}$