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 50059

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 13912	. . . . . . . . . . . . . . 15 ⊢ (0..^2) = {0, 1}
8	6, 7	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ 𝐼 = {0, 1}
9	8	raleqi 3321	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ 𝐼 (𝑋‘𝑖) = (𝑌‘𝑖) ↔ ∀𝑖 ∈ {0, 1} (𝑋‘𝑖) = (𝑌‘𝑖))
10		c0ex 11327	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
11		1ex 11330	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
12		fveq2 6908	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (𝑋‘𝑖) = (𝑋‘0))
13		fveq2 6908	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (𝑌‘𝑖) = (𝑌‘0))
14	12, 13	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → ((𝑋‘𝑖) = (𝑌‘𝑖) ↔ (𝑋‘0) = (𝑌‘0)))
15		fveq2 6908	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝑋‘𝑖) = (𝑋‘1))
16		fveq2 6908	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝑌‘𝑖) = (𝑌‘1))
17	15, 16	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → ((𝑋‘𝑖) = (𝑌‘𝑖) ↔ (𝑋‘1) = (𝑌‘1)))
18	10, 11, 14, 17	ralpr 4661	. . . . . . . . . . . . 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 8915	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ (ℝ ↑_m 𝐼) → 𝑋 Fn 𝐼)
22		rrx2line.b	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
23	21, 22	eleq2s 2882	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝑃 → 𝑋 Fn 𝐼)
24		elmapfn 8915	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ∈ (ℝ ↑_m 𝐼) → 𝑌 Fn 𝐼)
25	24, 22	eleq2s 2882	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝑃 → 𝑌 Fn 𝐼)
26	23, 25	anim12i 625	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼))
27	26	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼))
28		eqfnfv 7052	. . . . . . . . . . . 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 2980	. . . . . . . 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 50058	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘0) = (𝑌‘0) ∧ (𝑋‘1) ≠ (𝑌‘1))) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)})
40	1, 2, 3, 36, 39	syl112anc 1402	. . 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 7453	. . . . . . . . . 10 ⊢ (𝐴 · (𝑝‘1)) = (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1))
46	45	a1i 11	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝐴 · (𝑝‘1)) = (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)))
47		oveq2 7451	. . . . . . . . . . . 12 ⊢ ((𝑋‘0) = (𝑌‘0) → ((𝑌‘0) − (𝑋‘0)) = ((𝑌‘0) − (𝑌‘0)))
48	47	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑌‘0) − (𝑋‘0)) = ((𝑌‘0) − (𝑌‘0)))
49	6, 22	rrx2pxel 50028	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘0) ∈ ℝ)
50	49	recnd 11364	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘0) ∈ ℂ)
51	50	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘0) ∈ ℂ)
52	51	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑌‘0) ∈ ℂ)
53	52	subidd 11684	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑌‘0) − (𝑌‘0)) = 0)
54	48, 53	eqtrd 2798	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝑌‘0) − (𝑋‘0)) = 0)
55	54	oveq1d 7458	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = (0 · (𝑝‘1)))
56	6, 22	rrx2pyel 50029	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
57	56	recnd 11364	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
58	57	ad2antlr 740	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑝‘1) ∈ ℂ)
59	58	mul02d 11535	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (0 · (𝑝‘1)) = 0)
60	46, 55, 59	3eqtrd 2802	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → (𝐴 · (𝑝‘1)) = 0)
61		rrx2linest.b	. . . . . . . . . . 11 ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1))
62	61	oveq1i 7453	. . . . . . . . . 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 7450	. . . . . . . . . . . 12 ⊢ ((𝑋‘0) = (𝑌‘0) → ((𝑋‘0) · (𝑌‘1)) = ((𝑌‘0) · (𝑌‘1)))
66	65	oveq2d 7459	. . . . . . . . . . 11 ⊢ ((𝑋‘0) = (𝑌‘0) → (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))
67	64, 66	eqtrid 2810	. . . . . . . . . 10 ⊢ ((𝑋‘0) = (𝑌‘0) → 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))
68	67	adantl 487	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → 𝐶 = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))))
69	63, 68	oveq12d 7461	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) = (𝑌‘0)) → ((𝐵 · (𝑝‘0)) + 𝐶) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))))
70	60, 69	eqeq12d 2779	. . . . . . 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 50029	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ)
73	72	recnd 11364	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℂ)
74	73	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘1) ∈ ℂ)
75	51, 74	mulcomd 11357	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑌‘0) · (𝑌‘1)) = ((𝑌‘1) · (𝑌‘0)))
76	75	oveq2d 7459	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1))) = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘1) · (𝑌‘0))))
77	6, 22	rrx2pyel 50029	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ)
78	77	recnd 11364	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℂ)
79	78	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘1) ∈ ℂ)
80	79, 74, 51	subdird 11800	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘1) · (𝑌‘0))))
81	76, 80	eqtr4d 2801	. . . . . . . . . 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 7459	. . . . . . . 8 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0))))
84	83	eqeq2d 2774	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑌‘0) · (𝑌‘1)))) ↔ 0 = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)))))
85		eqcom 2770	. . . . . . . . 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 11696	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ∈ ℂ)
90	6, 22	rrx2pxel 50028	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℝ)
91	90	recnd 11364	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℂ)
92	91	adantl 487	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘0) ∈ ℂ)
93	89, 92	mulcld 11356	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) ∈ ℂ)
94	88, 87	subcld 11696	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑋‘1) − (𝑌‘1)) ∈ ℂ)
95	51	ad2antlr 740	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘0) ∈ ℂ)
96	94, 95	mulcld 11356	. . . . . . . . 9 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) ∈ ℂ)
97		addeq0 11766	. . . . . . . . 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 11796	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ( -((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)))
100	88, 87	negsubdi2d 11712	. . . . . . . . . . . 12 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → -((𝑋‘1) − (𝑌‘1)) = ((𝑌‘1) − (𝑋‘1)))
101	100	oveq1d 7458	. . . . . . . . . . 11 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ( -((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑌‘0)))
102	99, 101	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → -(((𝑋‘1) − (𝑌‘1)) · (𝑌‘0)) = (((𝑌‘1) − (𝑋‘1)) · (𝑌‘0)))
103	102	eqeq2d 2774	. . . . . . . . 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 3012	. . . . . . . . . . . . 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 11706	. . . . . . . . . 10 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ≠ 0)
109	92, 95, 89, 108	mulcand 11976	. . . . . . . . 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 2769	. . . . . . . 8 ⊢ (((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → (𝑌‘0) = (𝑋‘0))
115	114	adantr 486	. . . . . . 7 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘0) = (𝑋‘0))
116	115	eqeq2d 2774	. . . . . 6 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) = (𝑌‘0) ↔ (𝑝‘0) = (𝑋‘0)))
117	71, 112, 116	3bitrrd 309	. . . . 5 ⊢ ((((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) = (𝑋‘0) ↔ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)))
118	117	rabbidva 3422	. . . 4 ⊢ (((𝑋‘0) = (𝑌‘0) ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)} = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
119	118	ancoms 464	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘0) = (𝑋‘0)} = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
120	40, 119	eqtrd 2798	. 2 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑋‘0) = (𝑌‘0)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
121	6, 37, 22, 38	rrx2line 50057	. . . 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 2960	. . . . . . . 8 ⊢ ((𝑋‘0) ≠ (𝑌‘0) ↔ ¬ (𝑋‘0) = (𝑌‘0))
124	90	ad2antlr 740	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑝‘0) ∈ ℝ)
125	6, 22	rrx2pxel 50028	. . . . . . . . . . . . 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 50020	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ 𝑝 ∈ 𝑃) ∧ (𝑋‘0) ≠ (𝑌‘0)) → (∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1)))) ↔ (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))))))
137	44	eqcomi 2772	. . . . . . . . . . . 12 ⊢ ((𝑌‘0) − (𝑋‘0)) = 𝐴
138	137	oveq1i 7453	. . . . . . . . . . 11 ⊢ (((𝑌‘0) − (𝑋‘0)) · (𝑝‘1)) = (𝐴 · (𝑝‘1))
139	61	eqcomi 2772	. . . . . . . . . . . . 13 ⊢ ((𝑌‘1) − (𝑋‘1)) = 𝐵
140	139	oveq1i 7453	. . . . . . . . . . . 12 ⊢ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) = (𝐵 · (𝑝‘0))
141	64	eqcomi 2772	. . . . . . . . . . . 12 ⊢ (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1))) = 𝐶
142	140, 141	oveq12i 7455	. . . . . . . . . . 11 ⊢ ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘0)) + (((𝑋‘1) · (𝑌‘0)) − ((𝑋‘0) · (𝑌‘1)))) = ((𝐵 · (𝑝‘0)) + 𝐶)
143	138, 142	eqeq12i 2781	. . . . . . . . . 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 3422	. . 3 ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ ¬ (𝑋‘0) = (𝑌‘0)) → {𝑝 ∈ 𝑃 ∣ ∃𝑡 ∈ ℝ ((𝑝‘0) = (((1 − 𝑡) · (𝑋‘0)) + (𝑡 · (𝑌‘0))) ∧ (𝑝‘1) = (((1 − 𝑡) · (𝑋‘1)) + (𝑡 · (𝑌‘1))))} = {𝑝 ∈ 𝑃 ∣ (𝐴 · (𝑝‘1)) = ((𝐵 · (𝑝‘0)) + 𝐶)})
151	122, 150	eqtrd 2798	. 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 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 {cpr 4590 Fn wfn 6553 ‘cfv 6558 (class class class)co 7443 ↑_m cmap 8875 ℂcc 11225 ℝcr 11226 0cc0 11227 1c1 11228 + caddc 11230 · cmul 11232 − cmin 11568 -cneg 11569 2c2 12424 ..^cfzo 13815 ℝ^crrx 25734 Line_Mcline 50045

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305 ax-addf 11306 ax-mulf 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-er 8745 df-map 8877 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-sup 9461 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-z 12721 df-dec 12842 df-uz 12993 df-rp 13148 df-fz 13667 df-fzo 13816 df-seq 14172 df-exp 14232 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-sca 17473 df-vsca 17474 df-ip 17475 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-hom 17481 df-cco 17482 df-0g 17641 df-prds 17647 df-pws 17649 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-grp 19176 df-minusg 19177 df-sbg 19178 df-subg 19362 df-ghm 19457 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-ring 20491 df-cring 20492 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-rhm 20732 df-subrng 20828 df-subrg 20852 df-drng 21012 df-field 21013 df-staf 21126 df-srng 21127 df-lmod 21167 df-lss 21237 df-sra 21478 df-rgmod 21479 df-cnfld 21709 df-refld 21941 df-dsmm 22068 df-frlm 22083 df-tng 24933 df-tcph 25520 df-rrx 25736 df-line 50047

This theorem is used by: rrx2linest2 50061 line2x 50071 itsclinecirc0b 50091

W3C validator