# Metamath Proof Explorer

## Theorem normlem8

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 normlem8 ( ( 𝐴 + 𝐵 ) ·ih ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )

### Proof

Step Hyp Ref Expression
1 normlem8.1 𝐴 ∈ ℋ
2 normlem8.2 𝐵 ∈ ℋ
3 normlem8.3 𝐶 ∈ ℋ
4 normlem8.4 𝐷 ∈ ℋ
5 his7 ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐴 ·ih ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 ·ih 𝐶 ) + ( 𝐴 ·ih 𝐷 ) ) )
6 1 3 4 5 mp3an ( 𝐴 ·ih ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 ·ih 𝐶 ) + ( 𝐴 ·ih 𝐷 ) )
7 his7 ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐵 ·ih ( 𝐶 + 𝐷 ) ) = ( ( 𝐵 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) )
8 2 3 4 7 mp3an ( 𝐵 ·ih ( 𝐶 + 𝐷 ) ) = ( ( 𝐵 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) )
9 6 8 oveq12i ( ( 𝐴 ·ih ( 𝐶 + 𝐷 ) ) + ( 𝐵 ·ih ( 𝐶 + 𝐷 ) ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐴 ·ih 𝐷 ) ) + ( ( 𝐵 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) )
10 3 4 hvaddcli ( 𝐶 + 𝐷 ) ∈ ℋ
11 ax-his2 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( 𝐶 + 𝐷 ) ∈ ℋ ) → ( ( 𝐴 + 𝐵 ) ·ih ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 ·ih ( 𝐶 + 𝐷 ) ) + ( 𝐵 ·ih ( 𝐶 + 𝐷 ) ) ) )
12 1 2 10 11 mp3an ( ( 𝐴 + 𝐵 ) ·ih ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 ·ih ( 𝐶 + 𝐷 ) ) + ( 𝐵 ·ih ( 𝐶 + 𝐷 ) ) )
13 1 3 hicli ( 𝐴 ·ih 𝐶 ) ∈ ℂ
14 2 4 hicli ( 𝐵 ·ih 𝐷 ) ∈ ℂ
15 1 4 hicli ( 𝐴 ·ih 𝐷 ) ∈ ℂ
16 2 3 hicli ( 𝐵 ·ih 𝐶 ) ∈ ℂ
17 13 14 15 16 add42i ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐴 ·ih 𝐷 ) ) + ( ( 𝐵 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) )
18 9 12 17 3eqtr4i ( ( 𝐴 + 𝐵 ) ·ih ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 ·ih 𝐶 ) + ( 𝐵 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐷 ) + ( 𝐵 ·ih 𝐶 ) ) )