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 = (0 ..^2)$
	rrx2line.e	$⊢ E = I$
	rrx2line.b	$⊢ P = ℝ^{I}$
	rrx2line.l	$⊢ L = {Line}_{M} (E)$
	rrx2linest.a	$⊢ A = Y (0) - X (0)$
	rrx2linest.b	$⊢ B = Y (1) - X (1)$
	rrx2linest.c	$⊢ C = X (1) Y (0) - X (0) Y (1)$
Assertion	rrx2linest	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| A p (1) = B p (0) + C\}$

Proof

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

Metamath Proof Explorer

Theorem rrx2linest

Proof