Metamath Proof Explorer

Theorem hvsubdistr1

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

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

Proof

Step Hyp Ref Expression
1 neg1cn 
 |-  -u 1 e. CC
2 hvmulcl 
 |-  ( ( -u 1 e. CC /\ C e. ~H ) -> ( -u 1 .h C ) e. ~H )
3 1 2 mpan 
 |-  ( C e. ~H -> ( -u 1 .h C ) e. ~H )
4 ax-hvdistr1 
 |-  ( ( A e. CC /\ B e. ~H /\ ( -u 1 .h C ) e. ~H ) -> ( A .h ( B +h ( -u 1 .h C ) ) ) = ( ( A .h B ) +h ( A .h ( -u 1 .h C ) ) ) )
5 3 4 syl3an3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B +h ( -u 1 .h C ) ) ) = ( ( A .h B ) +h ( A .h ( -u 1 .h C ) ) ) )
6 hvmulcom 
 |-  ( ( A e. CC /\ -u 1 e. CC /\ C e. ~H ) -> ( A .h ( -u 1 .h C ) ) = ( -u 1 .h ( A .h C ) ) )
7 1 6 mp3an2 
 |-  ( ( A e. CC /\ C e. ~H ) -> ( A .h ( -u 1 .h C ) ) = ( -u 1 .h ( A .h C ) ) )
8 7 oveq2d 
 |-  ( ( A e. CC /\ C e. ~H ) -> ( ( A .h B ) +h ( A .h ( -u 1 .h C ) ) ) = ( ( A .h B ) +h ( -u 1 .h ( A .h C ) ) ) )
9 8 3adant2 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) +h ( A .h ( -u 1 .h C ) ) ) = ( ( A .h B ) +h ( -u 1 .h ( A .h C ) ) ) )
10 5 9 eqtrd 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B +h ( -u 1 .h C ) ) ) = ( ( A .h B ) +h ( -u 1 .h ( A .h C ) ) ) )
11 hvsubval 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B -h C ) = ( B +h ( -u 1 .h C ) ) )
12 11 3adant1 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B -h C ) = ( B +h ( -u 1 .h C ) ) )
13 12 oveq2d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B -h C ) ) = ( A .h ( B +h ( -u 1 .h C ) ) ) )
14 hvmulcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
15 14 3adant3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h B ) e. ~H )
16 hvmulcl 
 |-  ( ( A e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
17 16 3adant2 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h C ) e. ~H )
18 hvsubval 
 |-  ( ( ( A .h B ) e. ~H /\ ( A .h C ) e. ~H ) -> ( ( A .h B ) -h ( A .h C ) ) = ( ( A .h B ) +h ( -u 1 .h ( A .h C ) ) ) )
19 15 17 18 syl2anc 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) -h ( A .h C ) ) = ( ( A .h B ) +h ( -u 1 .h ( A .h C ) ) ) )
20 10 13 19 3eqtr4d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B -h C ) ) = ( ( A .h B ) -h ( A .h C ) ) )