This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℋ
hisubcom.2 ⊢ B ∈ ℋ
hisubcom.3 ⊢ C ∈ ℋ
hisubcom.4 ⊢ D ∈ ℋ
Assertion hisubcomi ⊢ A - ℎ B ⋅ ih C - ℎ D = B - ℎ A ⋅ ih D - ℎ C

Proof

Step Hyp Ref Expression
1 hisubcom.1 ⊢ A ∈ ℋ
2 hisubcom.2 ⊢ B ∈ ℋ
3 hisubcom.3 ⊢ C ∈ ℋ
4 hisubcom.4 ⊢ D ∈ ℋ
5 2 1 hvnegdii ⊢ -1 ⋅ ℎ B - ℎ A = A - ℎ B
6 4 3 hvnegdii ⊢ -1 ⋅ ℎ D - ℎ C = C - ℎ D
7 5 6 oveq12i ⊢ -1 ⋅ ℎ B - ℎ A ⋅ ih -1 ⋅ ℎ D - ℎ C = A - ℎ B ⋅ ih C - ℎ D
8 neg1cn ⊢ − 1 ∈ ℂ
9 2 1 hvsubcli ⊢ B - ℎ A ∈ ℋ
10 4 3 hvsubcli ⊢ D - ℎ C ∈ ℋ
11 8 8 9 10 his35i ⊢ -1 ⋅ ℎ B - ℎ A ⋅ ih -1 ⋅ ℎ D - ℎ C = -1 ⁢ − 1 ‾ ⁢ B - ℎ A ⋅ ih D - ℎ C
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 ‾ ⁢ B - ℎ A ⋅ ih D - ℎ C = 1 ⁢ B - ℎ A ⋅ ih D - ℎ C
21 9 10 hicli ⊢ B - ℎ A ⋅ ih D - ℎ C ∈ ℂ
22 21 mullidi ⊢ 1 ⁢ B - ℎ A ⋅ ih D - ℎ C = B - ℎ A ⋅ ih D - ℎ C
23 11 20 22 3eqtri ⊢ -1 ⋅ ℎ B - ℎ A ⋅ ih -1 ⋅ ℎ D - ℎ C = B - ℎ A ⋅ ih D - ℎ C
24 7 23 eqtr3i ⊢ A - ℎ B ⋅ ih C - ℎ D = B - ℎ A ⋅ ih D - ℎ C