This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℋ
lnophmlem.2 ⊢ B ∈ ℋ
lnophmlem.3 ⊢ T ∈ LinOp
lnophmlem.4 ⊢ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ
Assertion lnophmlem1 ⊢ A ⋅ ih T ⁡ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 lnophmlem.1 ⊢ A ∈ ℋ
2 lnophmlem.2 ⊢ B ∈ ℋ
3 lnophmlem.3 ⊢ T ∈ LinOp
4 lnophmlem.4 ⊢ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ
5 id ⊢ x = A → x = A
6 fveq2 ⊢ x = A → T ⁡ x = T ⁡ A
7 5 6 oveq12d ⊢ x = A → x ⋅ ih T ⁡ x = A ⋅ ih T ⁡ A
8 7 eleq1d ⊢ x = A → x ⋅ ih T ⁡ x ∈ ℝ ↔ A ⋅ ih T ⁡ A ∈ ℝ
9 8 rspcv ⊢ A ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ → A ⋅ ih T ⁡ A ∈ ℝ
10 1 4 9 mp2 ⊢ A ⋅ ih T ⁡ A ∈ ℝ