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