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