Theorem colinearalglem2 26970

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

Assertion

Ref	Expression
colinearalglem2	⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))

Distinct variable groups:   𝐴,𝑖,𝑗   𝐵,𝑖,𝑗   𝐶,𝑖,𝑗   𝑖,𝑁,𝑗

Proof of Theorem colinearalglem2

Step	Hyp	Ref	Expression
1		simp1 1138	. . . 4 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
2		simpl 486	. . . 4 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
3		fveecn 26965	. . . 4 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
4	1, 2, 3	syl2an 599	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → (𝐴‘𝑖) ∈ ℂ)
5		simp2 1139	. . . 4 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
6		fveecn 26965	. . . 4 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
7	5, 2, 6	syl2an 599	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → (𝐵‘𝑖) ∈ ℂ)
8		simp3 1140	. . . 4 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
9		fveecn 26965	. . . 4 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
10	8, 2, 9	syl2an 599	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → (𝐶‘𝑖) ∈ ℂ)
11		simpr 488	. . . 4 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
12		fveecn 26965	. . . 4 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐴‘𝑗) ∈ ℂ)
13	1, 11, 12	syl2an 599	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → (𝐴‘𝑗) ∈ ℂ)
14		fveecn 26965	. . . 4 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐵‘𝑗) ∈ ℂ)
15	5, 11, 14	syl2an 599	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → (𝐵‘𝑗) ∈ ℂ)
16		fveecn 26965	. . . 4 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐶‘𝑗) ∈ ℂ)
17	8, 11, 16	syl2an 599	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → (𝐶‘𝑗) ∈ ℂ)
18		simp1 1138	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → (𝐴‘𝑖) ∈ ℂ)
19		simp3 1140	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ) → (𝐶‘𝑗) ∈ ℂ)
20		mulcl 10796	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ) → ((𝐴‘𝑖) · (𝐶‘𝑗)) ∈ ℂ)
21	18, 19, 20	syl2an 599	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((𝐴‘𝑖) · (𝐶‘𝑗)) ∈ ℂ)
22		simp2 1139	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → (𝐵‘𝑖) ∈ ℂ)
23		simp1 1138	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ) → (𝐴‘𝑗) ∈ ℂ)
24		mulcl 10796	. . . . . . . . . . . 12 ⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐴‘𝑗) ∈ ℂ) → ((𝐵‘𝑖) · (𝐴‘𝑗)) ∈ ℂ)
25	22, 23, 24	syl2an 599	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((𝐵‘𝑖) · (𝐴‘𝑗)) ∈ ℂ)
26	21, 25	addcld 10835	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) ∈ ℂ)
27		mulcl 10796	. . . . . . . . . . 11 ⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ) → ((𝐵‘𝑖) · (𝐶‘𝑗)) ∈ ℂ)
28	22, 19, 27	syl2an 599	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((𝐵‘𝑖) · (𝐶‘𝑗)) ∈ ℂ)
29	26, 28	subcld 11172	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) ∈ ℂ)
30		simp2 1139	. . . . . . . . . 10 ⊢ (((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ) → (𝐵‘𝑗) ∈ ℂ)
31		mulcl 10796	. . . . . . . . . 10 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ) → ((𝐴‘𝑖) · (𝐵‘𝑗)) ∈ ℂ)
32	18, 30, 31	syl2an 599	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((𝐴‘𝑖) · (𝐵‘𝑗)) ∈ ℂ)
33		simp3 1140	. . . . . . . . . . 11 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → (𝐶‘𝑖) ∈ ℂ)
34		mulcl 10796	. . . . . . . . . . 11 ⊢ (((𝐶‘𝑖) ∈ ℂ ∧ (𝐴‘𝑗) ∈ ℂ) → ((𝐶‘𝑖) · (𝐴‘𝑗)) ∈ ℂ)
35	33, 23, 34	syl2an 599	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((𝐶‘𝑖) · (𝐴‘𝑗)) ∈ ℂ)
36		mulcl 10796	. . . . . . . . . . 11 ⊢ (((𝐶‘𝑖) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ) → ((𝐶‘𝑖) · (𝐵‘𝑗)) ∈ ℂ)
37	33, 30, 36	syl2an 599	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((𝐶‘𝑖) · (𝐵‘𝑗)) ∈ ℂ)
38	35, 37	subcld 11172	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ∈ ℂ)
39	29, 32, 38	subadd2d 11191	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗)))))
40		eqcom 2741	. . . . . . . 8 ⊢ (((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) ↔ ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗))))
41	39, 40	bitrdi 290	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗)))))
42	35, 32, 37	addsubd 11193	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) · (𝐴‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗))))
43	35, 32	addcomd 11017	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐶‘𝑖) · (𝐴‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))))
44	43	oveq1d 7217	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) · (𝐴‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))) = ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))))
45	42, 44	eqtr3d 2776	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗))) = ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))))
46	45	eqeq2d 2745	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) + ((𝐴‘𝑖) · (𝐵‘𝑗))) ↔ ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗)))))
47	41, 46	bitrd 282	. . . . . 6 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗)))))
48	26, 28, 32	subsub4d 11203	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))))
49	28, 32	addcld 10835	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) ∈ ℂ)
50	21, 49, 25	subsub3d 11202	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) − ((((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗)))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))))
51	28, 25, 32	subsub3d 11202	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗)))) = ((((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗))))
52	51	eqcomd 2740	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗))) = (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗)))))
53	52	oveq2d 7218	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) − ((((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗)))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗))))))
54	25, 32	subcld 11172	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗))) ∈ ℂ)
55	21, 28, 54	subsubd 11200	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗))))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) + (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗)))))
56	53, 55	eqtrd 2774	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) − ((((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗)))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) + (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗)))))
57	48, 50, 56	3eqtr2d 2780	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) + (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗)))))
58	21, 28	subcld 11172	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) ∈ ℂ)
59	58, 25, 32	addsub12d 11195	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) + (((𝐵‘𝑖) · (𝐴‘𝑗)) − ((𝐴‘𝑖) · (𝐵‘𝑗)))) = (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗)))))
60	21, 28, 32	subsub4d 11203	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))))
61	60	oveq2d 7218	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((((𝐴‘𝑖) · (𝐶‘𝑗)) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗)))) = (((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))))
62	57, 59, 61	3eqtrd 2778	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))))
63	62	eqeq1d 2736	. . . . . 6 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) − ((𝐴‘𝑖) · (𝐵‘𝑗))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ (((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗)))))
64	32, 35	addcld 10835	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) ∈ ℂ)
65		subeqrev 11237	. . . . . . 7 ⊢ ((((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) ∈ ℂ ∧ ((𝐵‘𝑖) · (𝐶‘𝑗)) ∈ ℂ) ∧ ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) ∈ ℂ ∧ ((𝐶‘𝑖) · (𝐵‘𝑗)) ∈ ℂ)) → (((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗)))) = (((𝐶‘𝑖) · (𝐵‘𝑗)) − (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))))))
66	26, 28, 64, 37, 65	syl22anc 839	. . . . . 6 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐵‘𝑖) · (𝐶‘𝑗))) = ((((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗)))) = (((𝐶‘𝑖) · (𝐵‘𝑗)) − (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))))))
67	47, 63, 66	3bitr3rd 313	. . . . 5 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗)))) = (((𝐶‘𝑖) · (𝐵‘𝑗)) − (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗)))) ↔ (((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗)))))
68	21, 49	subcld 11172	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))) ∈ ℂ)
69	25, 68, 38	addrsub 11232	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗)))))
70	35, 37, 25	sub32d 11204	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))))
71	35, 25, 37	subsub4d 11203	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐵‘𝑖) · (𝐴‘𝑗))) − ((𝐶‘𝑖) · (𝐵‘𝑗))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))))
72	70, 71	eqtrd 2774	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))))
73	72	eqeq2d 2745	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))) = ((((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) − ((𝐵‘𝑖) · (𝐴‘𝑗))) ↔ (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗))))))
74	69, 73	bitrd 282	. . . . . 6 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗))))))
75		eqcom 2741	. . . . . 6 ⊢ ((((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))) ↔ (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗)))))
76	74, 75	bitrdi 290	. . . . 5 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) · (𝐴‘𝑗)) + (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))) = (((𝐶‘𝑖) · (𝐴‘𝑗)) − ((𝐶‘𝑖) · (𝐵‘𝑗))) ↔ (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))))
77	67, 76	bitrd 282	. . . 4 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗)))) = (((𝐶‘𝑖) · (𝐵‘𝑗)) − (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗)))) ↔ (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))))
78		colinearalglem1 26969	. . . 4 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ (((𝐵‘𝑖) · (𝐶‘𝑗)) − (((𝐴‘𝑖) · (𝐶‘𝑗)) + ((𝐵‘𝑖) · (𝐴‘𝑗)))) = (((𝐶‘𝑖) · (𝐵‘𝑗)) − (((𝐴‘𝑖) · (𝐵‘𝑗)) + ((𝐶‘𝑖) · (𝐴‘𝑗))))))
79		3anrot 1102	. . . . 5 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ↔ ((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ ∧ (𝐴‘𝑖) ∈ ℂ))
80		3anrot 1102	. . . . 5 ⊢ (((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ) ↔ ((𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ ∧ (𝐴‘𝑗) ∈ ℂ))
81		colinearalglem1 26969	. . . . 5 ⊢ ((((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ ∧ (𝐴‘𝑖) ∈ ℂ) ∧ ((𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ ∧ (𝐴‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ↔ (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))))
82	79, 80, 81	syl2anb 601	. . . 4 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ↔ (((𝐶‘𝑖) · (𝐴‘𝑗)) − (((𝐵‘𝑖) · (𝐴‘𝑗)) + ((𝐶‘𝑖) · (𝐵‘𝑗)))) = (((𝐴‘𝑖) · (𝐶‘𝑗)) − (((𝐵‘𝑖) · (𝐶‘𝑗)) + ((𝐴‘𝑖) · (𝐵‘𝑗))))))
83	77, 78, 82	3bitr4d 314	. . 3 ⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑗) ∈ ℂ ∧ (𝐵‘𝑗) ∈ ℂ ∧ (𝐶‘𝑗) ∈ ℂ)) → ((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ (((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))
84	4, 7, 10, 13, 15, 17, 83	syl33anc 1387	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁))) → ((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ (((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))
85	84	2ralbidva 3112	1 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  ∀wral 3054  ‘cfv 6369  (class class class)co 7202  ℂcc 10710  1c1 10713   + caddc 10715   · cmul 10717   − cmin 11045  ...cfz 13078  𝔼cee 26951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-po 5457  df-so 5458  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-er 8380  df-map 8499  df-en 8616  df-dom 8617  df-sdom 8618  df-pnf 10852  df-mnf 10853  df-ltxr 10855  df-sub 11047  df-neg 11048  df-ee 26954

This theorem is referenced by:  colinearalglem3  26971  colinearalg  26973