Metamath Proof Explorer

Theorem hvsub4

Description: Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsub4 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B - ℎ C + ℎ D = A - ℎ C + ℎ B - ℎ D

Proof

Step Hyp Ref Expression
1 hvaddcl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ ℋ
2 hvaddcl ⊢ C ∈ ℋ ∧ D ∈ ℋ → C + ℎ D ∈ ℋ
3 hvsubval ⊢ A + ℎ B ∈ ℋ ∧ C + ℎ D ∈ ℋ → A + ℎ B - ℎ C + ℎ D = A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ D
4 1 2 3 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B - ℎ C + ℎ D = A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ D
5 hvsubval ⊢ A ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = A + ℎ -1 ⋅ ℎ C
6 5 ad2ant2r ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A - ℎ C = A + ℎ -1 ⋅ ℎ C
7 hvsubval ⊢ B ∈ ℋ ∧ D ∈ ℋ → B - ℎ D = B + ℎ -1 ⋅ ℎ D
8 7 ad2ant2l ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → B - ℎ D = B + ℎ -1 ⋅ ℎ D
9 6 8 oveq12d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A - ℎ C + ℎ B - ℎ D = A + ℎ -1 ⋅ ℎ C + ℎ B + ℎ -1 ⋅ ℎ D
10 neg1cn ⊢ − 1 ∈ ℂ
11 ax-hvdistr1 ⊢ − 1 ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → -1 ⋅ ℎ C + ℎ D = -1 ⋅ ℎ C + ℎ -1 ⋅ ℎ D
12 10 11 mp3an1 ⊢ C ∈ ℋ ∧ D ∈ ℋ → -1 ⋅ ℎ C + ℎ D = -1 ⋅ ℎ C + ℎ -1 ⋅ ℎ D
13 12 adantl ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → -1 ⋅ ℎ C + ℎ D = -1 ⋅ ℎ C + ℎ -1 ⋅ ℎ D
14 13 oveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ D = A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ -1 ⋅ ℎ D
15 hvmulcl ⊢ − 1 ∈ ℂ ∧ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
16 10 15 mpan ⊢ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
17 16 anim2i ⊢ A ∈ ℋ ∧ C ∈ ℋ → A ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ
18 hvmulcl ⊢ − 1 ∈ ℂ ∧ D ∈ ℋ → -1 ⋅ ℎ D ∈ ℋ
19 10 18 mpan ⊢ D ∈ ℋ → -1 ⋅ ℎ D ∈ ℋ
20 19 anim2i ⊢ B ∈ ℋ ∧ D ∈ ℋ → B ∈ ℋ ∧ -1 ⋅ ℎ D ∈ ℋ
21 17 20 anim12i ⊢ A ∈ ℋ ∧ C ∈ ℋ ∧ B ∈ ℋ ∧ D ∈ ℋ → A ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ D ∈ ℋ
22 21 an4s ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ D ∈ ℋ
23 hvadd4 ⊢ A ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ D ∈ ℋ → A + ℎ -1 ⋅ ℎ C + ℎ B + ℎ -1 ⋅ ℎ D = A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ -1 ⋅ ℎ D
24 22 23 syl ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ -1 ⋅ ℎ C + ℎ B + ℎ -1 ⋅ ℎ D = A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ -1 ⋅ ℎ D
25 14 24 eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ D = A + ℎ -1 ⋅ ℎ C + ℎ B + ℎ -1 ⋅ ℎ D
26 9 25 eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A - ℎ C + ℎ B - ℎ D = A + ℎ B + ℎ -1 ⋅ ℎ C + ℎ D
27 4 26 eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A + ℎ B - ℎ C + ℎ D = A - ℎ C + ℎ B - ℎ D