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 โŠข ๐‘† โˆˆ โ„‚
normlem1.2 โŠข ๐น โˆˆ โ„‹
normlem1.3 โŠข ๐บ โˆˆ โ„‹
Assertion normlem0 ( ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) ยทih ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ( ๐น ยทih ๐น ) + ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) ) + ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) ) )

Proof

Step Hyp Ref Expression
1 normlem1.1 โŠข ๐‘† โˆˆ โ„‚
2 normlem1.2 โŠข ๐น โˆˆ โ„‹
3 normlem1.3 โŠข ๐บ โˆˆ โ„‹
4 1 3 hvmulcli โŠข ( ๐‘† ยทโ„Ž ๐บ ) โˆˆ โ„‹
5 2 4 hvsubvali โŠข ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) = ( ๐น +โ„Ž ( - 1 ยทโ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) )
6 1 mulm1i โŠข ( - 1 ยท ๐‘† ) = - ๐‘†
7 6 oveq1i โŠข ( ( - 1 ยท ๐‘† ) ยทโ„Ž ๐บ ) = ( - ๐‘† ยทโ„Ž ๐บ )
8 neg1cn โŠข - 1 โˆˆ โ„‚
9 8 1 3 hvmulassi โŠข ( ( - 1 ยท ๐‘† ) ยทโ„Ž ๐บ ) = ( - 1 ยทโ„Ž ( ๐‘† ยทโ„Ž ๐บ ) )
10 7 9 eqtr3i โŠข ( - ๐‘† ยทโ„Ž ๐บ ) = ( - 1 ยทโ„Ž ( ๐‘† ยทโ„Ž ๐บ ) )
11 10 oveq2i โŠข ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) = ( ๐น +โ„Ž ( - 1 ยทโ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) )
12 5 11 eqtr4i โŠข ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) = ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) )
13 12 12 oveq12i โŠข ( ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) ยทih ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) )
14 1 negcli โŠข - ๐‘† โˆˆ โ„‚
15 14 3 hvmulcli โŠข ( - ๐‘† ยทโ„Ž ๐บ ) โˆˆ โ„‹
16 2 15 hvaddcli โŠข ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) โˆˆ โ„‹
17 ax-his2 โŠข ( ( ๐น โˆˆ โ„‹ โˆง ( - ๐‘† ยทโ„Ž ๐บ ) โˆˆ โ„‹ โˆง ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) โˆˆ โ„‹ ) โ†’ ( ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) + ( ( - ๐‘† ยทโ„Ž ๐บ ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) ) )
18 2 15 16 17 mp3an โŠข ( ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) + ( ( - ๐‘† ยทโ„Ž ๐บ ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) )
19 his7 โŠข ( ( ๐น โˆˆ โ„‹ โˆง ๐น โˆˆ โ„‹ โˆง ( - ๐‘† ยทโ„Ž ๐บ ) โˆˆ โ„‹ ) โ†’ ( ๐น ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น ยทih ๐น ) + ( ๐น ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) ) )
20 2 2 15 19 mp3an โŠข ( ๐น ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น ยทih ๐น ) + ( ๐น ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) )
21 his5 โŠข ( ( - ๐‘† โˆˆ โ„‚ โˆง ๐น โˆˆ โ„‹ โˆง ๐บ โˆˆ โ„‹ ) โ†’ ( ๐น ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) = ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) )
22 14 2 3 21 mp3an โŠข ( ๐น ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) = ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐น ยทih ๐บ ) )
23 1 cjnegi โŠข ( โˆ— โ€˜ - ๐‘† ) = - ( โˆ— โ€˜ ๐‘† )
24 23 oveq1i โŠข ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) = ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) )
25 22 24 eqtri โŠข ( ๐น ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) = ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) )
26 25 oveq2i โŠข ( ( ๐น ยทih ๐น ) + ( ๐น ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น ยทih ๐น ) + ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) )
27 20 26 eqtri โŠข ( ๐น ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐น ยทih ๐น ) + ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) )
28 ax-his3 โŠข ( ( - ๐‘† โˆˆ โ„‚ โˆง ๐บ โˆˆ โ„‹ โˆง ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) โˆˆ โ„‹ ) โ†’ ( ( - ๐‘† ยทโ„Ž ๐บ ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( - ๐‘† ยท ( ๐บ ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) ) )
29 14 3 16 28 mp3an โŠข ( ( - ๐‘† ยทโ„Ž ๐บ ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( - ๐‘† ยท ( ๐บ ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) )
30 his7 โŠข ( ( ๐บ โˆˆ โ„‹ โˆง ๐น โˆˆ โ„‹ โˆง ( - ๐‘† ยทโ„Ž ๐บ ) โˆˆ โ„‹ ) โ†’ ( ๐บ ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐บ ยทih ๐น ) + ( ๐บ ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) ) )
31 3 2 15 30 mp3an โŠข ( ๐บ ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐บ ยทih ๐น ) + ( ๐บ ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) )
32 his5 โŠข ( ( - ๐‘† โˆˆ โ„‚ โˆง ๐บ โˆˆ โ„‹ โˆง ๐บ โˆˆ โ„‹ ) โ†’ ( ๐บ ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) = ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) )
33 14 3 3 32 mp3an โŠข ( ๐บ ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) = ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) )
34 33 oveq2i โŠข ( ( ๐บ ยทih ๐น ) + ( ๐บ ยทih ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐บ ยทih ๐น ) + ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) )
35 31 34 eqtri โŠข ( ๐บ ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ๐บ ยทih ๐น ) + ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) )
36 35 oveq2i โŠข ( - ๐‘† ยท ( ๐บ ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) ) = ( - ๐‘† ยท ( ( ๐บ ยทih ๐น ) + ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) ) )
37 3 2 hicli โŠข ( ๐บ ยทih ๐น ) โˆˆ โ„‚
38 14 cjcli โŠข ( โˆ— โ€˜ - ๐‘† ) โˆˆ โ„‚
39 3 3 hicli โŠข ( ๐บ ยทih ๐บ ) โˆˆ โ„‚
40 38 39 mulcli โŠข ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) โˆˆ โ„‚
41 14 37 40 adddii โŠข ( - ๐‘† ยท ( ( ๐บ ยทih ๐น ) + ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) ) ) = ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( - ๐‘† ยท ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) ) )
42 14 38 39 mulassi โŠข ( ( - ๐‘† ยท ( โˆ— โ€˜ - ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) = ( - ๐‘† ยท ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) )
43 23 oveq2i โŠข ( - ๐‘† ยท ( โˆ— โ€˜ - ๐‘† ) ) = ( - ๐‘† ยท - ( โˆ— โ€˜ ๐‘† ) )
44 1 cjcli โŠข ( โˆ— โ€˜ ๐‘† ) โˆˆ โ„‚
45 1 44 mul2negi โŠข ( - ๐‘† ยท - ( โˆ— โ€˜ ๐‘† ) ) = ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) )
46 43 45 eqtri โŠข ( - ๐‘† ยท ( โˆ— โ€˜ - ๐‘† ) ) = ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) )
47 46 oveq1i โŠข ( ( - ๐‘† ยท ( โˆ— โ€˜ - ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) = ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) )
48 42 47 eqtr3i โŠข ( - ๐‘† ยท ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) ) = ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) )
49 48 oveq2i โŠข ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( - ๐‘† ยท ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) ) ) = ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) )
50 41 49 eqtri โŠข ( - ๐‘† ยท ( ( ๐บ ยทih ๐น ) + ( ( โˆ— โ€˜ - ๐‘† ) ยท ( ๐บ ยทih ๐บ ) ) ) ) = ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) )
51 29 36 50 3eqtri โŠข ( ( - ๐‘† ยทโ„Ž ๐บ ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) )
52 27 51 oveq12i โŠข ( ( ๐น ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) + ( ( - ๐‘† ยทโ„Ž ๐บ ) ยทih ( ๐น +โ„Ž ( - ๐‘† ยทโ„Ž ๐บ ) ) ) ) = ( ( ( ๐น ยทih ๐น ) + ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) ) + ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) ) )
53 13 18 52 3eqtri โŠข ( ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) ยทih ( ๐น โˆ’โ„Ž ( ๐‘† ยทโ„Ž ๐บ ) ) ) = ( ( ( ๐น ยทih ๐น ) + ( - ( โˆ— โ€˜ ๐‘† ) ยท ( ๐น ยทih ๐บ ) ) ) + ( ( - ๐‘† ยท ( ๐บ ยทih ๐น ) ) + ( ( ๐‘† ยท ( โˆ— โ€˜ ๐‘† ) ) ยท ( ๐บ ยทih ๐บ ) ) ) )