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 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∀ i ∈ 1 … N ∀ j ∈ 1 … N B ⁡ i − A ⁡ i ⁢ C ⁡ j − A ⁡ j = B ⁡ j − A ⁡ j ⁢ C ⁡ i − A ⁡ i ↔ ∀ i ∈ 1 … N ∀ j ∈ 1 … N C ⁡ i − B ⁡ i ⁢ A ⁡ j − B ⁡ j = C ⁡ j − B ⁡ j ⁢ A ⁡ i − B ⁡ i

Proof

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