# 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 𝐴 ∈ ℋ
normlem8.2 𝐵 ∈ ℋ
normlem8.3 𝐶 ∈ ℋ
normlem8.4 𝐷 ∈ ℋ
Assertion normlem9 ( ( 𝐴 𝐵 ) ·ih ( 𝐶 𝐷 ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) − ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )

### Proof

Step Hyp Ref Expression
1 normlem8.1 𝐴 ∈ ℋ
2 normlem8.2 𝐵 ∈ ℋ
3 normlem8.3 𝐶 ∈ ℋ
4 normlem8.4 𝐷 ∈ ℋ
5 1 2 hvsubvali ( 𝐴 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) )
6 3 4 hvsubvali ( 𝐶 𝐷 ) = ( 𝐶 + ( - 1 · 𝐷 ) )
7 5 6 oveq12i ( ( 𝐴 𝐵 ) ·ih ( 𝐶 𝐷 ) ) = ( ( 𝐴 + ( - 1 · 𝐵 ) ) ·ih ( 𝐶 + ( - 1 · 𝐷 ) ) )
8 neg1cn - 1 ∈ ℂ
9 8 2 hvmulcli ( - 1 · 𝐵 ) ∈ ℋ
10 8 4 hvmulcli ( - 1 · 𝐷 ) ∈ ℋ
11 1 9 3 10 normlem8 ( ( 𝐴 + ( - 1 · 𝐵 ) ) ·ih ( 𝐶 + ( - 1 · 𝐷 ) ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) ) + ( ( 𝐴 ·ih ( - 1 · 𝐷 ) ) + ( ( - 1 · 𝐵 ) ·ih 𝐶 ) ) )
12 ax-his3 ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ ( - 1 · 𝐷 ) ∈ ℋ ) → ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) = ( - 1 · ( 𝐵 ·ih ( - 1 · 𝐷 ) ) ) )
13 8 2 10 12 mp3an ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) = ( - 1 · ( 𝐵 ·ih ( - 1 · 𝐷 ) ) )
14 his5 ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐵 ·ih ( - 1 · 𝐷 ) ) = ( ( ∗ ‘ - 1 ) · ( 𝐵 ·ih 𝐷 ) ) )
15 8 2 4 14 mp3an ( 𝐵 ·ih ( - 1 · 𝐷 ) ) = ( ( ∗ ‘ - 1 ) · ( 𝐵 ·ih 𝐷 ) )
16 15 oveq2i ( - 1 · ( 𝐵 ·ih ( - 1 · 𝐷 ) ) ) = ( - 1 · ( ( ∗ ‘ - 1 ) · ( 𝐵 ·ih 𝐷 ) ) )
17 neg1rr - 1 ∈ ℝ
18 cjre ( - 1 ∈ ℝ → ( ∗ ‘ - 1 ) = - 1 )
19 17 18 ax-mp ( ∗ ‘ - 1 ) = - 1
20 19 oveq2i ( - 1 · ( ∗ ‘ - 1 ) ) = ( - 1 · - 1 )
21 ax-1cn 1 ∈ ℂ
22 21 21 mul2negi ( - 1 · - 1 ) = ( 1 · 1 )
23 21 mulid2i ( 1 · 1 ) = 1
24 20 22 23 3eqtri ( - 1 · ( ∗ ‘ - 1 ) ) = 1
25 24 oveq1i ( ( - 1 · ( ∗ ‘ - 1 ) ) · ( 𝐵 ·ih 𝐷 ) ) = ( 1 · ( 𝐵 ·ih 𝐷 ) )
26 8 cjcli ( ∗ ‘ - 1 ) ∈ ℂ
27 2 4 hicli ( 𝐵 ·ih 𝐷 ) ∈ ℂ
28 8 26 27 mulassi ( ( - 1 · ( ∗ ‘ - 1 ) ) · ( 𝐵 ·ih 𝐷 ) ) = ( - 1 · ( ( ∗ ‘ - 1 ) · ( 𝐵 ·ih 𝐷 ) ) )
29 27 mulid2i ( 1 · ( 𝐵 ·ih 𝐷 ) ) = ( 𝐵 ·ih 𝐷 )
30 25 28 29 3eqtr3i ( - 1 · ( ( ∗ ‘ - 1 ) · ( 𝐵 ·ih 𝐷 ) ) ) = ( 𝐵 ·ih 𝐷 )
31 13 16 30 3eqtri ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) = ( 𝐵 ·ih 𝐷 )
32 31 oveq2i ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) ) = ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) )
33 his5 ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐴 ·ih ( - 1 · 𝐷 ) ) = ( ( ∗ ‘ - 1 ) · ( 𝐴 ·ih 𝐷 ) ) )
34 8 1 4 33 mp3an ( 𝐴 ·ih ( - 1 · 𝐷 ) ) = ( ( ∗ ‘ - 1 ) · ( 𝐴 ·ih 𝐷 ) )
35 19 oveq1i ( ( ∗ ‘ - 1 ) · ( 𝐴 ·ih 𝐷 ) ) = ( - 1 · ( 𝐴 ·ih 𝐷 ) )
36 1 4 hicli ( 𝐴 ·ih 𝐷 ) ∈ ℂ
37 36 mulm1i ( - 1 · ( 𝐴 ·ih 𝐷 ) ) = - ( 𝐴 ·ih 𝐷 )
38 34 35 37 3eqtri ( 𝐴 ·ih ( - 1 · 𝐷 ) ) = - ( 𝐴 ·ih 𝐷 )
39 ax-his3 ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 · 𝐵 ) ·ih 𝐶 ) = ( - 1 · ( 𝐵 ·ih 𝐶 ) ) )
40 8 2 3 39 mp3an ( ( - 1 · 𝐵 ) ·ih 𝐶 ) = ( - 1 · ( 𝐵 ·ih 𝐶 ) )
41 2 3 hicli ( 𝐵 ·ih 𝐶 ) ∈ ℂ
42 41 mulm1i ( - 1 · ( 𝐵 ·ih 𝐶 ) ) = - ( 𝐵 ·ih 𝐶 )
43 40 42 eqtri ( ( - 1 · 𝐵 ) ·ih 𝐶 ) = - ( 𝐵 ·ih 𝐶 )
44 38 43 oveq12i ( ( 𝐴 ·ih ( - 1 · 𝐷 ) ) + ( ( - 1 · 𝐵 ) ·ih 𝐶 ) ) = ( - ( 𝐴 ·ih 𝐷 ) + - ( 𝐵 ·ih 𝐶 ) )
45 36 41 negdii - ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) = ( - ( 𝐴 ·ih 𝐷 ) + - ( 𝐵 ·ih 𝐶 ) )
46 44 45 eqtr4i ( ( 𝐴 ·ih ( - 1 · 𝐷 ) ) + ( ( - 1 · 𝐵 ) ·ih 𝐶 ) ) = - ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) )
47 32 46 oveq12i ( ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) ) + ( ( 𝐴 ·ih ( - 1 · 𝐷 ) ) + ( ( - 1 · 𝐵 ) ·ih 𝐶 ) ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) + - ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )
48 1 3 hicli ( 𝐴 ·ih 𝐶 ) ∈ ℂ
49 48 27 addcli ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) ∈ ℂ
50 36 41 addcli ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) ∈ ℂ
51 49 50 negsubi ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) + - ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) − ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )
52 47 51 eqtri ( ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 · 𝐵 ) ·ih ( - 1 · 𝐷 ) ) ) + ( ( 𝐴 ·ih ( - 1 · 𝐷 ) ) + ( ( - 1 · 𝐵 ) ·ih 𝐶 ) ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) − ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )
53 7 11 52 3eqtri ( ( 𝐴 𝐵 ) ·ih ( 𝐶 𝐷 ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) − ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )