Metamath Proof Explorer

Theorem normlem0

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

Ref Expression
Hypotheses normlem1.1 
|- S e. CC
normlem1.2 
|- F e. ~H
normlem1.3 
|- G e. ~H
Assertion normlem0 
|- ( ( F -h ( S .h G ) ) .ih ( F -h ( S .h G ) ) ) = ( ( ( F .ih F ) + ( -u ( * ` S ) x. ( F .ih G ) ) ) + ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) 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 1 3 hvmulcli 
 |-  ( S .h G ) e. ~H
5 2 4 hvsubvali 
 |-  ( F -h ( S .h G ) ) = ( F +h ( -u 1 .h ( S .h G ) ) )
6 1 mulm1i 
 |-  ( -u 1 x. S ) = -u S
7 6 oveq1i 
 |-  ( ( -u 1 x. S ) .h G ) = ( -u S .h G )
8 neg1cn 
 |-  -u 1 e. CC
9 8 1 3 hvmulassi 
 |-  ( ( -u 1 x. S ) .h G ) = ( -u 1 .h ( S .h G ) )
10 7 9 eqtr3i 
 |-  ( -u S .h G ) = ( -u 1 .h ( S .h G ) )
11 10 oveq2i 
 |-  ( F +h ( -u S .h G ) ) = ( F +h ( -u 1 .h ( S .h G ) ) )
12 5 11 eqtr4i 
 |-  ( F -h ( S .h G ) ) = ( F +h ( -u S .h G ) )
13 12 12 oveq12i 
 |-  ( ( F -h ( S .h G ) ) .ih ( F -h ( S .h G ) ) ) = ( ( F +h ( -u S .h G ) ) .ih ( F +h ( -u S .h G ) ) )
14 1 negcli 
 |-  -u S e. CC
15 14 3 hvmulcli 
 |-  ( -u S .h G ) e. ~H
16 2 15 hvaddcli 
 |-  ( F +h ( -u S .h G ) ) e. ~H
17 ax-his2 
 |-  ( ( F e. ~H /\ ( -u S .h G ) e. ~H /\ ( F +h ( -u S .h G ) ) e. ~H ) -> ( ( F +h ( -u S .h G ) ) .ih ( F +h ( -u S .h G ) ) ) = ( ( F .ih ( F +h ( -u S .h G ) ) ) + ( ( -u S .h G ) .ih ( F +h ( -u S .h G ) ) ) ) )
18 2 15 16 17 mp3an 
 |-  ( ( F +h ( -u S .h G ) ) .ih ( F +h ( -u S .h G ) ) ) = ( ( F .ih ( F +h ( -u S .h G ) ) ) + ( ( -u S .h G ) .ih ( F +h ( -u S .h G ) ) ) )
19 his7 
 |-  ( ( F e. ~H /\ F e. ~H /\ ( -u S .h G ) e. ~H ) -> ( F .ih ( F +h ( -u S .h G ) ) ) = ( ( F .ih F ) + ( F .ih ( -u S .h G ) ) ) )
20 2 2 15 19 mp3an 
 |-  ( F .ih ( F +h ( -u S .h G ) ) ) = ( ( F .ih F ) + ( F .ih ( -u S .h G ) ) )
21 his5 
 |-  ( ( -u S e. CC /\ F e. ~H /\ G e. ~H ) -> ( F .ih ( -u S .h G ) ) = ( ( * ` -u S ) x. ( F .ih G ) ) )
22 14 2 3 21 mp3an 
 |-  ( F .ih ( -u S .h G ) ) = ( ( * ` -u S ) x. ( F .ih G ) )
23 1 cjnegi 
 |-  ( * ` -u S ) = -u ( * ` S )
24 23 oveq1i 
 |-  ( ( * ` -u S ) x. ( F .ih G ) ) = ( -u ( * ` S ) x. ( F .ih G ) )
25 22 24 eqtri 
 |-  ( F .ih ( -u S .h G ) ) = ( -u ( * ` S ) x. ( F .ih G ) )
26 25 oveq2i 
 |-  ( ( F .ih F ) + ( F .ih ( -u S .h G ) ) ) = ( ( F .ih F ) + ( -u ( * ` S ) x. ( F .ih G ) ) )
27 20 26 eqtri 
 |-  ( F .ih ( F +h ( -u S .h G ) ) ) = ( ( F .ih F ) + ( -u ( * ` S ) x. ( F .ih G ) ) )
28 ax-his3 
 |-  ( ( -u S e. CC /\ G e. ~H /\ ( F +h ( -u S .h G ) ) e. ~H ) -> ( ( -u S .h G ) .ih ( F +h ( -u S .h G ) ) ) = ( -u S x. ( G .ih ( F +h ( -u S .h G ) ) ) ) )
29 14 3 16 28 mp3an 
 |-  ( ( -u S .h G ) .ih ( F +h ( -u S .h G ) ) ) = ( -u S x. ( G .ih ( F +h ( -u S .h G ) ) ) )
30 his7 
 |-  ( ( G e. ~H /\ F e. ~H /\ ( -u S .h G ) e. ~H ) -> ( G .ih ( F +h ( -u S .h G ) ) ) = ( ( G .ih F ) + ( G .ih ( -u S .h G ) ) ) )
31 3 2 15 30 mp3an 
 |-  ( G .ih ( F +h ( -u S .h G ) ) ) = ( ( G .ih F ) + ( G .ih ( -u S .h G ) ) )
32 his5 
 |-  ( ( -u S e. CC /\ G e. ~H /\ G e. ~H ) -> ( G .ih ( -u S .h G ) ) = ( ( * ` -u S ) x. ( G .ih G ) ) )
33 14 3 3 32 mp3an 
 |-  ( G .ih ( -u S .h G ) ) = ( ( * ` -u S ) x. ( G .ih G ) )
34 33 oveq2i 
 |-  ( ( G .ih F ) + ( G .ih ( -u S .h G ) ) ) = ( ( G .ih F ) + ( ( * ` -u S ) x. ( G .ih G ) ) )
35 31 34 eqtri 
 |-  ( G .ih ( F +h ( -u S .h G ) ) ) = ( ( G .ih F ) + ( ( * ` -u S ) x. ( G .ih G ) ) )
36 35 oveq2i 
 |-  ( -u S x. ( G .ih ( F +h ( -u S .h G ) ) ) ) = ( -u S x. ( ( G .ih F ) + ( ( * ` -u S ) x. ( G .ih G ) ) ) )
37 3 2 hicli 
 |-  ( G .ih F ) e. CC
38 14 cjcli 
 |-  ( * ` -u S ) e. CC
39 3 3 hicli 
 |-  ( G .ih G ) e. CC
40 38 39 mulcli 
 |-  ( ( * ` -u S ) x. ( G .ih G ) ) e. CC
41 14 37 40 adddii 
 |-  ( -u S x. ( ( G .ih F ) + ( ( * ` -u S ) x. ( G .ih G ) ) ) ) = ( ( -u S x. ( G .ih F ) ) + ( -u S x. ( ( * ` -u S ) x. ( G .ih G ) ) ) )
42 14 38 39 mulassi 
 |-  ( ( -u S x. ( * ` -u S ) ) x. ( G .ih G ) ) = ( -u S x. ( ( * ` -u S ) x. ( G .ih G ) ) )
43 23 oveq2i 
 |-  ( -u S x. ( * ` -u S ) ) = ( -u S x. -u ( * ` S ) )
44 1 cjcli 
 |-  ( * ` S ) e. CC
45 1 44 mul2negi 
 |-  ( -u S x. -u ( * ` S ) ) = ( S x. ( * ` S ) )
46 43 45 eqtri 
 |-  ( -u S x. ( * ` -u S ) ) = ( S x. ( * ` S ) )
47 46 oveq1i 
 |-  ( ( -u S x. ( * ` -u S ) ) x. ( G .ih G ) ) = ( ( S x. ( * ` S ) ) x. ( G .ih G ) )
48 42 47 eqtr3i 
 |-  ( -u S x. ( ( * ` -u S ) x. ( G .ih G ) ) ) = ( ( S x. ( * ` S ) ) x. ( G .ih G ) )
49 48 oveq2i 
 |-  ( ( -u S x. ( G .ih F ) ) + ( -u S x. ( ( * ` -u S ) x. ( G .ih G ) ) ) ) = ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) x. ( G .ih G ) ) )
50 41 49 eqtri 
 |-  ( -u S x. ( ( G .ih F ) + ( ( * ` -u S ) x. ( G .ih G ) ) ) ) = ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) x. ( G .ih G ) ) )
51 29 36 50 3eqtri 
 |-  ( ( -u S .h G ) .ih ( F +h ( -u S .h G ) ) ) = ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) x. ( G .ih G ) ) )
52 27 51 oveq12i 
 |-  ( ( F .ih ( F +h ( -u S .h G ) ) ) + ( ( -u S .h G ) .ih ( F +h ( -u S .h G ) ) ) ) = ( ( ( F .ih F ) + ( -u ( * ` S ) x. ( F .ih G ) ) ) + ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) x. ( G .ih G ) ) ) )
53 13 18 52 3eqtri 
 |-  ( ( F -h ( S .h G ) ) .ih ( F -h ( S .h G ) ) ) = ( ( ( F .ih F ) + ( -u ( * ` S ) x. ( F .ih G ) ) ) + ( ( -u S x. ( G .ih F ) ) + ( ( S x. ( * ` S ) ) x. ( G .ih G ) ) ) )