Metamath Proof Explorer


Theorem hvsubass

Description: Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 neg1cn
 |-  -u 1 e. CC
2 hvmulcl
 |-  ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H )
3 1 2 mpan
 |-  ( B e. ~H -> ( -u 1 .h B ) e. ~H )
4 hvaddsubass
 |-  ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) -h C ) = ( A +h ( ( -u 1 .h B ) -h C ) ) )
5 3 4 syl3an2
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) -h C ) = ( A +h ( ( -u 1 .h B ) -h C ) ) )
6 hvsubval
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
7 6 3adant3
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
8 7 oveq1d
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( ( A +h ( -u 1 .h B ) ) -h C ) )
9 simp1
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> A e. ~H )
10 hvaddcl
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B +h C ) e. ~H )
11 10 3adant1
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( B +h C ) e. ~H )
12 hvsubval
 |-  ( ( A e. ~H /\ ( B +h C ) e. ~H ) -> ( A -h ( B +h C ) ) = ( A +h ( -u 1 .h ( B +h C ) ) ) )
13 9 11 12 syl2anc
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h ( B +h C ) ) = ( A +h ( -u 1 .h ( B +h C ) ) ) )
14 hvsubval
 |-  ( ( ( -u 1 .h B ) e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) )
15 3 14 sylan
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) )
16 15 3adant1
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) )
17 ax-hvdistr1
 |-  ( ( -u 1 e. CC /\ B e. ~H /\ C e. ~H ) -> ( -u 1 .h ( B +h C ) ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) )
18 1 17 mp3an1
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( -u 1 .h ( B +h C ) ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) )
19 18 3adant1
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( -u 1 .h ( B +h C ) ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) )
20 16 19 eqtr4d
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( -u 1 .h ( B +h C ) ) )
21 20 oveq2d
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A +h ( ( -u 1 .h B ) -h C ) ) = ( A +h ( -u 1 .h ( B +h C ) ) ) )
22 13 21 eqtr4d
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h ( B +h C ) ) = ( A +h ( ( -u 1 .h B ) -h C ) ) )
23 5 8 22 3eqtr4d
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( A -h ( B +h C ) ) )