Theorem lnophmlem1

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

	Ref	Expression
Hypotheses	lnophmlem.1	$$⊢A\in \mathscr{H}$$
	lnophmlem.2	$$⊢B\in \mathscr{H}$$
	lnophmlem.3	$$⊢T\in \mathrm{LinOp}$$
	lnophmlem.4	$$⊢\forall x\in \mathscr{H}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 \mathscr{H}$$
2		lnophmlem.2	$$⊢B\in \mathscr{H}$$
3		lnophmlem.3	$$⊢T\in \mathrm{LinOp}$$
4		lnophmlem.4	$$⊢\forall x\in \mathscr{H}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 ℝ\leftrightarrow A{\cdot }_{\mathrm{ih}}T\left(A\right)\in ℝ\right)$$
9	8	rspcv	$$⊢A\in \mathscr{H}\to \left(\forall x\in \mathscr{H}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 ℝ$$