Axiom ax-his2

Description: Distributive law for inner product. Postulate (S2) of Beran p. 95. (Contributed by NM, 31-Jul-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-his2	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) .ih C ) = ( ( A .ih C ) + ( B .ih C ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		chba	|- ~H
2	0 1	wcel	|- A e. ~H
3		cB	|- B
4	3 1	wcel	|- B e. ~H
5		cC	|- C
6	5 1	wcel	|- C e. ~H
7	2 4 6	w3a	|- ( A e. ~H /\ B e. ~H /\ C e. ~H )
8		cva	|- +h
9	0 3 8	co	|- ( A +h B )
10		csp	|- .ih
11	9 5 10	co	|- ( ( A +h B ) .ih C )
12	0 5 10	co	|- ( A .ih C )
13		caddc	|- +
14	3 5 10	co	|- ( B .ih C )
15	12 14 13	co	|- ( ( A .ih C ) + ( B .ih C ) )
16	11 15	wceq	|- ( ( A +h B ) .ih C ) = ( ( A .ih C ) + ( B .ih C ) )
17	7 16	wi	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) .ih C ) = ( ( A .ih C ) + ( B .ih C ) ) )