Metamath Proof Explorer

Theorem colinearalglem3

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

Ref Expression
Assertion colinearalglem3 ⊢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…NA⁡i−C⁡i⁢B⁡j−C⁡j=A⁡j−C⁡j⁢B⁡i−C⁡i

Proof

Step Hyp Ref Expression
1 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
2 colinearalglem2 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→∀i∈1…N∀j∈1…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i↔∀i∈1…N∀j∈1…NA⁡i−C⁡i⁢B⁡j−C⁡j=A⁡j−C⁡j⁢B⁡i−C⁡i
3 2 3comr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…N∀j∈1…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i↔∀i∈1…N∀j∈1…NA⁡i−C⁡i⁢B⁡j−C⁡j=A⁡j−C⁡j⁢B⁡i−C⁡i
4 1 3 bitrd ⊢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…NA⁡i−C⁡i⁢B⁡j−C⁡j=A⁡j−C⁡j⁢B⁡i−C⁡i