rrx2linest - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrx2linest		Structured version Visualization version GIF version

Theorem rrx2linest 49947

Description: The line passing through the two different points 𝑋 and 𝑌 in a real Euclidean space of dimension 2 in "standard form". (Contributed by AV, 2-Feb-2023.)

**Hypotheses**
Ref	Expression
rrx2line.i	⊢ 𝐼 = (0..^2)
rrx2line.e	⊢ 𝐸 = (ℝ^‘𝐼)
rrx2line.b	⊢ 𝑃 = (ℝ ↑_m 𝐼)
rrx2line.l	⊢ 𝐿 = (Line_M‘𝐸)
rrx2linest.a	⊢ 𝐴 = ((𝑌‘0) − (𝑋‘0))
rrx2linest.b	⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1))
rrx2linest.c	⊢ 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))

**Assertion**
Ref	Expression
rrx2linest	⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})

Distinct variable groups: 𝐸,𝑝 𝐼,𝑝 𝑃,𝑝 𝑋,𝑝 𝑌,𝑝 Allowed substitution hints: 𝐴(𝑝) 𝐵(𝑝) 𝐶(𝑝) 𝐿(𝑝)

Proof of Theorem rrx2linest Dummy variables 𝑖 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1210	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → 𝑋 ∈ 𝑃)
2		simpl2 1211	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → 𝑌 ∈ 𝑃)
3		simpr 490	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋‘0) = (𝑌‘0))
4		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋‘0) = (𝑌‘0))
5	4	anim1i 627	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) ∧ (𝑋‘1) = (𝑌‘1)) → ((𝑋‘0) = (𝑌‘0) ∧ (𝑋‘1) = (𝑌‘1)))
6		rrx2line.i	. . . . . . . . . . . . . . 15 ⊢ 𝐼 = (0..^2)
7		fzo0to2pr 13888	. . . . . . . . . . . . . . 15 ⊢ (0..^2) = {0, 1}
8	6, 7	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ 𝐼 = {0, 1}
9	8	raleqi 3317	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ 𝐼 (𝑋‘𝑖) = (𝑌‘𝑖) ↔ ∀𝑖 ∈ {0, 1} (𝑋‘𝑖) = (𝑌‘𝑖))
10		c0ex 11303	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
11		1ex 11306	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
12		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (𝑋‘𝑖) = (𝑋‘0))
13		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (𝑌‘𝑖) = (𝑌‘0))
14	12, 13	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → ((𝑋‘𝑖) = (𝑌‘𝑖) ↔ (𝑋‘0) = (𝑌‘0)))
15		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝑋‘𝑖) = (𝑋‘1))
16		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝑌‘𝑖) = (𝑌‘1))
17	15, 16	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑋‘𝑖) = (𝑌‘𝑖) ↔ (𝑋‘1) = (𝑌‘1)))
18	10, 11, 14, 17	ralpr 4657	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ {0, 1} (𝑋‘𝑖) = (𝑌‘𝑖) ↔ ((𝑋‘0) = (𝑌‘0) ∧ (𝑋‘1) = (𝑌‘1)))
19	9, 18	bitri 278	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ 𝐼 (𝑋‘𝑖) = (𝑌‘𝑖) ↔ ((𝑋‘0) = (𝑌‘0) ∧ (𝑋‘1) = (𝑌‘1)))
20	5, 19	sylibr 237	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) ∧ (𝑋‘1) = (𝑌‘1)) → ∀𝑖 ∈ 𝐼 (𝑋‘𝑖) = (𝑌‘𝑖))
21		elmapfn 8890	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ (ℝ ↑_m 𝐼) → 𝑋 Fn 𝐼)
22		rrx2line.b	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
23	21, 22	eleq2s 2878	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝑃 → 𝑋 Fn 𝐼)
24		elmapfn 8890	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ∈ (ℝ ↑_m 𝐼) → 𝑌 Fn 𝐼)
25	24, 22	eleq2s 2878	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝑃 → 𝑌 Fn 𝐼)
26	23, 25	anim12i 625	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼))
27	26	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼))
28		eqfnfv 7029	. . . . . . . . . . . 12 ⊢ ((𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼) → (𝑋 = 𝑌 ↔ ∀𝑖 ∈ 𝐼 (𝑋‘𝑖) = (𝑌‘𝑖)))
29	27, 28	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋 = 𝑌 ↔ ∀𝑖 ∈ 𝐼 (𝑋‘𝑖) = (𝑌‘𝑖)))
30	20, 29	mpbird 260	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) ∧ (𝑋‘1) = (𝑌‘1)) → 𝑋 = 𝑌)
31	30	ex 418	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑋‘1) = (𝑌‘1) → 𝑋 = 𝑌))
32	31	necon3d 2976	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋 ≠ 𝑌 → (𝑋‘1) ≠ (𝑌‘1)))
33	32	ex 418	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘0) = (𝑌‘0) → (𝑋 ≠ 𝑌 → (𝑋‘1) ≠ (𝑌‘1))))
34	33	com23 87	. . . . . 6 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋 ≠ 𝑌 → ((𝑋‘0) = (𝑌‘0) → (𝑋‘1) ≠ (𝑌‘1))))
35	34	3impia 1135	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑋‘0) = (𝑌‘0) → (𝑋‘1) ≠ (𝑌‘1)))
36	35	imp 412	. . . 4 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋‘1) ≠ (𝑌‘1))
37		rrx2line.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
38		rrx2line.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
39	6, 37, 22, 38	rrx2vlinest 49946	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘0) = (𝑌‘0) ∧ (𝑋‘1) ≠ (𝑌‘1))) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)})
40	1, 2, 3, 36, 39	syl112anc 1401	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)})
41		simplr 781	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
42		simpr 490	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
43		simpll 779	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑋‘0) = (𝑌‘0))
44		rrx2linest.a	. . . . . . . . . . 11 ⊢ 𝐴 = ((𝑌‘0) − (𝑋‘0))
45	44	oveq1i 7430	. . . . . . . . . 10 ⊢ (𝐴 · (𝑝‘1)) = (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))
46	45	a1i 11	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝐴 · (𝑝‘1)) = (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)))
47		oveq2 7428	. . . . . . . . . . . 12 ⊢ ((𝑋‘0) = (𝑌‘0) → ((𝑌‘0) − (𝑋‘0)) = ((𝑌‘0) − (𝑌‘0)))
48	47	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑌‘0) − (𝑋‘0)) = ((𝑌‘0) − (𝑌‘0)))
49	6, 22	rrx2pxel 49916	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘0) ∈ ℝ)
50	49	recnd 11340	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘0) ∈ ℂ)
51	50	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘0) ∈ ℂ)
52	51	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑌‘0) ∈ ℂ)
53	52	subidd 11660	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑌‘0) − (𝑌‘0)) = 0)
54	48, 53	eqtrd 2795	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑌‘0) − (𝑋‘0)) = 0)
55	54	oveq1d 7435	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = (0 · (𝑝‘1)))
56	6, 22	rrx2pyel 49917	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
57	56	recnd 11340	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
58	57	ad2antlr 740	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑝‘1) ∈ ℂ)
59	58	mul02d 11511	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (0 · (𝑝‘1)) = 0)
60	46, 55, 59	3eqtrd 2799	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝐴 · (𝑝‘1)) = 0)
61		rrx2linest.b	. . . . . . . . . . 11 ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1))
62	61	oveq1i 7430	. . . . . . . . . 10 ⊢ (𝐵 · (𝑝‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0))
63	62	a1i 11	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝐵 · (𝑝‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)))
64		rrx2linest.c	. . . . . . . . . . 11 ⊢ 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))
65		oveq1 7427	. . . . . . . . . . . 12 ⊢ ((𝑋‘0) = (𝑌‘0) → ((𝑋‘0) · (𝑌‘1)) = ((𝑌‘0) · (𝑌‘1)))
66	65	oveq2d 7436	. . . . . . . . . . 11 ⊢ ((𝑋‘0) = (𝑌‘0) → (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))
67	64, 66	eqtrid 2807	. . . . . . . . . 10 ⊢ ((𝑋‘0) = (𝑌‘0) → 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))
68	67	adantl 487	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))
69	63, 68	oveq12d 7438	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝐵 · (𝑝‘0)) + 𝐶) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))))
70	60, 69	eqeq12d 2776	. . . . . . 7 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶) ↔ 0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))))
71	41, 42, 43, 70	syl21anc 851	. . . . . 6 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶) ↔ 0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))))
72	6, 22	rrx2pyel 49917	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ)
73	72	recnd 11340	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℂ)
74	73	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘1) ∈ ℂ)
75	51, 74	mulcomd 11333	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑌‘0) · (𝑌‘1)) = ((𝑌‘1) · (𝑌‘0)))
76	75	oveq2d 7436	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘1) · (𝑌‘0))))
77	6, 22	rrx2pyel 49917	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ)
78	77	recnd 11340	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℂ)
79	78	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘1) ∈ ℂ)
80	79, 74, 51	subdird 11776	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘1) · (𝑌‘0))))
81	76, 80	eqtr4d 2798	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))) = (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)))
82	81	ad2antlr 740	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))) = (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)))
83	82	oveq2d 7436	. . . . . . . 8 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))))
84	83	eqeq2d 2771	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))) ↔ 0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)))))
85		eqcom 2767	. . . . . . . . 9 ⊢ (0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) ↔ ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) = 0)
86	85	a1i 11	. . . . . . . 8 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) ↔ ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) = 0))
87	74	ad2antlr 740	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘1) ∈ ℂ)
88	79	ad2antlr 740	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑋‘1) ∈ ℂ)
89	87, 88	subcld 11672	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ∈ ℂ)
90	6, 22	rrx2pxel 49916	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℝ)
91	90	recnd 11340	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℂ)
92	91	adantl 487	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘0) ∈ ℂ)
93	89, 92	mulcld 11332	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) ∈ ℂ)
94	88, 87	subcld 11672	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑋‘1) − (𝑌‘1)) ∈ ℂ)
95	51	ad2antlr 740	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘0) ∈ ℂ)
96	94, 95	mulcld 11332	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) ∈ ℂ)
97		addeq0 11742	. . . . . . . . 9 ⊢ (((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) ∈ ℂ ∧ (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) ∈ ℂ) → (((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) = 0 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))))
98	93, 96, 97	syl2anc 596	. . . . . . . 8 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) = 0 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))))
99	94, 95	mulneg1d 11772	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ( -((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)))
100	88, 87	negsubdi2d 11688	. . . . . . . . . . . 12 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → -((𝑋‘1) − (𝑌‘1)) = ((𝑌‘1) − (𝑋‘1)))
101	100	oveq1d 7435	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ( -((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑌‘0)))
102	99, 101	eqtr3d 2797	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑌‘0)))
103	102	eqeq2d 2771	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑌‘0))))
104		ancom 466	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) ↔ ((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)))
105		necom 3008	. . . . . . . . . . . . 13 ⊢ ((𝑋‘1) ≠ (𝑌‘1) ↔ (𝑌‘1) ≠ (𝑋‘1))
106	36, 104, 105	3imtr3i 294	. . . . . . . . . . . 12 ⊢ (((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑌‘1) ≠ (𝑋‘1))
107	106	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘1) ≠ (𝑋‘1))
108	87, 88, 107	subne0d 11682	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ≠ 0)
109	92, 95, 89, 108	mulcand 11952	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑌‘0)) ↔ (𝑝‘0) = (𝑌‘0)))
110	103, 109	bitrd 282	. . . . . . . 8 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) ↔ (𝑝‘0) = (𝑌‘0)))
111	86, 98, 110	3bitrd 308	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))) ↔ (𝑝‘0) = (𝑌‘0)))
112	84, 111	bitrd 282	. . . . . 6 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))) ↔ (𝑝‘0) = (𝑌‘0)))
113		simpl 488	. . . . . . . . 9 ⊢ (((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑋‘0) = (𝑌‘0))
114	113	eqcomd 2766	. . . . . . . 8 ⊢ (((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑌‘0) = (𝑋‘0))
115	114	adantr 486	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘0) = (𝑋‘0))
116	115	eqeq2d 2771	. . . . . 6 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) = (𝑌‘0) ↔ (𝑝‘0) = (𝑋‘0)))
117	71, 112, 116	3bitrrd 309	. . . . 5 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) = (𝑋‘0) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)))
118	117	rabbidva 3418	. . . 4 ⊢ (((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)} = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
119	118	ancoms 464	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)} = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
120	40, 119	eqtrd 2795	. 2 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
121	6, 37, 22, 38	rrx2line 49945	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1))))})
122	121	adantr 486	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ ¬ (𝑋‘0) = (𝑌‘0)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1))))})
123		df-ne 2956	. . . . . . . 8 ⊢ ((𝑋‘0) ≠ (𝑌‘0) ↔ ¬ (𝑋‘0) = (𝑌‘0))
124	90	ad2antlr 740	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑝‘0) ∈ ℝ)
125	6, 22	rrx2pxel 49916	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘0) ∈ ℝ)
126	125	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘0) ∈ ℝ)
127	126	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑋‘0) ∈ ℝ)
128	49	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘0) ∈ ℝ)
129	128	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑌‘0) ∈ ℝ)
130		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑋‘0) ≠ (𝑌‘0))
131	56	ad2antlr 740	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑝‘1) ∈ ℝ)
132	77	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘1) ∈ ℝ)
133	132	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑋‘1) ∈ ℝ)
134	72	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘1) ∈ ℝ)
135	134	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑌‘1) ∈ ℝ)
136	124, 127, 129, 130, 131, 133, 135	affinecomb2 49908	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
137	44	eqcomi 2769	. . . . . . . . . . . 12 ⊢ ((𝑌‘0) − (𝑋‘0)) = 𝐴
138	137	oveq1i 7430	. . . . . . . . . . 11 ⊢ (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = (𝐴 · (𝑝‘1))
139	61	eqcomi 2769	. . . . . . . . . . . . 13 ⊢ ((𝑌‘1) − (𝑋‘1)) = 𝐵
140	139	oveq1i 7430	. . . . . . . . . . . 12 ⊢ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = (𝐵 · (𝑝‘0))
141	64	eqcomi 2769	. . . . . . . . . . . 12 ⊢ (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) = 𝐶
142	140, 141	oveq12i 7432	. . . . . . . . . . 11 ⊢ ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) = ((𝐵 · (𝑝‘0)) + 𝐶)
143	138, 142	eqeq12i 2778	. . . . . . . . . 10 ⊢ ((((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶))
144	136, 143	bitrdi 290	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)))
145	144	expcom 419	. . . . . . . 8 ⊢ ((𝑋‘0) ≠ (𝑌‘0) → (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶))))
146	123, 145	sylbir 238	. . . . . . 7 ⊢ (¬ (𝑋‘0) = (𝑌‘0) → (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶))))
147	146	expd 421	. . . . . 6 ⊢ (¬ (𝑋‘0) = (𝑌‘0) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑝 ∈ 𝑃 → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)))))
148	147	impcom 413	. . . . 5 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ ¬ (𝑋‘0) = (𝑌‘0)) → (𝑝 ∈ 𝑃 → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶))))
149	148	imp 412	. . . 4 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ ¬ (𝑋‘0) = (𝑌‘0)) ∧ 𝑝 ∈ 𝑃) → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)))
150	149	rabbidva 3418	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ ¬ (𝑋‘0) = (𝑌‘0)) → {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1))))} = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
151	122, 150	eqtrd 2795	. 2 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ ¬ (𝑋‘0) = (𝑌‘0)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
152	120, 151	pm2.61dan 825	1 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 {cpr 4586 Fn wfn 6533 ‘cfv 6538 (class class class)co 7420 ↑_m cmap 8850 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 + caddc 11206 · cmul 11208 − cmin 11544 -cneg 11545 2c2 12400 ..^cfzo 13791 ℝ^crrx 25709 Line_Mcline 49933

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281 ax-addf 11282 ax-mulf 11283

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8180 df-tpos 8246 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-er 8720 df-map 8852 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9357 df-sup 9437 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-8 12414 df-9 12415 df-n0 12610 df-z 12697 df-dec 12818 df-uz 12969 df-rp 13124 df-fz 13643 df-fzo 13792 df-seq 14148 df-exp 14208 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-struct 17330 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-starv 17448 df-sca 17449 df-vsca 17450 df-ip 17451 df-tset 17452 df-ple 17453 df-ds 17455 df-unif 17456 df-hom 17457 df-cco 17458 df-0g 17617 df-prds 17623 df-pws 17625 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-mhm 18983 df-grp 19152 df-minusg 19153 df-sbg 19154 df-subg 19338 df-ghm 19433 df-cmn 20001 df-abl 20002 df-mgp 20366 df-rng 20380 df-ur 20413 df-ring 20466 df-cring 20467 df-oppr 20572 df-dvdsr 20592 df-unit 20593 df-invr 20623 df-dvr 20636 df-rhm 20707 df-subrng 20803 df-subrg 20827 df-drng 20987 df-field 20988 df-staf 21101 df-srng 21102 df-lmod 21142 df-lss 21212 df-sra 21453 df-rgmod 21454 df-cnfld 21684 df-refld 21916 df-dsmm 22043 df-frlm 22058 df-tng 24908 df-tcph 25495 df-rrx 25711 df-line 49935

This theorem is used by: rrx2linest2 49949 line2x 49959 itsclinecirc0b 49979

W3C validator