Metamath Proof Explorer

Theorem hvpncan

Description: Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvaddcl ⊢A∈ℋ∧B∈ℋ→A+ℎB∈ℋ
2 hvsubval ⊢A+ℎB∈ℋ∧B∈ℋ→A+ℎB-ℎB=A+ℎB+ℎ-1⋅ℎB
3 1 2 sylancom ⊢A∈ℋ∧B∈ℋ→A+ℎB-ℎB=A+ℎB+ℎ-1⋅ℎB
4 neg1cn ⊢−1∈ℂ
5 hvmulcl ⊢−1∈ℂ∧B∈ℋ→-1⋅ℎB∈ℋ
6 4 5 mpan ⊢B∈ℋ→-1⋅ℎB∈ℋ
7 6 ancli ⊢B∈ℋ→B∈ℋ∧-1⋅ℎB∈ℋ
8 ax-hvass ⊢A∈ℋ∧B∈ℋ∧-1⋅ℎB∈ℋ→A+ℎB+ℎ-1⋅ℎB=A+ℎB+ℎ-1⋅ℎB
9 8 3expb ⊢A∈ℋ∧B∈ℋ∧-1⋅ℎB∈ℋ→A+ℎB+ℎ-1⋅ℎB=A+ℎB+ℎ-1⋅ℎB
10 7 9 sylan2 ⊢A∈ℋ∧B∈ℋ→A+ℎB+ℎ-1⋅ℎB=A+ℎB+ℎ-1⋅ℎB
11 hvnegid ⊢B∈ℋ→B+ℎ-1⋅ℎB=0ℎ
12 11 oveq2d ⊢B∈ℋ→A+ℎB+ℎ-1⋅ℎB=A+ℎ0ℎ
13 ax-hvaddid ⊢A∈ℋ→A+ℎ0ℎ=A
14 12 13 sylan9eqr ⊢A∈ℋ∧B∈ℋ→A+ℎB+ℎ-1⋅ℎB=A
15 3 10 14 3eqtrd ⊢A∈ℋ∧B∈ℋ→A+ℎB-ℎB=A