Metamath Proof Explorer

Theorem hvaddsubass

Description: Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 neg1cn ⊢−1∈ℂ
2 hvmulcl ⊢−1∈ℂ∧C∈ℋ→-1⋅ℎC∈ℋ
3 1 2 mpan ⊢C∈ℋ→-1⋅ℎC∈ℋ
4 ax-hvass ⊢A∈ℋ∧B∈ℋ∧-1⋅ℎC∈ℋ→A+ℎB+ℎ-1⋅ℎC=A+ℎB+ℎ-1⋅ℎC
5 3 4 syl3an3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎ-1⋅ℎC=A+ℎB+ℎ-1⋅ℎC
6 hvaddcl ⊢A∈ℋ∧B∈ℋ→A+ℎB∈ℋ
7 hvsubval ⊢A+ℎB∈ℋ∧C∈ℋ→A+ℎB-ℎC=A+ℎB+ℎ-1⋅ℎC
8 6 7 stoic3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB-ℎC=A+ℎB+ℎ-1⋅ℎC
9 hvsubval ⊢B∈ℋ∧C∈ℋ→B-ℎC=B+ℎ-1⋅ℎC
10 9 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→B-ℎC=B+ℎ-1⋅ℎC
11 10 oveq2d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB-ℎC=A+ℎB+ℎ-1⋅ℎC
12 5 8 11 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB-ℎC=A+ℎB-ℎC