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 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) )