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 = \{1, 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 (1) = Y (1) \land X (2) \neq Y (2))) \to X L Y = \{p \in P \| p (1) = X (1)\}$

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

Metamath Proof Explorer

Theorem rrx2vlinest

Proof