Metamath Proof Explorer

Theorem lnopunilem2

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

Ref Expression
Hypotheses lnopunilem.1 ⊢ 𝑇 ∈ LinOp
lnopunilem.2 ⊢ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 )
lnopunilem.3 ⊢ 𝐴 ∈ ℋ
lnopunilem.4 ⊢ 𝐵 ∈ ℋ
Assertion lnopunilem2 ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐴 ·ih 𝐵 )

Proof

Step Hyp Ref Expression
1 lnopunilem.1 ⊢ 𝑇 ∈ LinOp
2 lnopunilem.2 ⊢ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 )
3 lnopunilem.3 ⊢ 𝐴 ∈ ℋ
4 lnopunilem.4 ⊢ 𝐵 ∈ ℋ
5 fvoveq1 ⊢ ( 𝑦 = if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) → ( ℜ ‘ ( 𝑦 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) )
6 fvoveq1 ⊢ ( 𝑦 = if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) → ( ℜ ‘ ( 𝑦 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ℜ ‘ ( if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) · ( 𝐴 ·ih 𝐵 ) ) ) )
7 5 6 eqeq12d ⊢ ( 𝑦 = if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) → ( ( ℜ ‘ ( 𝑦 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝑦 · ( 𝐴 ·ih 𝐵 ) ) ) ↔ ( ℜ ‘ ( if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) · ( 𝐴 ·ih 𝐵 ) ) ) ) )
8 0cn ⊢ 0 ∈ ℂ
9 8 elimel ⊢ if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) ∈ ℂ
10 1 2 3 4 9 lnopunilem1 ⊢ ( ℜ ‘ ( if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( if ( 𝑦 ∈ ℂ , 𝑦 , 0 ) · ( 𝐴 ·ih 𝐵 ) ) )
11 7 10 dedth ⊢ ( 𝑦 ∈ ℂ → ( ℜ ‘ ( 𝑦 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝑦 · ( 𝐴 ·ih 𝐵 ) ) ) )
12 11 rgen ⊢ ∀ 𝑦 ∈ ℂ ( ℜ ‘ ( 𝑦 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝑦 · ( 𝐴 ·ih 𝐵 ) ) )
13 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
14 13 ffvelrni ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
15 3 14 ax-mp ⊢ ( 𝑇 ‘ 𝐴 ) ∈ ℋ
16 13 ffvelrni ⊢ ( 𝐵 ∈ ℋ → ( 𝑇 ‘ 𝐵 ) ∈ ℋ )
17 4 16 ax-mp ⊢ ( 𝑇 ‘ 𝐵 ) ∈ ℋ
18 15 17 hicli ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ∈ ℂ
19 3 4 hicli ⊢ ( 𝐴 ·ih 𝐵 ) ∈ ℂ
20 recan ⊢ ( ( ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ∈ ℂ ∧ ( 𝐴 ·ih 𝐵 ) ∈ ℂ ) → ( ∀ 𝑦 ∈ ℂ ( ℜ ‘ ( 𝑦 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝑦 · ( 𝐴 ·ih 𝐵 ) ) ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐴 ·ih 𝐵 ) ) )
21 18 19 20 mp2an ⊢ ( ∀ 𝑦 ∈ ℂ ( ℜ ‘ ( 𝑦 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝑦 · ( 𝐴 ·ih 𝐵 ) ) ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐴 ·ih 𝐵 ) )
22 12 21 mpbi ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐴 ·ih 𝐵 )