This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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