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