Metamath Proof Explorer

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 ℋ$
hisubcom.2 ${⊢}{B}\in ℋ$
hisubcom.3 ${⊢}{C}\in ℋ$
hisubcom.4 ${⊢}{D}\in ℋ$
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 ℋ$
2 hisubcom.2 ${⊢}{B}\in ℋ$
3 hisubcom.3 ${⊢}{C}\in ℋ$
4 hisubcom.4 ${⊢}{D}\in ℋ$
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 ℋ$
10 4 3 hvsubcli ${⊢}{D}{-}_{ℎ}{C}\in ℋ$
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\stackrel{‾}{-1}\left(\left({B}{-}_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}\left({D}{-}_{ℎ}{C}\right)\right)$
12 neg1rr ${⊢}-1\in ℝ$
13 cjre ${⊢}-1\in ℝ\to \stackrel{‾}{-1}=-1$
14 12 13 ax-mp ${⊢}\stackrel{‾}{-1}=-1$
15 14 oveq2i ${⊢}-1\stackrel{‾}{-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\stackrel{‾}{-1}=1$
20 19 oveq1i ${⊢}-1\stackrel{‾}{-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)$