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 𝐴 ) ) ) ) )