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