Metamath Proof Explorer

Theorem normlem2

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

Ref Expression
Hypotheses normlem1.1 
|- S e. CC
normlem1.2 
|- F e. ~H
normlem1.3 
|- G e. ~H
normlem2.4 
|- B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
Assertion normlem2 
|- B e. RR

Proof

Step Hyp Ref Expression
1 normlem1.1 
 |-  S e. CC
2 normlem1.2 
 |-  F e. ~H
3 normlem1.3 
 |-  G e. ~H
4 normlem2.4 
 |-  B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
5 1 cjcli 
 |-  ( * ` S ) e. CC
6 2 3 hicli 
 |-  ( F .ih G ) e. CC
7 5 6 mulcli 
 |-  ( ( * ` S ) x. ( F .ih G ) ) e. CC
8 3 2 hicli 
 |-  ( G .ih F ) e. CC
9 1 8 mulcli 
 |-  ( S x. ( G .ih F ) ) e. CC
10 7 9 cjaddi 
 |-  ( * ` ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) = ( ( * ` ( ( * ` S ) x. ( F .ih G ) ) ) + ( * ` ( S x. ( G .ih F ) ) ) )
11 1 cjcji 
 |-  ( * ` ( * ` S ) ) = S
12 11 eqcomi 
 |-  S = ( * ` ( * ` S ) )
13 3 2 his1i 
 |-  ( G .ih F ) = ( * ` ( F .ih G ) )
14 12 13 oveq12i 
 |-  ( S x. ( G .ih F ) ) = ( ( * ` ( * ` S ) ) x. ( * ` ( F .ih G ) ) )
15 5 6 cjmuli 
 |-  ( * ` ( ( * ` S ) x. ( F .ih G ) ) ) = ( ( * ` ( * ` S ) ) x. ( * ` ( F .ih G ) ) )
16 14 15 eqtr4i 
 |-  ( S x. ( G .ih F ) ) = ( * ` ( ( * ` S ) x. ( F .ih G ) ) )
17 2 3 his1i 
 |-  ( F .ih G ) = ( * ` ( G .ih F ) )
18 17 oveq2i 
 |-  ( ( * ` S ) x. ( F .ih G ) ) = ( ( * ` S ) x. ( * ` ( G .ih F ) ) )
19 1 8 cjmuli 
 |-  ( * ` ( S x. ( G .ih F ) ) ) = ( ( * ` S ) x. ( * ` ( G .ih F ) ) )
20 18 19 eqtr4i 
 |-  ( ( * ` S ) x. ( F .ih G ) ) = ( * ` ( S x. ( G .ih F ) ) )
21 16 20 oveq12i 
 |-  ( ( S x. ( G .ih F ) ) + ( ( * ` S ) x. ( F .ih G ) ) ) = ( ( * ` ( ( * ` S ) x. ( F .ih G ) ) ) + ( * ` ( S x. ( G .ih F ) ) ) )
22 10 21 eqtr4i 
 |-  ( * ` ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) = ( ( S x. ( G .ih F ) ) + ( ( * ` S ) x. ( F .ih G ) ) )
23 7 9 addcomi 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) = ( ( S x. ( G .ih F ) ) + ( ( * ` S ) x. ( F .ih G ) ) )
24 22 23 eqtr4i 
 |-  ( * ` ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) = ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
25 7 9 addcli 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. CC
26 25 cjrebi 
 |-  ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR <-> ( * ` ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) = ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) )
27 24 26 mpbir 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR
28 27 renegcli 
 |-  -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR
29 4 28 eqeltri 
 |-  B e. RR