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 
|- A e. ~H
normlem7t.2 
|- B e. ~H
Assertion normlem7tALT 
|- ( ( S e. CC /\ ( abs ` S ) = 1 ) -> ( ( ( * ` S ) x. ( A .ih B ) ) + ( S x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 normlem7t.1 
 |-  A e. ~H
2 normlem7t.2 
 |-  B e. ~H
3 fveq2 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( * ` S ) = ( * ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) )
4 3 oveq1d 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( * ` S ) x. ( A .ih B ) ) = ( ( * ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) x. ( A .ih B ) ) )
5 oveq1 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( S x. ( B .ih A ) ) = ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) x. ( B .ih A ) ) )
6 4 5 oveq12d 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( ( * ` S ) x. ( A .ih B ) ) + ( S x. ( B .ih A ) ) ) = ( ( ( * ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) x. ( A .ih B ) ) + ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) x. ( B .ih A ) ) ) )
7 6 breq1d 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( ( ( * ` S ) x. ( A .ih B ) ) + ( S x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) <-> ( ( ( * ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) x. ( A .ih B ) ) + ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) ) )
8 eleq1 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( S e. CC <-> if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) e. CC ) )
9 fveq2 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( abs ` S ) = ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) )
10 9 eqeq1d 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( abs ` S ) = 1 <-> ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) = 1 ) )
11 8 10 anbi12d 
 |-  ( S = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( S e. CC /\ ( abs ` S ) = 1 ) <-> ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) e. CC /\ ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) = 1 ) ) )
12 eleq1 
 |-  ( 1 = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( 1 e. CC <-> if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) e. CC ) )
13 fveq2 
 |-  ( 1 = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( abs ` 1 ) = ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) )
14 13 eqeq1d 
 |-  ( 1 = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( abs ` 1 ) = 1 <-> ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) = 1 ) )
15 12 14 anbi12d 
 |-  ( 1 = if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) -> ( ( 1 e. CC /\ ( abs ` 1 ) = 1 ) <-> ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) e. CC /\ ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) = 1 ) ) )
16 ax-1cn 
 |-  1 e. CC
17 abs1 
 |-  ( abs ` 1 ) = 1
18 16 17 pm3.2i 
 |-  ( 1 e. CC /\ ( abs ` 1 ) = 1 )
19 11 15 18 elimhyp 
 |-  ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) e. CC /\ ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) = 1 )
20 19 simpli 
 |-  if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) e. CC
21 19 simpri 
 |-  ( abs ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) = 1
22 20 1 2 21 normlem7 
 |-  ( ( ( * ` if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) ) x. ( A .ih B ) ) + ( if ( ( S e. CC /\ ( abs ` S ) = 1 ) , S , 1 ) x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) )
23 7 22 dedth 
 |-  ( ( S e. CC /\ ( abs ` S ) = 1 ) -> ( ( ( * ` S ) x. ( A .ih B ) ) + ( S x. ( B .ih A ) ) ) <_ ( 2 x. ( ( sqrt ` ( B .ih B ) ) x. ( sqrt ` ( A .ih A ) ) ) ) )