rrx2vlinest

Description: The vertical 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)$
Assertion	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)\}$

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		fveq1	$⊢ X = Y \to X (1) = Y (1)$
6	5	necon3i	$⊢ X (1) \neq Y (1) \to X \neq Y$
7	6	adantl	$⊢ (X (0) = Y (0) \land X (1) \neq Y (1)) \to X \neq Y$
8	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))\}$
9	7 8	syl3an3	$⊢ (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 \| \exists t \in ℝ (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1))\}$
10		oveq2	$⊢ Y (0) = X (0) \to t Y (0) = t X (0)$
11	10	oveq2d	$⊢ Y (0) = X (0) \to (1 - t) X (0) + t Y (0) = (1 - t) X (0) + t X (0)$
12	11	eqcoms	$⊢ X (0) = Y (0) \to (1 - t) X (0) + t Y (0) = (1 - t) X (0) + t X (0)$
13	12	adantr	$⊢ (X (0) = Y (0) \land X (1) \neq Y (1)) \to (1 - t) X (0) + t Y (0) = (1 - t) X (0) + t X (0)$
14	13	3ad2ant3	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to (1 - t) X (0) + t Y (0) = (1 - t) X (0) + t X (0)$
15	14	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to (1 - t) X (0) + t Y (0) = (1 - t) X (0) + t X (0)$
16	15	adantr	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to (1 - t) X (0) + t Y (0) = (1 - t) X (0) + t X (0)$
17	1 3	rrx2pxel	$⊢ X \in P \to X (0) \in ℝ$
18	17	recnd	$⊢ X \in P \to X (0) \in ℂ$
19	18	3ad2ant1	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to X (0) \in ℂ$
20	19	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to X (0) \in ℂ$
21	20	adantr	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to X (0) \in ℂ$
22		recn	$⊢ t \in ℝ \to t \in ℂ$
23	22	adantl	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to t \in ℂ$
24	21 23	affineid	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to (1 - t) X (0) + t X (0) = X (0)$
25	16 24	eqtrd	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to (1 - t) X (0) + t Y (0) = X (0)$
26	25	eqeq2d	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to (p (0) = (1 - t) X (0) + t Y (0) \leftrightarrow p (0) = X (0))$
27	26	anbi1d	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to ((p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1)) \leftrightarrow (p (0) = X (0) \land p (1) = (1 - t) X (1) + t Y (1)))$
28	27	rexbidva	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \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 \exists t \in ℝ (p (0) = X (0) \land p (1) = (1 - t) X (1) + t Y (1)))$
29		simpl	$⊢ (p (0) = X (0) \land p (1) = (1 - t) X (1) + t Y (1)) \to p (0) = X (0)$
30	29	a1i	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land t \in ℝ) \to ((p (0) = X (0) \land p (1) = (1 - t) X (1) + t Y (1)) \to p (0) = X (0))$
31	1 3	rrx2pyel	$⊢ p \in P \to p (1) \in ℝ$
32	31	adantl	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to p (1) \in ℝ$
33	1 3	rrx2pyel	$⊢ X \in P \to X (1) \in ℝ$
34	33	3ad2ant1	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to X (1) \in ℝ$
35	34	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to X (1) \in ℝ$
36	32 35	resubcld	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to p (1) - X (1) \in ℝ$
37	1 3	rrx2pyel	$⊢ Y \in P \to Y (1) \in ℝ$
38	37	3ad2ant2	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to Y (1) \in ℝ$
39	38 34	resubcld	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to Y (1) - X (1) \in ℝ$
40	39	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to Y (1) - X (1) \in ℝ$
41	37	recnd	$⊢ Y \in P \to Y (1) \in ℂ$
42	41	3ad2ant2	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to Y (1) \in ℂ$
43	33	recnd	$⊢ X \in P \to X (1) \in ℂ$
44	43	3ad2ant1	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to X (1) \in ℂ$
45		simpr	$⊢ (X (0) = Y (0) \land X (1) \neq Y (1)) \to X (1) \neq Y (1)$
46	45	necomd	$⊢ (X (0) = Y (0) \land X (1) \neq Y (1)) \to Y (1) \neq X (1)$
47	46	3ad2ant3	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to Y (1) \neq X (1)$
48	42 44 47	subne0d	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to Y (1) - X (1) \neq 0$
49	48	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to Y (1) - X (1) \neq 0$
50	36 40 49	redivcld	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to \frac{p (1) - X (1)}{Y (1) - X (1)} \in ℝ$
51	50	adantr	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land p (0) = X (0)) \to \frac{p (1) - X (1)}{Y (1) - X (1)} \in ℝ$
52		simpr	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land p (0) = X (0)) \to p (0) = X (0)$
53	43	mullidd	$⊢ X \in P \to 1 X (1) = X (1)$
54	53	3ad2ant1	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to 1 X (1) = X (1)$
55	54	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to 1 X (1) = X (1)$
56	36	recnd	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to p (1) - X (1) \in ℂ$
57	41	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℂ$
58	43	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℂ$
59	57 58	subcld	$⊢ (X \in P \land Y \in P) \to Y (1) - X (1) \in ℂ$
60	59	3adant3	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \to Y (1) - X (1) \in ℂ$
61	60	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to Y (1) - X (1) \in ℂ$
62	56 61 49	divcan1d	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to (\frac{p (1) - X (1)}{Y (1) - X (1)}) (Y (1) - X (1)) = p (1) - X (1)$
63	55 62	oveq12d	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to 1 X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) (Y (1) - X (1)) = X (1) + p (1) - X (1)$
64	44	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to X (1) \in ℂ$
65	31	recnd	$⊢ p \in P \to p (1) \in ℂ$
66	65	adantl	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to p (1) \in ℂ$
67	64 66	pncan3d	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to X (1) + p (1) - X (1) = p (1)$
68	63 67	eqtr2d	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to p (1) = 1 X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) (Y (1) - X (1))$
69	68	adantr	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land p (0) = X (0)) \to p (1) = 1 X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) (Y (1) - X (1))$
70		1cnd	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to 1 \in ℂ$
71	50	recnd	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to \frac{p (1) - X (1)}{Y (1) - X (1)} \in ℂ$
72	42	adantr	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to Y (1) \in ℂ$
73	70 71 64 72	submuladdmuld	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1) = 1 X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) (Y (1) - X (1))$
74	73	adantr	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land p (0) = X (0)) \to (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1) = 1 X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) (Y (1) - X (1))$
75	69 74	eqtr4d	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land p (0) = X (0)) \to p (1) = (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1)$
76	52 75	jca	$⊢ (((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \land p (0) = X (0)) \to (p (0) = X (0) \land p (1) = (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1))$
77		oveq2	$⊢ t = \frac{p (1) - X (1)}{Y (1) - X (1)} \to 1 - t = 1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})$
78	77	oveq1d	$⊢ t = \frac{p (1) - X (1)}{Y (1) - X (1)} \to (1 - t) X (1) = (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1)$
79		oveq1	$⊢ t = \frac{p (1) - X (1)}{Y (1) - X (1)} \to t Y (1) = (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1)$
80	78 79	oveq12d	$⊢ t = \frac{p (1) - X (1)}{Y (1) - X (1)} \to (1 - t) X (1) + t Y (1) = (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1)$
81	80	eqeq2d	$⊢ t = \frac{p (1) - X (1)}{Y (1) - X (1)} \to (p (1) = (1 - t) X (1) + t Y (1) \leftrightarrow p (1) = (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1))$
82	81	anbi2d	$⊢ t = \frac{p (1) - X (1)}{Y (1) - X (1)} \to ((p (0) = X (0) \land p (1) = (1 - t) X (1) + t Y (1)) \leftrightarrow (p (0) = X (0) \land p (1) = (1 - (\frac{p (1) - X (1)}{Y (1) - X (1)})) X (1) + (\frac{p (1) - X (1)}{Y (1) - X (1)}) Y (1)))$
83	30 51 76 82	rspceb2dv	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \land p \in P) \to (\exists t \in ℝ (p (0) = X (0) \land p (1) = (1 - t) X (1) + t Y (1)) \leftrightarrow p (0) = X (0))$
84	28 83	bitrd	$⊢ ((X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \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 p (0) = X (0))$
85	84	rabbidva	$⊢ (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1))) \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 \| p (0) = X (0)\}$
86	9 85	eqtrd	$⊢ (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)\}$

Metamath Proof Explorer

Theorem rrx2vlinest

Proof