This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mullidi ⊢ ( 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 mullidi ⊢ ( 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 𝐶 ) ) )