Theorem hvsubdistr2

Description: Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsubdistr2	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A - B ) .h C ) = ( ( A .h C ) -h ( B .h C ) ) )

Proof

Step	Hyp	Ref	Expression
1		hvmulcl	|- ( ( A e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
2	1	3adant2	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
3		hvmulcl	|- ( ( B e. CC /\ C e. ~H ) -> ( B .h C ) e. ~H )
4	3	3adant1	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( B .h C ) e. ~H )
5		hvsubval	|- ( ( ( A .h C ) e. ~H /\ ( B .h C ) e. ~H ) -> ( ( A .h C ) -h ( B .h C ) ) = ( ( A .h C ) +h ( -u 1 .h ( B .h C ) ) ) )
6	2 4 5	syl2anc	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A .h C ) -h ( B .h C ) ) = ( ( A .h C ) +h ( -u 1 .h ( B .h C ) ) ) )
7		mulm1	|- ( B e. CC -> ( -u 1 x. B ) = -u B )
8	7	oveq1d	|- ( B e. CC -> ( ( -u 1 x. B ) .h C ) = ( -u B .h C ) )
9	8	adantr	|- ( ( B e. CC /\ C e. ~H ) -> ( ( -u 1 x. B ) .h C ) = ( -u B .h C ) )
10		neg1cn	|- -u 1 e. CC
11		ax-hvmulass	|- ( ( -u 1 e. CC /\ B e. CC /\ C e. ~H ) -> ( ( -u 1 x. B ) .h C ) = ( -u 1 .h ( B .h C ) ) )
12	10 11	mp3an1	|- ( ( B e. CC /\ C e. ~H ) -> ( ( -u 1 x. B ) .h C ) = ( -u 1 .h ( B .h C ) ) )
13	9 12	eqtr3d	|- ( ( B e. CC /\ C e. ~H ) -> ( -u B .h C ) = ( -u 1 .h ( B .h C ) ) )
14	13	3adant1	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( -u B .h C ) = ( -u 1 .h ( B .h C ) ) )
15	14	oveq2d	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A .h C ) +h ( -u B .h C ) ) = ( ( A .h C ) +h ( -u 1 .h ( B .h C ) ) ) )
16		negcl	|- ( B e. CC -> -u B e. CC )
17		ax-hvdistr2	|- ( ( A e. CC /\ -u B e. CC /\ C e. ~H ) -> ( ( A + -u B ) .h C ) = ( ( A .h C ) +h ( -u B .h C ) ) )
18	16 17	syl3an2	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A + -u B ) .h C ) = ( ( A .h C ) +h ( -u B .h C ) ) )
19		negsub	|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
20	19	3adant3	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( A + -u B ) = ( A - B ) )
21	20	oveq1d	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A + -u B ) .h C ) = ( ( A - B ) .h C ) )
22	18 21	eqtr3d	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A .h C ) +h ( -u B .h C ) ) = ( ( A - B ) .h C ) )
23	6 15 22	3eqtr2rd	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A - B ) .h C ) = ( ( A .h C ) -h ( B .h C ) ) )