Metamath Proof Explorer

Theorem hvaddsub4

Description: Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvaddcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ~H )
2 1 adantr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( A +h B ) e. ~H )
3 hvaddcl 
 |-  ( ( C e. ~H /\ D e. ~H ) -> ( C +h D ) e. ~H )
4 3 adantl 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C +h D ) e. ~H )
5 hvaddcl 
 |-  ( ( C e. ~H /\ B e. ~H ) -> ( C +h B ) e. ~H )
6 5 ancoms 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( C +h B ) e. ~H )
7 6 ad2ant2lr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C +h B ) e. ~H )
8 hvsubcan2 
 |-  ( ( ( A +h B ) e. ~H /\ ( C +h D ) e. ~H /\ ( C +h B ) e. ~H ) -> ( ( ( A +h B ) -h ( C +h B ) ) = ( ( C +h D ) -h ( C +h B ) ) <-> ( A +h B ) = ( C +h D ) ) )
9 2 4 7 8 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A +h B ) -h ( C +h B ) ) = ( ( C +h D ) -h ( C +h B ) ) <-> ( A +h B ) = ( C +h D ) ) )
10 simpr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> B e. ~H )
11 10 anim2i 
 |-  ( ( C e. ~H /\ ( A e. ~H /\ B e. ~H ) ) -> ( C e. ~H /\ B e. ~H ) )
12 11 ancoms 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( C e. ~H /\ B e. ~H ) )
13 hvsub4 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ B e. ~H ) ) -> ( ( A +h B ) -h ( C +h B ) ) = ( ( A -h C ) +h ( B -h B ) ) )
14 12 13 syldan 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A +h B ) -h ( C +h B ) ) = ( ( A -h C ) +h ( B -h B ) ) )
15 hvsubid 
 |-  ( B e. ~H -> ( B -h B ) = 0h )
16 15 ad2antlr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( B -h B ) = 0h )
17 16 oveq2d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A -h C ) +h ( B -h B ) ) = ( ( A -h C ) +h 0h ) )
18 hvsubcl 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( A -h C ) e. ~H )
19 ax-hvaddid 
 |-  ( ( A -h C ) e. ~H -> ( ( A -h C ) +h 0h ) = ( A -h C ) )
20 18 19 syl 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( ( A -h C ) +h 0h ) = ( A -h C ) )
21 20 adantlr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A -h C ) +h 0h ) = ( A -h C ) )
22 14 17 21 3eqtrd 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A +h B ) -h ( C +h B ) ) = ( A -h C ) )
23 22 adantrr 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) -h ( C +h B ) ) = ( A -h C ) )
24 simpl 
 |-  ( ( C e. ~H /\ D e. ~H ) -> C e. ~H )
25 24 anim1i 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( C e. ~H /\ B e. ~H ) )
26 hvsub4 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ ( C e. ~H /\ B e. ~H ) ) -> ( ( C +h D ) -h ( C +h B ) ) = ( ( C -h C ) +h ( D -h B ) ) )
27 25 26 syldan 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( ( C +h D ) -h ( C +h B ) ) = ( ( C -h C ) +h ( D -h B ) ) )
28 hvsubid 
 |-  ( C e. ~H -> ( C -h C ) = 0h )
29 28 ad2antrr 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( C -h C ) = 0h )
30 29 oveq1d 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( ( C -h C ) +h ( D -h B ) ) = ( 0h +h ( D -h B ) ) )
31 hvsubcl 
 |-  ( ( D e. ~H /\ B e. ~H ) -> ( D -h B ) e. ~H )
32 hvaddlid 
 |-  ( ( D -h B ) e. ~H -> ( 0h +h ( D -h B ) ) = ( D -h B ) )
33 31 32 syl 
 |-  ( ( D e. ~H /\ B e. ~H ) -> ( 0h +h ( D -h B ) ) = ( D -h B ) )
34 33 adantll 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( 0h +h ( D -h B ) ) = ( D -h B ) )
35 27 30 34 3eqtrd 
 |-  ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( ( C +h D ) -h ( C +h B ) ) = ( D -h B ) )
36 35 ancoms 
 |-  ( ( B e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( C +h D ) -h ( C +h B ) ) = ( D -h B ) )
37 36 adantll 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( C +h D ) -h ( C +h B ) ) = ( D -h B ) )
38 23 37 eqeq12d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A +h B ) -h ( C +h B ) ) = ( ( C +h D ) -h ( C +h B ) ) <-> ( A -h C ) = ( D -h B ) ) )
39 9 38 bitr3d 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) = ( C +h D ) <-> ( A -h C ) = ( D -h B ) ) )