Metamath Proof Explorer

Theorem normlem3

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 21-Aug-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 ) ) )
normlem3.5 
|- A = ( G .ih G )
normlem3.6 
|- C = ( F .ih F )
normlem3.7 
|- R e. RR
Assertion normlem3 
|- ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C ) = ( ( ( 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 normlem2.4 
 |-  B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
5 normlem3.5 
 |-  A = ( G .ih G )
6 normlem3.6 
 |-  C = ( F .ih F )
7 normlem3.7 
 |-  R e. RR
8 3 3 hicli 
 |-  ( G .ih G ) e. CC
9 5 8 eqeltri 
 |-  A e. CC
10 7 recni 
 |-  R e. CC
11 10 sqcli 
 |-  ( R ^ 2 ) e. CC
12 9 11 mulcli 
 |-  ( A x. ( R ^ 2 ) ) e. CC
13 1 2 3 4 normlem2 
 |-  B e. RR
14 13 recni 
 |-  B e. CC
15 14 10 mulcli 
 |-  ( B x. R ) e. CC
16 12 15 addcomi 
 |-  ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) = ( ( B x. R ) + ( A x. ( R ^ 2 ) ) )
17 1 cjcli 
 |-  ( * ` S ) e. CC
18 2 3 hicli 
 |-  ( F .ih G ) e. CC
19 17 18 mulcli 
 |-  ( ( * ` S ) x. ( F .ih G ) ) e. CC
20 3 2 hicli 
 |-  ( G .ih F ) e. CC
21 1 20 mulcli 
 |-  ( S x. ( G .ih F ) ) e. CC
22 19 21 addcli 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. CC
23 22 10 mulneg1i 
 |-  ( -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. R ) = -u ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. R )
24 4 oveq1i 
 |-  ( B x. R ) = ( -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. R )
25 22 10 mulneg2i 
 |-  ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. -u R ) = -u ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. R )
26 23 24 25 3eqtr4i 
 |-  ( B x. R ) = ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. -u R )
27 10 negcli 
 |-  -u R e. CC
28 19 21 27 adddiri 
 |-  ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) x. -u R ) = ( ( ( ( * ` S ) x. ( F .ih G ) ) x. -u R ) + ( ( S x. ( G .ih F ) ) x. -u R ) )
29 17 18 27 mul32i 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) x. -u R ) = ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) )
30 1 20 27 mul32i 
 |-  ( ( S x. ( G .ih F ) ) x. -u R ) = ( ( S x. -u R ) x. ( G .ih F ) )
31 29 30 oveq12i 
 |-  ( ( ( ( * ` S ) x. ( F .ih G ) ) x. -u R ) + ( ( S x. ( G .ih F ) ) x. -u R ) ) = ( ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) + ( ( S x. -u R ) x. ( G .ih F ) ) )
32 26 28 31 3eqtri 
 |-  ( B x. R ) = ( ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) + ( ( S x. -u R ) x. ( G .ih F ) ) )
33 5 oveq2i 
 |-  ( ( R ^ 2 ) x. A ) = ( ( R ^ 2 ) x. ( G .ih G ) )
34 11 9 33 mulcomli 
 |-  ( A x. ( R ^ 2 ) ) = ( ( R ^ 2 ) x. ( G .ih G ) )
35 32 34 oveq12i 
 |-  ( ( B x. R ) + ( A x. ( R ^ 2 ) ) ) = ( ( ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) + ( ( S x. -u R ) x. ( G .ih F ) ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) )
36 17 27 mulcli 
 |-  ( ( * ` S ) x. -u R ) e. CC
37 36 18 mulcli 
 |-  ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) e. CC
38 1 27 mulcli 
 |-  ( S x. -u R ) e. CC
39 38 20 mulcli 
 |-  ( ( S x. -u R ) x. ( G .ih F ) ) e. CC
40 11 8 mulcli 
 |-  ( ( R ^ 2 ) x. ( G .ih G ) ) e. CC
41 37 39 40 addassi 
 |-  ( ( ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) + ( ( S x. -u R ) x. ( G .ih F ) ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) = ( ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
42 16 35 41 3eqtri 
 |-  ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) = ( ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
43 6 42 oveq12i 
 |-  ( C + ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) ) = ( ( 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 ) ) ) ) )
44 12 15 addcli 
 |-  ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) e. CC
45 2 2 hicli 
 |-  ( F .ih F ) e. CC
46 6 45 eqeltri 
 |-  C e. CC
47 44 46 addcomi 
 |-  ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C ) = ( C + ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) )
48 39 40 addcli 
 |-  ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) e. CC
49 45 37 48 addassi 
 |-  ( ( ( 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 ) ) ) ) = ( ( 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 ) ) ) ) )
50 43 47 49 3eqtr4i 
 |-  ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C ) = ( ( ( 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 ) ) ) )