Theorem 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	$$⊢A\in \mathscr{H}$$
	hisubcom.2	$$⊢B\in \mathscr{H}$$
	hisubcom.3	$$⊢C\in \mathscr{H}$$
	hisubcom.4	$$⊢D\in \mathscr{H}$$
Assertion	hisubcomi	$$⊢\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(C{-}_{ℎ}D\right)=\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		hisubcom.1	$$⊢A\in \mathscr{H}$$
2		hisubcom.2	$$⊢B\in \mathscr{H}$$
3		hisubcom.3	$$⊢C\in \mathscr{H}$$
4		hisubcom.4	$$⊢D\in \mathscr{H}$$
5	2 1	hvnegdii	$$⊢-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)=A{-}_{ℎ}B$$
6	4 3	hvnegdii	$$⊢-1{\cdot }_{ℎ}\left(D{-}_{ℎ}C\right)=C{-}_{ℎ}D$$
7	5 6	oveq12i	$$⊢\left(-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}\left(D{-}_{ℎ}C\right)\right)=\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(C{-}_{ℎ}D\right)$$
8		neg1cn	$$⊢-1\in ℂ$$
9	2 1	hvsubcli	$$⊢B{-}_{ℎ}A\in \mathscr{H}$$
10	4 3	hvsubcli	$$⊢D{-}_{ℎ}C\in \mathscr{H}$$
11	8 8 9 10	his35i	$$⊢\left(-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}\left(D{-}_{ℎ}C\right)\right)=-1\overline{-1}\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)\right)$$
12		neg1rr	$$⊢-1\in ℝ$$
13		cjre	$$⊢-1\in ℝ\to \overline{-1}=-1$$
14	12 13	ax-mp	$$⊢\overline{-1}=-1$$
15	14	oveq2i	$$⊢-1\overline{-1}=-1-1$$
16		ax-1cn	$$⊢1\in ℂ$$
17	16 16	mul2negi	$$⊢-1-1=1\cdot 1$$
18		1t1e1	$$⊢1\cdot 1=1$$
19	15 17 18	3eqtri	$$⊢-1\overline{-1}=1$$
20	19	oveq1i	$$⊢-1\overline{-1}\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)\right)=1\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)\right)$$
21	9 10	hicli	$$⊢\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)\in ℂ$$
22	21	mulid2i	$$⊢1\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)\right)=\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)$$
23	11 20 22	3eqtri	$$⊢\left(-1{\cdot }_{ℎ}\left(B{-}_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(-1{\cdot }_{ℎ}\left(D{-}_{ℎ}C\right)\right)=\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)$$
24	7 23	eqtr3i	$$⊢\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(C{-}_{ℎ}D\right)=\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(D{-}_{ℎ}C\right)$$