Metamath Proof Explorer

Theorem normlem7tALT

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses normlem7t.1 ⊢ 𝐴 ∈ ℋ
normlem7t.2 ⊢ 𝐵 ∈ ℋ
Assertion normlem7tALT ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) → ( ( ( ∗ ‘ 𝑆 ) · ( 𝐴 ·ih 𝐵 ) ) + ( 𝑆 · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 normlem7t.1 ⊢ 𝐴 ∈ ℋ
2 normlem7t.2 ⊢ 𝐵 ∈ ℋ
3 fveq2 ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ∗ ‘ 𝑆 ) = ( ∗ ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) )
4 3 oveq1d ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( ∗ ‘ 𝑆 ) · ( 𝐴 ·ih 𝐵 ) ) = ( ( ∗ ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) · ( 𝐴 ·ih 𝐵 ) ) )
5 oveq1 ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( 𝑆 · ( 𝐵 ·ih 𝐴 ) ) = ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) · ( 𝐵 ·ih 𝐴 ) ) )
6 4 5 oveq12d ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( ( ∗ ‘ 𝑆 ) · ( 𝐴 ·ih 𝐵 ) ) + ( 𝑆 · ( 𝐵 ·ih 𝐴 ) ) ) = ( ( ( ∗ ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) · ( 𝐵 ·ih 𝐴 ) ) ) )
7 6 breq1d ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐴 ·ih 𝐵 ) ) + ( 𝑆 · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) ↔ ( ( ( ∗ ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) ) )
8 eleq1 ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( 𝑆 ∈ ℂ ↔ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ∈ ℂ ) )
9 fveq2 ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( abs ‘ 𝑆 ) = ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) )
10 9 eqeq1d ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( abs ‘ 𝑆 ) = 1 ↔ ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) = 1 ) )
11 8 10 anbi12d ⊢ ( 𝑆 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) ↔ ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ∈ ℂ ∧ ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) = 1 ) ) )
12 eleq1 ⊢ ( 1 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( 1 ∈ ℂ ↔ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ∈ ℂ ) )
13 fveq2 ⊢ ( 1 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( abs ‘ 1 ) = ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) )
14 13 eqeq1d ⊢ ( 1 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( abs ‘ 1 ) = 1 ↔ ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) = 1 ) )
15 12 14 anbi12d ⊢ ( 1 = if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) → ( ( 1 ∈ ℂ ∧ ( abs ‘ 1 ) = 1 ) ↔ ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ∈ ℂ ∧ ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) = 1 ) ) )
16 ax-1cn ⊢ 1 ∈ ℂ
17 abs1 ⊢ ( abs ‘ 1 ) = 1
18 16 17 pm3.2i ⊢ ( 1 ∈ ℂ ∧ ( abs ‘ 1 ) = 1 )
19 11 15 18 elimhyp ⊢ ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ∈ ℂ ∧ ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) = 1 )
20 19 simpli ⊢ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ∈ ℂ
21 19 simpri ⊢ ( abs ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) = 1
22 20 1 2 21 normlem7 ⊢ ( ( ( ∗ ‘ if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) ) · ( 𝐴 ·ih 𝐵 ) ) + ( if ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) , 𝑆 , 1 ) · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
23 7 22 dedth ⊢ ( ( 𝑆 ∈ ℂ ∧ ( abs ‘ 𝑆 ) = 1 ) → ( ( ( ∗ ‘ 𝑆 ) · ( 𝐴 ·ih 𝐵 ) ) + ( 𝑆 · ( 𝐵 ·ih 𝐴 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) · ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )