This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) −ℎ 𝐶 ) = ( 𝐴 −ℎ ( 𝐵 +ℎ 𝐶 ) ) )

Proof

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