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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…N∀j∈1…NC⁡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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…N∀j∈1…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i