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	|- A e. ~H
	normlem8.2	|- B e. ~H
	normlem8.3	|- C e. ~H
	normlem8.4	|- D e. ~H
Assertion	normlem8	|- ( ( A +h B ) .ih ( C +h D ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) + ( ( A .ih D ) + ( B .ih C ) ) )

Proof

Step	Hyp	Ref	Expression
1		normlem8.1	|- A e. ~H
2		normlem8.2	|- B e. ~H
3		normlem8.3	|- C e. ~H
4		normlem8.4	|- D e. ~H
5		his7	|- ( ( A e. ~H /\ C e. ~H /\ D e. ~H ) -> ( A .ih ( C +h D ) ) = ( ( A .ih C ) + ( A .ih D ) ) )
6	1 3 4 5	mp3an	|- ( A .ih ( C +h D ) ) = ( ( A .ih C ) + ( A .ih D ) )
7		his7	|- ( ( B e. ~H /\ C e. ~H /\ D e. ~H ) -> ( B .ih ( C +h D ) ) = ( ( B .ih C ) + ( B .ih D ) ) )
8	2 3 4 7	mp3an	|- ( B .ih ( C +h D ) ) = ( ( B .ih C ) + ( B .ih D ) )
9	6 8	oveq12i	|- ( ( A .ih ( C +h D ) ) + ( B .ih ( C +h D ) ) ) = ( ( ( A .ih C ) + ( A .ih D ) ) + ( ( B .ih C ) + ( B .ih D ) ) )
10	3 4	hvaddcli	|- ( C +h D ) e. ~H
11		ax-his2	|- ( ( A e. ~H /\ B e. ~H /\ ( C +h D ) e. ~H ) -> ( ( A +h B ) .ih ( C +h D ) ) = ( ( A .ih ( C +h D ) ) + ( B .ih ( C +h D ) ) ) )
12	1 2 10 11	mp3an	|- ( ( A +h B ) .ih ( C +h D ) ) = ( ( A .ih ( C +h D ) ) + ( B .ih ( C +h D ) ) )
13	1 3	hicli	|- ( A .ih C ) e. CC
14	2 4	hicli	|- ( B .ih D ) e. CC
15	1 4	hicli	|- ( A .ih D ) e. CC
16	2 3	hicli	|- ( B .ih C ) e. CC
17	13 14 15 16	add42i	|- ( ( ( A .ih C ) + ( B .ih D ) ) + ( ( A .ih D ) + ( B .ih C ) ) ) = ( ( ( A .ih C ) + ( A .ih D ) ) + ( ( B .ih C ) + ( B .ih D ) ) )
18	9 12 17	3eqtr4i	|- ( ( A +h B ) .ih ( C +h D ) ) = ( ( ( A .ih C ) + ( B .ih D ) ) + ( ( A .ih D ) + ( B .ih C ) ) )