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

Metamath Proof Explorer

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