rrx2linest

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

	Ref	Expression
Hypotheses	rrx2line.i	$⊢ I = \{1, 2\}$
	rrx2line.e	$⊢ E = I$
	rrx2line.b	$⊢ P = ℝ^{I}$
	rrx2line.l	$⊢ L = {Line}_{M} (E)$
	rrx2linest.a	$⊢ A = Y (1) - X (1)$
	rrx2linest.b	$⊢ B = Y (2) - X (2)$
	rrx2linest.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
Assertion	rrx2linest	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| A p (2) = B p (1) + C\}$

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	$⊢ I = \{1, 2\}$
2		rrx2line.e	$⊢ E = I$
3		rrx2line.b	$⊢ P = ℝ^{I}$
4		rrx2line.l	$⊢ L = {Line}_{M} (E)$
5		rrx2linest.a	$⊢ A = Y (1) - X (1)$
6		rrx2linest.b	$⊢ B = Y (2) - X (2)$
7		rrx2linest.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
8		simpl1	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to X \in P$
9		simpl2	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to Y \in P$
10		simpr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to X (1) = Y (1)$
11		simpr	$⊢ ((X \in P \land Y \in P) \land X (1) = Y (1)) \to X (1) = Y (1)$
12	11	anim1i	$⊢ (((X \in P \land Y \in P) \land X (1) = Y (1)) \land X (2) = Y (2)) \to (X (1) = Y (1) \land X (2) = Y (2))$
13	1	raleqi	$⊢ \forall i \in I X (i) = Y (i) \leftrightarrow \forall i \in \{1, 2\} X (i) = Y (i)$
14		1ex	$⊢ 1 \in V$
15		2ex	$⊢ 2 \in V$
16		fveq2	$⊢ i = 1 \to X (i) = X (1)$
17		fveq2	$⊢ i = 1 \to Y (i) = Y (1)$
18	16 17	eqeq12d	$⊢ i = 1 \to (X (i) = Y (i) \leftrightarrow X (1) = Y (1))$
19		fveq2	$⊢ i = 2 \to X (i) = X (2)$
20		fveq2	$⊢ i = 2 \to Y (i) = Y (2)$
21	19 20	eqeq12d	$⊢ i = 2 \to (X (i) = Y (i) \leftrightarrow X (2) = Y (2))$
22	14 15 18 21	ralpr	$⊢ \forall i \in \{1, 2\} X (i) = Y (i) \leftrightarrow (X (1) = Y (1) \land X (2) = Y (2))$
23	13 22	bitri	$⊢ \forall i \in I X (i) = Y (i) \leftrightarrow (X (1) = Y (1) \land X (2) = Y (2))$
24	12 23	sylibr	$⊢ (((X \in P \land Y \in P) \land X (1) = Y (1)) \land X (2) = Y (2)) \to \forall i \in I X (i) = Y (i)$
25		elmapfn	$⊢ X \in (ℝ^{I}) \to X Fn I$
26	25 3	eleq2s	$⊢ X \in P \to X Fn I$
27		elmapfn	$⊢ Y \in (ℝ^{I}) \to Y Fn I$
28	27 3	eleq2s	$⊢ Y \in P \to Y Fn I$
29	26 28	anim12i	$⊢ (X \in P \land Y \in P) \to (X Fn I \land Y Fn I)$
30	29	ad2antrr	$⊢ (((X \in P \land Y \in P) \land X (1) = Y (1)) \land X (2) = Y (2)) \to (X Fn I \land Y Fn I)$
31		eqfnfv	$⊢ (X Fn I \land Y Fn I) \to (X = Y \leftrightarrow \forall i \in I X (i) = Y (i))$
32	30 31	syl	$⊢ (((X \in P \land Y \in P) \land X (1) = Y (1)) \land X (2) = Y (2)) \to (X = Y \leftrightarrow \forall i \in I X (i) = Y (i))$
33	24 32	mpbird	$⊢ (((X \in P \land Y \in P) \land X (1) = Y (1)) \land X (2) = Y (2)) \to X = Y$
34	33	ex	$⊢ ((X \in P \land Y \in P) \land X (1) = Y (1)) \to (X (2) = Y (2) \to X = Y)$
35	34	necon3d	$⊢ ((X \in P \land Y \in P) \land X (1) = Y (1)) \to (X \neq Y \to X (2) \neq Y (2))$
36	35	ex	$⊢ (X \in P \land Y \in P) \to (X (1) = Y (1) \to (X \neq Y \to X (2) \neq Y (2)))$
37	36	com23	$⊢ (X \in P \land Y \in P) \to (X \neq Y \to (X (1) = Y (1) \to X (2) \neq Y (2)))$
38	37	3impia	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (1) = Y (1) \to X (2) \neq Y (2))$
39	38	imp	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to X (2) \neq Y (2)$
40	1 2 3 4	rrx2vlinest	$⊢ (X \in P \land Y \in P \land (X (1) = Y (1) \land X (2) \neq Y (2))) \to X L Y = \{p \in P \| p (1) = X (1)\}$
41	8 9 10 39 40	syl112anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to X L Y = \{p \in P \| p (1) = X (1)\}$
42		ancom	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \leftrightarrow (X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y))$
43		simplr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (X \in P \land Y \in P \land X \neq Y)$
44		simpr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to p \in P$
45		simpll	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to X (1) = Y (1)$
46	5	oveq1i	$⊢ A p (2) = (Y (1) - X (1)) p (2)$
47	46	a1i	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to A p (2) = (Y (1) - X (1)) p (2)$
48		oveq2	$⊢ X (1) = Y (1) \to Y (1) - X (1) = Y (1) - Y (1)$
49	48	adantl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to Y (1) - X (1) = Y (1) - Y (1)$
50	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
51	50	recnd	$⊢ Y \in P \to Y (1) \in ℂ$
52	51	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) \in ℂ$
53	52	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to Y (1) \in ℂ$
54	53	subidd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to Y (1) - Y (1) = 0$
55	49 54	eqtrd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to Y (1) - X (1) = 0$
56	55	oveq1d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to (Y (1) - X (1)) p (2) = 0 \cdot p (2)$
57	1 3	rrx2pyel	$⊢ p \in P \to p (2) \in ℝ$
58	57	recnd	$⊢ p \in P \to p (2) \in ℂ$
59	58	ad2antlr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to p (2) \in ℂ$
60	59	mul02d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to 0 \cdot p (2) = 0$
61	47 56 60	3eqtrd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to A p (2) = 0$
62	6	oveq1i	$⊢ B p (1) = (Y (2) - X (2)) p (1)$
63	62	a1i	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to B p (1) = (Y (2) - X (2)) p (1)$
64		oveq1	$⊢ X (1) = Y (1) \to X (1) Y (2) = Y (1) Y (2)$
65	64	oveq2d	$⊢ X (1) = Y (1) \to X (2) Y (1) - X (1) Y (2) = X (2) Y (1) - Y (1) Y (2)$
66	7 65	eqtrid	$⊢ X (1) = Y (1) \to C = X (2) Y (1) - Y (1) Y (2)$
67	66	adantl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to C = X (2) Y (1) - Y (1) Y (2)$
68	63 67	oveq12d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to B p (1) + C = (Y (2) - X (2)) p (1) + X (2) Y (1) - Y (1) Y (2)$
69	61 68	eqeq12d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) = Y (1)) \to (A p (2) = B p (1) + C \leftrightarrow 0 = (Y (2) - X (2)) p (1) + X (2) Y (1) - Y (1) Y (2))$
70	43 44 45 69	syl21anc	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (A p (2) = B p (1) + C \leftrightarrow 0 = (Y (2) - X (2)) p (1) + X (2) Y (1) - Y (1) Y (2))$
71	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
72	71	recnd	$⊢ Y \in P \to Y (2) \in ℂ$
73	72	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) \in ℂ$
74	52 73	mulcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) Y (2) = Y (2) Y (1)$
75	74	oveq2d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) Y (1) - Y (1) Y (2) = X (2) Y (1) - Y (2) Y (1)$
76	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
77	76	recnd	$⊢ X \in P \to X (2) \in ℂ$
78	77	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) \in ℂ$
79	78 73 52	subdird	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (2) - Y (2)) Y (1) = X (2) Y (1) - Y (2) Y (1)$
80	75 79	eqtr4d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) Y (1) - Y (1) Y (2) = (X (2) - Y (2)) Y (1)$
81	80	ad2antlr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to X (2) Y (1) - Y (1) Y (2) = (X (2) - Y (2)) Y (1)$
82	81	oveq2d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (Y (2) - X (2)) p (1) + X (2) Y (1) - Y (1) Y (2) = (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1)$
83	82	eqeq2d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (0 = (Y (2) - X (2)) p (1) + X (2) Y (1) - Y (1) Y (2) \leftrightarrow 0 = (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1))$
84		eqcom	$⊢ 0 = (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) \leftrightarrow (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) = 0$
85	84	a1i	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (0 = (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) \leftrightarrow (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) = 0)$
86	73	ad2antlr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to Y (2) \in ℂ$
87	78	ad2antlr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to X (2) \in ℂ$
88	86 87	subcld	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to Y (2) - X (2) \in ℂ$
89	1 3	rrx2pxel	$⊢ p \in P \to p (1) \in ℝ$
90	89	recnd	$⊢ p \in P \to p (1) \in ℂ$
91	90	adantl	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to p (1) \in ℂ$
92	88 91	mulcld	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (Y (2) - X (2)) p (1) \in ℂ$
93	87 86	subcld	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to X (2) - Y (2) \in ℂ$
94	52	ad2antlr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to Y (1) \in ℂ$
95	93 94	mulcld	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (X (2) - Y (2)) Y (1) \in ℂ$
96		addeq0	$⊢ ((Y (2) - X (2)) p (1) \in ℂ \land (X (2) - Y (2)) Y (1) \in ℂ) \to ((Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) = 0 \leftrightarrow (Y (2) - X (2)) p (1) = - (X (2) - Y (2)) Y (1))$
97	92 95 96	syl2anc	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to ((Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) = 0 \leftrightarrow (Y (2) - X (2)) p (1) = - (X (2) - Y (2)) Y (1))$
98	93 94	mulneg1d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (- (X (2) - Y (2))) Y (1) = - (X (2) - Y (2)) Y (1)$
99	87 86	negsubdi2d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to - (X (2) - Y (2)) = Y (2) - X (2)$
100	99	oveq1d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (- (X (2) - Y (2))) Y (1) = (Y (2) - X (2)) Y (1)$
101	98 100	eqtr3d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to - (X (2) - Y (2)) Y (1) = (Y (2) - X (2)) Y (1)$
102	101	eqeq2d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to ((Y (2) - X (2)) p (1) = - (X (2) - Y (2)) Y (1) \leftrightarrow (Y (2) - X (2)) p (1) = (Y (2) - X (2)) Y (1))$
103		necom	$⊢ X (2) \neq Y (2) \leftrightarrow Y (2) \neq X (2)$
104	39 42 103	3imtr3i	$⊢ (X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \to Y (2) \neq X (2)$
105	104	adantr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to Y (2) \neq X (2)$
106	86 87 105	subne0d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to Y (2) - X (2) \neq 0$
107	91 94 88 106	mulcand	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to ((Y (2) - X (2)) p (1) = (Y (2) - X (2)) Y (1) \leftrightarrow p (1) = Y (1))$
108	102 107	bitrd	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to ((Y (2) - X (2)) p (1) = - (X (2) - Y (2)) Y (1) \leftrightarrow p (1) = Y (1))$
109	85 97 108	3bitrd	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (0 = (Y (2) - X (2)) p (1) + (X (2) - Y (2)) Y (1) \leftrightarrow p (1) = Y (1))$
110	83 109	bitrd	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (0 = (Y (2) - X (2)) p (1) + X (2) Y (1) - Y (1) Y (2) \leftrightarrow p (1) = Y (1))$
111		simpl	$⊢ (X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \to X (1) = Y (1)$
112	111	eqcomd	$⊢ (X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \to Y (1) = X (1)$
113	112	adantr	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to Y (1) = X (1)$
114	113	eqeq2d	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (p (1) = Y (1) \leftrightarrow p (1) = X (1))$
115	70 110 114	3bitrrd	$⊢ ((X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (p (1) = X (1) \leftrightarrow A p (2) = B p (1) + C)$
116	115	rabbidva	$⊢ (X (1) = Y (1) \land (X \in P \land Y \in P \land X \neq Y)) \to \{p \in P \| p (1) = X (1)\} = \{p \in P \| A p (2) = B p (1) + C\}$
117	42 116	sylbi	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to \{p \in P \| p (1) = X (1)\} = \{p \in P \| A p (2) = B p (1) + C\}$
118	41 117	eqtrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land X (1) = Y (1)) \to X L Y = \{p \in P \| A p (2) = B p (1) + C\}$
119	1 2 3 4	rrx2line	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| \exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\}$
120	119	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land \neg X (1) = Y (1)) \to X L Y = \{p \in P \| \exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\}$
121		df-ne	$⊢ X (1) \neq Y (1) \leftrightarrow \neg X (1) = Y (1)$
122	89	ad2antlr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to p (1) \in ℝ$
123	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
124	123	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (1) \in ℝ$
125	124	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to X (1) \in ℝ$
126	50	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) \in ℝ$
127	126	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to Y (1) \in ℝ$
128		simpr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to X (1) \neq Y (1)$
129	57	ad2antlr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to p (2) \in ℝ$
130	76	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) \in ℝ$
131	130	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to X (2) \in ℝ$
132	71	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) \in ℝ$
133	132	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to Y (2) \in ℝ$
134	122 125 127 128 129 131 133	affinecomb2	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2))$
135	5	eqcomi	$⊢ Y (1) - X (1) = A$
136	135	oveq1i	$⊢ (Y (1) - X (1)) p (2) = A p (2)$
137	6	eqcomi	$⊢ Y (2) - X (2) = B$
138	137	oveq1i	$⊢ (Y (2) - X (2)) p (1) = B p (1)$
139	7	eqcomi	$⊢ X (2) Y (1) - X (1) Y (2) = C$
140	138 139	oveq12i	$⊢ (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2) = B p (1) + C$
141	136 140	eqeq12i	$⊢ (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2) \leftrightarrow A p (2) = B p (1) + C$
142	134 141	bitrdi	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land X (1) \neq Y (1)) \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow A p (2) = B p (1) + C)$
143	142	expcom	$⊢ X (1) \neq Y (1) \to (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow A p (2) = B p (1) + C))$
144	121 143	sylbir	$⊢ \neg X (1) = Y (1) \to (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow A p (2) = B p (1) + C))$
145	144	expd	$⊢ \neg X (1) = Y (1) \to ((X \in P \land Y \in P \land X \neq Y) \to (p \in P \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow A p (2) = B p (1) + C)))$
146	145	impcom	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land \neg X (1) = Y (1)) \to (p \in P \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow A p (2) = B p (1) + C))$
147	146	imp	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land \neg X (1) = Y (1)) \land p \in P) \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow A p (2) = B p (1) + C)$
148	147	rabbidva	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land \neg X (1) = Y (1)) \to \{p \in P \| \exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\} = \{p \in P \| A p (2) = B p (1) + C\}$
149	120 148	eqtrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land \neg X (1) = Y (1)) \to X L Y = \{p \in P \| A p (2) = B p (1) + C\}$
150	118 149	pm2.61dan	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| A p (2) = B p (1) + C\}$

Metamath Proof Explorer

Theorem rrx2linest

Proof