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