Metamath Proof Explorer

Theorem normlem9

Description: Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005) (New usage is discouraged.)

Ref Expression
Hypotheses normlem8.1 
|- A e. ~H
normlem8.2 
|- B e. ~H
normlem8.3 
|- C e. ~H
normlem8.4 
|- D e. ~H
Assertion normlem9 
|- ( ( A -h B ) .ih ( C -h D ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) - ( ( A .ih D ) + ( B .ih C ) ) )

Proof

Step Hyp Ref Expression
1 normlem8.1 
 |-  A e. ~H
2 normlem8.2 
 |-  B e. ~H
3 normlem8.3 
 |-  C e. ~H
4 normlem8.4 
 |-  D e. ~H
5 1 2 hvsubvali 
 |-  ( A -h B ) = ( A +h ( -u 1 .h B ) )
6 3 4 hvsubvali 
 |-  ( C -h D ) = ( C +h ( -u 1 .h D ) )
7 5 6 oveq12i 
 |-  ( ( A -h B ) .ih ( C -h D ) ) = ( ( A +h ( -u 1 .h B ) ) .ih ( C +h ( -u 1 .h D ) ) )
8 neg1cn 
 |-  -u 1 e. CC
9 8 2 hvmulcli 
 |-  ( -u 1 .h B ) e. ~H
10 8 4 hvmulcli 
 |-  ( -u 1 .h D ) e. ~H
11 1 9 3 10 normlem8 
 |-  ( ( A +h ( -u 1 .h B ) ) .ih ( C +h ( -u 1 .h D ) ) ) = ( ( ( A .ih C ) + ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) ) + ( ( A .ih ( -u 1 .h D ) ) + ( ( -u 1 .h B ) .ih C ) ) )
12 ax-his3 
 |-  ( ( -u 1 e. CC /\ B e. ~H /\ ( -u 1 .h D ) e. ~H ) -> ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) = ( -u 1 x. ( B .ih ( -u 1 .h D ) ) ) )
13 8 2 10 12 mp3an 
 |-  ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) = ( -u 1 x. ( B .ih ( -u 1 .h D ) ) )
14 his5 
 |-  ( ( -u 1 e. CC /\ B e. ~H /\ D e. ~H ) -> ( B .ih ( -u 1 .h D ) ) = ( ( * ` -u 1 ) x. ( B .ih D ) ) )
15 8 2 4 14 mp3an 
 |-  ( B .ih ( -u 1 .h D ) ) = ( ( * ` -u 1 ) x. ( B .ih D ) )
16 15 oveq2i 
 |-  ( -u 1 x. ( B .ih ( -u 1 .h D ) ) ) = ( -u 1 x. ( ( * ` -u 1 ) x. ( B .ih D ) ) )
17 neg1rr 
 |-  -u 1 e. RR
18 cjre 
 |-  ( -u 1 e. RR -> ( * ` -u 1 ) = -u 1 )
19 17 18 ax-mp 
 |-  ( * ` -u 1 ) = -u 1
20 19 oveq2i 
 |-  ( -u 1 x. ( * ` -u 1 ) ) = ( -u 1 x. -u 1 )
21 ax-1cn 
 |-  1 e. CC
22 21 21 mul2negi 
 |-  ( -u 1 x. -u 1 ) = ( 1 x. 1 )
23 21 mulid2i 
 |-  ( 1 x. 1 ) = 1
24 20 22 23 3eqtri 
 |-  ( -u 1 x. ( * ` -u 1 ) ) = 1
25 24 oveq1i 
 |-  ( ( -u 1 x. ( * ` -u 1 ) ) x. ( B .ih D ) ) = ( 1 x. ( B .ih D ) )
26 8 cjcli 
 |-  ( * ` -u 1 ) e. CC
27 2 4 hicli 
 |-  ( B .ih D ) e. CC
28 8 26 27 mulassi 
 |-  ( ( -u 1 x. ( * ` -u 1 ) ) x. ( B .ih D ) ) = ( -u 1 x. ( ( * ` -u 1 ) x. ( B .ih D ) ) )
29 27 mulid2i 
 |-  ( 1 x. ( B .ih D ) ) = ( B .ih D )
30 25 28 29 3eqtr3i 
 |-  ( -u 1 x. ( ( * ` -u 1 ) x. ( B .ih D ) ) ) = ( B .ih D )
31 13 16 30 3eqtri 
 |-  ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) = ( B .ih D )
32 31 oveq2i 
 |-  ( ( A .ih C ) + ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) ) = ( ( A .ih C ) + ( B .ih D ) )
33 his5 
 |-  ( ( -u 1 e. CC /\ A e. ~H /\ D e. ~H ) -> ( A .ih ( -u 1 .h D ) ) = ( ( * ` -u 1 ) x. ( A .ih D ) ) )
34 8 1 4 33 mp3an 
 |-  ( A .ih ( -u 1 .h D ) ) = ( ( * ` -u 1 ) x. ( A .ih D ) )
35 19 oveq1i 
 |-  ( ( * ` -u 1 ) x. ( A .ih D ) ) = ( -u 1 x. ( A .ih D ) )
36 1 4 hicli 
 |-  ( A .ih D ) e. CC
37 36 mulm1i 
 |-  ( -u 1 x. ( A .ih D ) ) = -u ( A .ih D )
38 34 35 37 3eqtri 
 |-  ( A .ih ( -u 1 .h D ) ) = -u ( A .ih D )
39 ax-his3 
 |-  ( ( -u 1 e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) .ih C ) = ( -u 1 x. ( B .ih C ) ) )
40 8 2 3 39 mp3an 
 |-  ( ( -u 1 .h B ) .ih C ) = ( -u 1 x. ( B .ih C ) )
41 2 3 hicli 
 |-  ( B .ih C ) e. CC
42 41 mulm1i 
 |-  ( -u 1 x. ( B .ih C ) ) = -u ( B .ih C )
43 40 42 eqtri 
 |-  ( ( -u 1 .h B ) .ih C ) = -u ( B .ih C )
44 38 43 oveq12i 
 |-  ( ( A .ih ( -u 1 .h D ) ) + ( ( -u 1 .h B ) .ih C ) ) = ( -u ( A .ih D ) + -u ( B .ih C ) )
45 36 41 negdii 
 |-  -u ( ( A .ih D ) + ( B .ih C ) ) = ( -u ( A .ih D ) + -u ( B .ih C ) )
46 44 45 eqtr4i 
 |-  ( ( A .ih ( -u 1 .h D ) ) + ( ( -u 1 .h B ) .ih C ) ) = -u ( ( A .ih D ) + ( B .ih C ) )
47 32 46 oveq12i 
 |-  ( ( ( A .ih C ) + ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) ) + ( ( A .ih ( -u 1 .h D ) ) + ( ( -u 1 .h B ) .ih C ) ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) + -u ( ( A .ih D ) + ( B .ih C ) ) )
48 1 3 hicli 
 |-  ( A .ih C ) e. CC
49 48 27 addcli 
 |-  ( ( A .ih C ) + ( B .ih D ) ) e. CC
50 36 41 addcli 
 |-  ( ( A .ih D ) + ( B .ih C ) ) e. CC
51 49 50 negsubi 
 |-  ( ( ( A .ih C ) + ( B .ih D ) ) + -u ( ( A .ih D ) + ( B .ih C ) ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) - ( ( A .ih D ) + ( B .ih C ) ) )
52 47 51 eqtri 
 |-  ( ( ( A .ih C ) + ( ( -u 1 .h B ) .ih ( -u 1 .h D ) ) ) + ( ( A .ih ( -u 1 .h D ) ) + ( ( -u 1 .h B ) .ih C ) ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) - ( ( A .ih D ) + ( B .ih C ) ) )
53 7 11 52 3eqtri 
 |-  ( ( A -h B ) .ih ( C -h D ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) - ( ( A .ih D ) + ( B .ih C ) ) )