Metamath Proof Explorer

Theorem normlem1

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

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

Proof

Step Hyp Ref Expression
1 normlem1.1 
 |-  S e. CC
2 normlem1.2 
 |-  F e. ~H
3 normlem1.3 
 |-  G e. ~H
4 normlem1.4 
 |-  R e. RR
5 normlem1.5 
 |-  ( abs ` S ) = 1
6 4 recni 
 |-  R e. CC
7 1 6 mulcli 
 |-  ( S x. R ) e. CC
8 7 2 3 normlem0 
 |-  ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) = ( ( ( F .ih F ) + ( -u ( * ` ( S x. R ) ) x. ( F .ih G ) ) ) + ( ( -u ( S x. R ) x. ( G .ih F ) ) + ( ( ( S x. R ) x. ( * ` ( S x. R ) ) ) x. ( G .ih G ) ) ) )
9 1 6 cjmuli 
 |-  ( * ` ( S x. R ) ) = ( ( * ` S ) x. ( * ` R ) )
10 6 cjrebi 
 |-  ( R e. RR <-> ( * ` R ) = R )
11 4 10 mpbi 
 |-  ( * ` R ) = R
12 11 oveq2i 
 |-  ( ( * ` S ) x. ( * ` R ) ) = ( ( * ` S ) x. R )
13 9 12 eqtri 
 |-  ( * ` ( S x. R ) ) = ( ( * ` S ) x. R )
14 13 negeqi 
 |-  -u ( * ` ( S x. R ) ) = -u ( ( * ` S ) x. R )
15 1 cjcli 
 |-  ( * ` S ) e. CC
16 15 6 mulneg2i 
 |-  ( ( * ` S ) x. -u R ) = -u ( ( * ` S ) x. R )
17 14 16 eqtr4i 
 |-  -u ( * ` ( S x. R ) ) = ( ( * ` S ) x. -u R )
18 17 oveq1i 
 |-  ( -u ( * ` ( S x. R ) ) x. ( F .ih G ) ) = ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) )
19 18 oveq2i 
 |-  ( ( F .ih F ) + ( -u ( * ` ( S x. R ) ) x. ( F .ih G ) ) ) = ( ( F .ih F ) + ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) )
20 1 6 mulneg2i 
 |-  ( S x. -u R ) = -u ( S x. R )
21 20 eqcomi 
 |-  -u ( S x. R ) = ( S x. -u R )
22 21 oveq1i 
 |-  ( -u ( S x. R ) x. ( G .ih F ) ) = ( ( S x. -u R ) x. ( G .ih F ) )
23 9 oveq2i 
 |-  ( ( S x. R ) x. ( * ` ( S x. R ) ) ) = ( ( S x. R ) x. ( ( * ` S ) x. ( * ` R ) ) )
24 6 cjcli 
 |-  ( * ` R ) e. CC
25 1 6 15 24 mul4i 
 |-  ( ( S x. R ) x. ( ( * ` S ) x. ( * ` R ) ) ) = ( ( S x. ( * ` S ) ) x. ( R x. ( * ` R ) ) )
26 5 oveq1i 
 |-  ( ( abs ` S ) ^ 2 ) = ( 1 ^ 2 )
27 1 absvalsqi 
 |-  ( ( abs ` S ) ^ 2 ) = ( S x. ( * ` S ) )
28 sq1 
 |-  ( 1 ^ 2 ) = 1
29 26 27 28 3eqtr3i 
 |-  ( S x. ( * ` S ) ) = 1
30 11 oveq2i 
 |-  ( R x. ( * ` R ) ) = ( R x. R )
31 29 30 oveq12i 
 |-  ( ( S x. ( * ` S ) ) x. ( R x. ( * ` R ) ) ) = ( 1 x. ( R x. R ) )
32 6 6 mulcli 
 |-  ( R x. R ) e. CC
33 32 mulid2i 
 |-  ( 1 x. ( R x. R ) ) = ( R x. R )
34 31 33 eqtri 
 |-  ( ( S x. ( * ` S ) ) x. ( R x. ( * ` R ) ) ) = ( R x. R )
35 25 34 eqtri 
 |-  ( ( S x. R ) x. ( ( * ` S ) x. ( * ` R ) ) ) = ( R x. R )
36 23 35 eqtri 
 |-  ( ( S x. R ) x. ( * ` ( S x. R ) ) ) = ( R x. R )
37 6 sqvali 
 |-  ( R ^ 2 ) = ( R x. R )
38 36 37 eqtr4i 
 |-  ( ( S x. R ) x. ( * ` ( S x. R ) ) ) = ( R ^ 2 )
39 38 oveq1i 
 |-  ( ( ( S x. R ) x. ( * ` ( S x. R ) ) ) x. ( G .ih G ) ) = ( ( R ^ 2 ) x. ( G .ih G ) )
40 22 39 oveq12i 
 |-  ( ( -u ( S x. R ) x. ( G .ih F ) ) + ( ( ( S x. R ) x. ( * ` ( S x. R ) ) ) x. ( G .ih G ) ) ) = ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) )
41 19 40 oveq12i 
 |-  ( ( ( F .ih F ) + ( -u ( * ` ( S x. R ) ) x. ( F .ih G ) ) ) + ( ( -u ( S x. R ) x. ( G .ih F ) ) + ( ( ( S x. R ) x. ( * ` ( S x. R ) ) ) x. ( G .ih G ) ) ) ) = ( ( ( F .ih F ) + ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
42 8 41 eqtri 
 |-  ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) = ( ( ( F .ih F ) + ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )