# 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`
` |-  ( ( A .ih C ) + ( B .ih D ) ) e. CC`
` |-  ( ( A .ih D ) + ( B .ih C ) ) e. CC`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( A -h B ) .ih ( C -h D ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) - ( ( A .ih D ) + ( B .ih C ) ) )`