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