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⋅ihC-ℎD=A⋅ihC+B⋅ihD-A⋅ihD+B⋅ihC

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