his2sub

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	his2sub	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −_ℎ 𝐵 ) ·_ih 𝐶 ) = ( ( 𝐴 ·_ih 𝐶 ) − ( 𝐵 ·_ih 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hvsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −_ℎ 𝐵 ) = ( 𝐴 +_ℎ ( - 1 ·_ℎ 𝐵 ) ) )
2	1	oveq1d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 −_ℎ 𝐵 ) ·_ih 𝐶 ) = ( ( 𝐴 +_ℎ ( - 1 ·_ℎ 𝐵 ) ) ·_ih 𝐶 ) )
3	2	3adant3	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −_ℎ 𝐵 ) ·_ih 𝐶 ) = ( ( 𝐴 +_ℎ ( - 1 ·_ℎ 𝐵 ) ) ·_ih 𝐶 ) )
4		neg1cn	⊢ - 1 ∈ ℂ
5		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·_ℎ 𝐵 ) ∈ ℋ )
6	4 5	mpan	⊢ ( 𝐵 ∈ ℋ → ( - 1 ·_ℎ 𝐵 ) ∈ ℋ )
7		ax-his2	⊢ ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·_ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +_ℎ ( - 1 ·_ℎ 𝐵 ) ) ·_ih 𝐶 ) = ( ( 𝐴 ·_ih 𝐶 ) + ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) ) )
8	6 7	syl3an2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +_ℎ ( - 1 ·_ℎ 𝐵 ) ) ·_ih 𝐶 ) = ( ( 𝐴 ·_ih 𝐶 ) + ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) ) )
9		ax-his3	⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) = ( - 1 · ( 𝐵 ·_ih 𝐶 ) ) )
10	4 9	mp3an1	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) = ( - 1 · ( 𝐵 ·_ih 𝐶 ) ) )
11		hicl	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·_ih 𝐶 ) ∈ ℂ )
12	11	mulm1d	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( - 1 · ( 𝐵 ·_ih 𝐶 ) ) = - ( 𝐵 ·_ih 𝐶 ) )
13	10 12	eqtrd	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) = - ( 𝐵 ·_ih 𝐶 ) )
14	13	oveq2d	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·_ih 𝐶 ) + ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) ) = ( ( 𝐴 ·_ih 𝐶 ) + - ( 𝐵 ·_ih 𝐶 ) ) )
15	14	3adant1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·_ih 𝐶 ) + ( ( - 1 ·_ℎ 𝐵 ) ·_ih 𝐶 ) ) = ( ( 𝐴 ·_ih 𝐶 ) + - ( 𝐵 ·_ih 𝐶 ) ) )
16	8 15	eqtrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +_ℎ ( - 1 ·_ℎ 𝐵 ) ) ·_ih 𝐶 ) = ( ( 𝐴 ·_ih 𝐶 ) + - ( 𝐵 ·_ih 𝐶 ) ) )
17		hicl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐶 ) ∈ ℂ )
18	17	3adant2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐶 ) ∈ ℂ )
19	11	3adant1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·_ih 𝐶 ) ∈ ℂ )
20	18 19	negsubd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·_ih 𝐶 ) + - ( 𝐵 ·_ih 𝐶 ) ) = ( ( 𝐴 ·_ih 𝐶 ) − ( 𝐵 ·_ih 𝐶 ) ) )
21	3 16 20	3eqtrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −_ℎ 𝐵 ) ·_ih 𝐶 ) = ( ( 𝐴 ·_ih 𝐶 ) − ( 𝐵 ·_ih 𝐶 ) ) )

Metamath Proof Explorer

Theorem his2sub

Proof