Theorem lnophmlem1

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

	Ref	Expression
Hypotheses	lnophmlem.1	⊢ 𝐴 ∈ ℋ
	lnophmlem.2	⊢ 𝐵 ∈ ℋ
	lnophmlem.3	⊢ 𝑇 ∈ LinOp
	lnophmlem.4	⊢ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ
Assertion	lnophmlem1	⊢ ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		lnophmlem.1	⊢ 𝐴 ∈ ℋ
2		lnophmlem.2	⊢ 𝐵 ∈ ℋ
3		lnophmlem.3	⊢ 𝑇 ∈ LinOp
4		lnophmlem.4	⊢ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ
5		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
6		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝐴 ) )
7	5 6	oveq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ↔ ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ) )
9	8	rspcv	⊢ ( 𝐴 ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ) )
10	1 4 9	mp2	⊢ ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ