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 𝐶 ) ) )