Metamath Proof Explorer

Theorem colinearalglem2

Description: Lemma for colinearalg . Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion colinearalglem2 ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
2 simpl ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
3 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
4 1 2 3 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
5 simp2 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
6 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
7 5 2 6 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
8 simp3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
9 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
10 8 2 9 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
11 simpr ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
12 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
13 1 11 12 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
14 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ℂ )
15 5 11 14 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ℂ )
16 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
17 8 11 16 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
18 simp1 ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
19 simp3 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
20 mulcl ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
21 18 19 20 syl2an ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
22 simp2 ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
23 simp1 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
24 mulcl ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
25 22 23 24 syl2an ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
26 21 25 addcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ∈ ℂ )
27 mulcl ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
28 22 19 27 syl2an ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
29 26 28 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℂ )
30 simp2 ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) → ( 𝐵 ‘ 𝑗 ) ∈ ℂ )
31 mulcl ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ∈ ℂ )
32 18 30 31 syl2an ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ∈ ℂ )
33 simp3 ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
34 mulcl ⊢ ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
35 33 23 34 syl2an ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ∈ ℂ )
36 mulcl ⊢ ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ) → ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ∈ ℂ )
37 33 30 36 syl2an ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ∈ ℂ )
38 35 37 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ∈ ℂ )
39 29 32 38 subadd2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) ) )
40 eqcom ⊢ ( ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) ↔ ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) )
41 39 40 bitrdi ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
42 35 32 37 addsubd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) )
43 35 32 addcomd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) )
44 43 oveq1d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) )
45 42 44 eqtr3d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) )
46 45 eqeq2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
47 41 46 bitrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
48 26 28 32 subsub4d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
49 28 32 addcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ∈ ℂ )
50 21 49 25 subsub3d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
51 28 25 32 subsub3d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) )
52 51 eqcomd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
53 52 oveq2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
54 25 32 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ∈ ℂ )
55 21 28 54 subsubd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) + ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
56 53 55 eqtrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) + ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
57 48 50 56 3eqtr2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) + ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
58 21 28 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℂ )
59 58 25 32 addsub12d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) + ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
60 21 28 32 subsub4d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
61 60 oveq2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
62 57 59 61 3eqtrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
63 62 eqeq1d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) − ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
64 32 35 addcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ∈ ℂ )
65 subeqrev ⊢ ( ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ∈ ℂ ∧ ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ ) ∧ ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ∈ ℂ ∧ ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ∈ ℂ ) ) → ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) ) )
66 26 28 64 37 65 syl22anc ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) ) )
67 47 63 66 3bitr3rd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
68 21 49 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ∈ ℂ )
69 25 68 38 addrsub ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) )
70 35 37 25 sub32d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) )
71 35 25 37 subsub4d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
72 70 71 eqtrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
73 72 eqeq2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) − ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
74 69 73 bitrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
75 eqcom ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) )
76 74 75 bitrdi ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
77 67 76 bitrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
78 colinearalglem1 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) − ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) ) ) ) )
79 3anrot ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ↔ ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑖 ) ∈ ℂ ) )
80 3anrot ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ↔ ( ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) )
81 colinearalglem1 ⊢ ( ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
82 79 80 81 syl2anb ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐴 ‘ 𝑗 ) ) + ( ( 𝐶 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) − ( ( ( 𝐵 ‘ 𝑖 ) · ( 𝐶 ‘ 𝑗 ) ) + ( ( 𝐴 ‘ 𝑖 ) · ( 𝐵 ‘ 𝑗 ) ) ) ) ) )
83 77 78 82 3bitr4d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑗 ) ∈ ℂ ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) )
84 4 7 10 13 15 17 83 syl33anc ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) )
85 84 2ralbidva ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) )