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 ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B = C + ℎ D ↔ A - ℎ C = D - ℎ B

Proof

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