# Metamath Proof Explorer

## Theorem lnophmlem1

Description: Lemma for lnophmi . (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 lnophmlem.1 ${⊢}{A}\in ℋ$
2 lnophmlem.2 ${⊢}{B}\in ℋ$
3 lnophmlem.3 ${⊢}{T}\in \mathrm{LinOp}$
4 lnophmlem.4 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ$
5 id ${⊢}{x}={A}\to {x}={A}$
6 fveq2 ${⊢}{x}={A}\to {T}\left({x}\right)={T}\left({A}\right)$
7 5 6 oveq12d ${⊢}{x}={A}\to {x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)={A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)$
8 7 eleq1d ${⊢}{x}={A}\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ↔{A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)\in ℝ\right)$
9 8 rspcv ${⊢}{A}\in ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)\in ℝ\right)$
10 1 4 9 mp2 ${⊢}{A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)\in ℝ$