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}\in ℋ$
normlem8.2 ${⊢}{B}\in ℋ$
normlem8.3 ${⊢}{C}\in ℋ$
normlem8.4 ${⊢}{D}\in ℋ$
Assertion normlem9 ${⊢}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{-}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$

Proof

Step Hyp Ref Expression
1 normlem8.1 ${⊢}{A}\in ℋ$
2 normlem8.2 ${⊢}{B}\in ℋ$
3 normlem8.3 ${⊢}{C}\in ℋ$
4 normlem8.4 ${⊢}{D}\in ℋ$
5 1 2 hvsubvali ${⊢}{A}{-}_{ℎ}{B}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
6 3 4 hvsubvali ${⊢}{C}{-}_{ℎ}{D}={C}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{D}\right)$
7 5 6 oveq12i ${⊢}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{-}_{ℎ}{D}\right)=\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{D}\right)\right)$
8 neg1cn ${⊢}-1\in ℂ$
9 8 2 hvmulcli ${⊢}-1{\cdot }_{ℎ}{B}\in ℋ$
10 8 4 hvmulcli ${⊢}-1{\cdot }_{ℎ}{D}\in ℋ$
11 1 9 3 10 normlem8 ${⊢}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{D}\right)\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left({A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)$
12 ax-his3 ${⊢}\left(-1\in ℂ\wedge {B}\in ℋ\wedge -1{\cdot }_{ℎ}{D}\in ℋ\right)\to \left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=-1\left({B}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)$
13 8 2 10 12 mp3an ${⊢}\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=-1\left({B}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)$
14 his5 ${⊢}\left(-1\in ℂ\wedge {B}\in ℋ\wedge {D}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
15 8 2 4 14 mp3an ${⊢}{B}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
16 15 oveq2i ${⊢}-1\left({B}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)=-1\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
17 neg1rr ${⊢}-1\in ℝ$
18 cjre ${⊢}-1\in ℝ\to \stackrel{‾}{-1}=-1$
19 17 18 ax-mp ${⊢}\stackrel{‾}{-1}=-1$
20 19 oveq2i ${⊢}-1\stackrel{‾}{-1}=-1-1$
21 ax-1cn ${⊢}1\in ℂ$
22 21 21 mul2negi ${⊢}-1-1=1\cdot 1$
23 21 mulid2i ${⊢}1\cdot 1=1$
24 20 22 23 3eqtri ${⊢}-1\stackrel{‾}{-1}=1$
25 24 oveq1i ${⊢}-1\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)=1\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
26 8 cjcli ${⊢}\stackrel{‾}{-1}\in ℂ$
27 2 4 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{D}\in ℂ$
28 8 26 27 mulassi ${⊢}-1\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)=-1\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
29 27 mulid2i ${⊢}1\left({B}{\cdot }_{\mathrm{ih}}{D}\right)={B}{\cdot }_{\mathrm{ih}}{D}$
30 25 28 29 3eqtr3i ${⊢}-1\stackrel{‾}{-1}\left({B}{\cdot }_{\mathrm{ih}}{D}\right)={B}{\cdot }_{\mathrm{ih}}{D}$
31 13 16 30 3eqtri ${⊢}\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)={B}{\cdot }_{\mathrm{ih}}{D}$
32 31 oveq2i ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
33 his5 ${⊢}\left(-1\in ℂ\wedge {A}\in ℋ\wedge {D}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{-1}\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
34 8 1 4 33 mp3an ${⊢}{A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=\stackrel{‾}{-1}\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
35 19 oveq1i ${⊢}\stackrel{‾}{-1}\left({A}{\cdot }_{\mathrm{ih}}{D}\right)=-1\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
36 1 4 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{D}\in ℂ$
37 36 mulm1i ${⊢}-1\left({A}{\cdot }_{\mathrm{ih}}{D}\right)=-\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
38 34 35 37 3eqtri ${⊢}{A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)=-\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
39 ax-his3 ${⊢}\left(-1\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=-1\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
40 8 2 3 39 mp3an ${⊢}\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=-1\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
41 2 3 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
42 41 mulm1i ${⊢}-1\left({B}{\cdot }_{\mathrm{ih}}{C}\right)=-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
43 40 42 eqtri ${⊢}\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
44 38 43 oveq12i ${⊢}\left({A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)=-\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left(-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
45 36 41 negdii ${⊢}-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)=-\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left(-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
46 44 45 eqtr4i ${⊢}\left({A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)=-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
47 32 46 oveq12i ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left({A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)+\left(-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)\right)$
48 1 3 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
49 48 27 addcli ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)\in ℂ$
50 36 41 addcli ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\in ℂ$
51 49 50 negsubi ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)+\left(-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
52 47 51 eqtri ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left({A}{\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}{D}\right)\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
53 7 11 52 3eqtri ${⊢}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{-}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)-\left(\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$