hisubcomi

Description: Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hisubcom.1	⊢ 𝐴 ∈ ℋ
	hisubcom.2	⊢ 𝐵 ∈ ℋ
	hisubcom.3	⊢ 𝐶 ∈ ℋ
	hisubcom.4	⊢ 𝐷 ∈ ℋ
Assertion	hisubcomi	⊢ ( ( 𝐴 −_ℎ 𝐵 ) ·_ih ( 𝐶 −_ℎ 𝐷 ) ) = ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		hisubcom.1	⊢ 𝐴 ∈ ℋ
2		hisubcom.2	⊢ 𝐵 ∈ ℋ
3		hisubcom.3	⊢ 𝐶 ∈ ℋ
4		hisubcom.4	⊢ 𝐷 ∈ ℋ
5	2 1	hvnegdii	⊢ ( - 1 ·_ℎ ( 𝐵 −_ℎ 𝐴 ) ) = ( 𝐴 −_ℎ 𝐵 )
6	4 3	hvnegdii	⊢ ( - 1 ·_ℎ ( 𝐷 −_ℎ 𝐶 ) ) = ( 𝐶 −_ℎ 𝐷 )
7	5 6	oveq12i	⊢ ( ( - 1 ·_ℎ ( 𝐵 −_ℎ 𝐴 ) ) ·_ih ( - 1 ·_ℎ ( 𝐷 −_ℎ 𝐶 ) ) ) = ( ( 𝐴 −_ℎ 𝐵 ) ·_ih ( 𝐶 −_ℎ 𝐷 ) )
8		neg1cn	⊢ - 1 ∈ ℂ
9	2 1	hvsubcli	⊢ ( 𝐵 −_ℎ 𝐴 ) ∈ ℋ
10	4 3	hvsubcli	⊢ ( 𝐷 −_ℎ 𝐶 ) ∈ ℋ
11	8 8 9 10	his35i	⊢ ( ( - 1 ·_ℎ ( 𝐵 −_ℎ 𝐴 ) ) ·_ih ( - 1 ·_ℎ ( 𝐷 −_ℎ 𝐶 ) ) ) = ( ( - 1 · ( ∗ ‘ - 1 ) ) · ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) ) )
12		neg1rr	⊢ - 1 ∈ ℝ
13		cjre	⊢ ( - 1 ∈ ℝ → ( ∗ ‘ - 1 ) = - 1 )
14	12 13	ax-mp	⊢ ( ∗ ‘ - 1 ) = - 1
15	14	oveq2i	⊢ ( - 1 · ( ∗ ‘ - 1 ) ) = ( - 1 · - 1 )
16		ax-1cn	⊢ 1 ∈ ℂ
17	16 16	mul2negi	⊢ ( - 1 · - 1 ) = ( 1 · 1 )
18		1t1e1	⊢ ( 1 · 1 ) = 1
19	15 17 18	3eqtri	⊢ ( - 1 · ( ∗ ‘ - 1 ) ) = 1
20	19	oveq1i	⊢ ( ( - 1 · ( ∗ ‘ - 1 ) ) · ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) ) ) = ( 1 · ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) ) )
21	9 10	hicli	⊢ ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) ) ∈ ℂ
22	21	mullidi	⊢ ( 1 · ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) ) ) = ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) )
23	11 20 22	3eqtri	⊢ ( ( - 1 ·_ℎ ( 𝐵 −_ℎ 𝐴 ) ) ·_ih ( - 1 ·_ℎ ( 𝐷 −_ℎ 𝐶 ) ) ) = ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) )
24	7 23	eqtr3i	⊢ ( ( 𝐴 −_ℎ 𝐵 ) ·_ih ( 𝐶 −_ℎ 𝐷 ) ) = ( ( 𝐵 −_ℎ 𝐴 ) ·_ih ( 𝐷 −_ℎ 𝐶 ) )

Metamath Proof Explorer

Theorem hisubcomi

Proof