Metamath Proof Explorer

Theorem hvsubass

Description: Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 neg1cn ⊢−1∈ℂ
2 hvmulcl ⊢−1∈ℂ∧B∈ℋ→-1⋅ℎB∈ℋ
3 1 2 mpan ⊢B∈ℋ→-1⋅ℎB∈ℋ
4 hvaddsubass ⊢A∈ℋ∧-1⋅ℎB∈ℋ∧C∈ℋ→A+ℎ-1⋅ℎB-ℎC=A+ℎ-1⋅ℎB-ℎC
5 3 4 syl3an2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎ-1⋅ℎB-ℎC=A+ℎ-1⋅ℎB-ℎC
6 hvsubval ⊢A∈ℋ∧B∈ℋ→A-ℎB=A+ℎ-1⋅ℎB
7 6 3adant3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=A+ℎ-1⋅ℎB
8 7 oveq1d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB-ℎC=A+ℎ-1⋅ℎB-ℎC
9 simp1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A∈ℋ
10 hvaddcl ⊢B∈ℋ∧C∈ℋ→B+ℎC∈ℋ
11 10 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→B+ℎC∈ℋ
12 hvsubval ⊢A∈ℋ∧B+ℎC∈ℋ→A-ℎB+ℎC=A+ℎ-1⋅ℎB+ℎC
13 9 11 12 syl2anc ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB+ℎC=A+ℎ-1⋅ℎB+ℎC
14 hvsubval ⊢-1⋅ℎB∈ℋ∧C∈ℋ→-1⋅ℎB-ℎC=-1⋅ℎB+ℎ-1⋅ℎC
15 3 14 sylan ⊢B∈ℋ∧C∈ℋ→-1⋅ℎB-ℎC=-1⋅ℎB+ℎ-1⋅ℎC
16 15 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→-1⋅ℎB-ℎC=-1⋅ℎB+ℎ-1⋅ℎC
17 ax-hvdistr1 ⊢−1∈ℂ∧B∈ℋ∧C∈ℋ→-1⋅ℎB+ℎC=-1⋅ℎB+ℎ-1⋅ℎC
18 1 17 mp3an1 ⊢B∈ℋ∧C∈ℋ→-1⋅ℎB+ℎC=-1⋅ℎB+ℎ-1⋅ℎC
19 18 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→-1⋅ℎB+ℎC=-1⋅ℎB+ℎ-1⋅ℎC
20 16 19 eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→-1⋅ℎB-ℎC=-1⋅ℎB+ℎC
21 20 oveq2d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎ-1⋅ℎB-ℎC=A+ℎ-1⋅ℎB+ℎC
22 13 21 eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB+ℎC=A+ℎ-1⋅ℎB-ℎC
23 5 8 22 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB-ℎC=A-ℎB+ℎC