Metamath Proof Explorer

Theorem his2sub2

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		his2sub	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) = ( ( 𝐵 ·_ih 𝐴 ) − ( 𝐶 ·_ih 𝐴 ) ) )
2	1	fveq2d	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) ) = ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) − ( 𝐶 ·_ih 𝐴 ) ) ) )
3		hicl	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·_ih 𝐴 ) ∈ ℂ )
4		hicl	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐶 ·_ih 𝐴 ) ∈ ℂ )
5		cjsub	⊢ ( ( ( 𝐵 ·_ih 𝐴 ) ∈ ℂ ∧ ( 𝐶 ·_ih 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) − ( 𝐶 ·_ih 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) − ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
6	3 4 5	syl2an	⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) ) → ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) − ( 𝐶 ·_ih 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) − ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
7	6	3impdir	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) − ( 𝐶 ·_ih 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) − ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
8	2 7	eqtrd	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) − ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
9	8	3comr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) − ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
10		hvsubcl	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 −_ℎ 𝐶 ) ∈ ℋ )
11		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐵 −_ℎ 𝐶 ) ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 −_ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) ) )
12	10 11	sylan2	⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ) → ( 𝐴 ·_ih ( 𝐵 −_ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) ) )
13	12	3impb	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 −_ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐵 −_ℎ 𝐶 ) ·_ih 𝐴 ) ) )
14		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·_ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) )
15	14	3adant3	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) )
16		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐶 ) = ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) )
17	16	3adant2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐶 ) = ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) )
18	15 17	oveq12d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·_ih 𝐵 ) − ( 𝐴 ·_ih 𝐶 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) − ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
19	9 13 18	3eqtr4d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 −_ℎ 𝐶 ) ) = ( ( 𝐴 ·_ih 𝐵 ) − ( 𝐴 ·_ih 𝐶 ) ) )