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 ∈ ℋ
normlem8.2 ⊢ B ∈ ℋ
normlem8.3 ⊢ C ∈ ℋ
normlem8.4 ⊢ D ∈ ℋ
Assertion normlem9 ⊢ A - ℎ B ⋅ ih C - ℎ D = A ⋅ ih C + B ⋅ ih D - A ⋅ ih D + B ⋅ ih C

Proof

Step Hyp Ref Expression
1 normlem8.1 ⊢ A ∈ ℋ
2 normlem8.2 ⊢ B ∈ ℋ
3 normlem8.3 ⊢ C ∈ ℋ
4 normlem8.4 ⊢ D ∈ ℋ
5 1 2 hvsubvali ⊢ A - ℎ B = A + ℎ -1 ⋅ ℎ B
6 3 4 hvsubvali ⊢ C - ℎ D = C + ℎ -1 ⋅ ℎ D
7 5 6 oveq12i ⊢ A - ℎ B ⋅ ih C - ℎ D = A + ℎ -1 ⋅ ℎ B ⋅ ih C + ℎ -1 ⋅ ℎ D
8 neg1cn ⊢ − 1 ∈ ℂ
9 8 2 hvmulcli ⊢ -1 ⋅ ℎ B ∈ ℋ
10 8 4 hvmulcli ⊢ -1 ⋅ ℎ D ∈ ℋ
11 1 9 3 10 normlem8 ⊢ A + ℎ -1 ⋅ ℎ B ⋅ ih C + ℎ -1 ⋅ ℎ D = A ⋅ ih C + -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D + A ⋅ ih -1 ⋅ ℎ D + -1 ⋅ ℎ B ⋅ ih C
12 ax-his3 ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ D ∈ ℋ → -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D = -1 ⁢ B ⋅ ih -1 ⋅ ℎ D
13 8 2 10 12 mp3an ⊢ -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D = -1 ⁢ B ⋅ ih -1 ⋅ ℎ D
14 his5 ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ ∧ D ∈ ℋ → B ⋅ ih -1 ⋅ ℎ D = − 1 ‾ ⁢ B ⋅ ih D
15 8 2 4 14 mp3an ⊢ B ⋅ ih -1 ⋅ ℎ D = − 1 ‾ ⁢ B ⋅ ih D
16 15 oveq2i ⊢ -1 ⁢ B ⋅ ih -1 ⋅ ℎ D = -1 ⁢ − 1 ‾ ⁢ B ⋅ ih D
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 ‾ ⁢ B ⋅ ih D = 1 ⁢ B ⋅ ih D
26 8 cjcli ⊢ − 1 ‾ ∈ ℂ
27 2 4 hicli ⊢ B ⋅ ih D ∈ ℂ
28 8 26 27 mulassi ⊢ -1 ⁢ − 1 ‾ ⁢ B ⋅ ih D = -1 ⁢ − 1 ‾ ⁢ B ⋅ ih D
29 27 mulid2i ⊢ 1 ⁢ B ⋅ ih D = B ⋅ ih D
30 25 28 29 3eqtr3i ⊢ -1 ⁢ − 1 ‾ ⁢ B ⋅ ih D = B ⋅ ih D
31 13 16 30 3eqtri ⊢ -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D = B ⋅ ih D
32 31 oveq2i ⊢ A ⋅ ih C + -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D = A ⋅ ih C + B ⋅ ih D
33 his5 ⊢ − 1 ∈ ℂ ∧ A ∈ ℋ ∧ D ∈ ℋ → A ⋅ ih -1 ⋅ ℎ D = − 1 ‾ ⁢ A ⋅ ih D
34 8 1 4 33 mp3an ⊢ A ⋅ ih -1 ⋅ ℎ D = − 1 ‾ ⁢ A ⋅ ih D
35 19 oveq1i ⊢ − 1 ‾ ⁢ A ⋅ ih D = -1 ⁢ A ⋅ ih D
36 1 4 hicli ⊢ A ⋅ ih D ∈ ℂ
37 36 mulm1i ⊢ -1 ⁢ A ⋅ ih D = − A ⋅ ih D
38 34 35 37 3eqtri ⊢ A ⋅ ih -1 ⋅ ℎ D = − A ⋅ ih D
39 ax-his3 ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → -1 ⋅ ℎ B ⋅ ih C = -1 ⁢ B ⋅ ih C
40 8 2 3 39 mp3an ⊢ -1 ⋅ ℎ B ⋅ ih C = -1 ⁢ B ⋅ ih C
41 2 3 hicli ⊢ B ⋅ ih C ∈ ℂ
42 41 mulm1i ⊢ -1 ⁢ B ⋅ ih C = − B ⋅ ih C
43 40 42 eqtri ⊢ -1 ⋅ ℎ B ⋅ ih C = − B ⋅ ih C
44 38 43 oveq12i ⊢ A ⋅ ih -1 ⋅ ℎ D + -1 ⋅ ℎ B ⋅ ih C = - A ⋅ ih D + − B ⋅ ih C
45 36 41 negdii ⊢ − A ⋅ ih D + B ⋅ ih C = - A ⋅ ih D + − B ⋅ ih C
46 44 45 eqtr4i ⊢ A ⋅ ih -1 ⋅ ℎ D + -1 ⋅ ℎ B ⋅ ih C = − A ⋅ ih D + B ⋅ ih C
47 32 46 oveq12i ⊢ A ⋅ ih C + -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D + A ⋅ ih -1 ⋅ ℎ D + -1 ⋅ ℎ B ⋅ ih C = A ⋅ ih C + B ⋅ ih D + − A ⋅ ih D + B ⋅ ih C
48 1 3 hicli ⊢ A ⋅ ih C ∈ ℂ
49 48 27 addcli ⊢ A ⋅ ih C + B ⋅ ih D ∈ ℂ
50 36 41 addcli ⊢ A ⋅ ih D + B ⋅ ih C ∈ ℂ
51 49 50 negsubi ⊢ A ⋅ ih C + B ⋅ ih D + − 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 + -1 ⋅ ℎ B ⋅ ih -1 ⋅ ℎ D + A ⋅ ih -1 ⋅ ℎ D + -1 ⋅ ℎ B ⋅ ih C = A ⋅ ih C + B ⋅ ih D - A ⋅ ih D + B ⋅ ih C
53 7 11 52 3eqtri ⊢ A - ℎ B ⋅ ih C - ℎ D = A ⋅ ih C + B ⋅ ih D - A ⋅ ih D + B ⋅ ih C