line2y

Description: Example for a vertical line G passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023)

	Ref	Expression
Hypotheses	line2.i	$⊢ I = \{1, 2\}$
	line2.e	$⊢ E = I$
	line2.p	$⊢ P = ℝ^{I}$
	line2.l	$⊢ L = {Line}_{M} (E)$
	line2.g	$⊢ G = \{p \in P \| A p (1) + B p (2) = C\}$
	line2y.x	$⊢ X = \{⟨1, 0⟩, ⟨2, M⟩\}$
	line2y.y	$⊢ Y = \{⟨1, 0⟩, ⟨2, N⟩\}$
Assertion	line2y	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (G = X L Y \leftrightarrow (A \neq 0 \land B = 0 \land C = 0))$

Proof

Step	Hyp	Ref	Expression
1		line2.i	$⊢ I = \{1, 2\}$
2		line2.e	$⊢ E = I$
3		line2.p	$⊢ P = ℝ^{I}$
4		line2.l	$⊢ L = {Line}_{M} (E)$
5		line2.g	$⊢ G = \{p \in P \| A p (1) + B p (2) = C\}$
6		line2y.x	$⊢ X = \{⟨1, 0⟩, ⟨2, M⟩\}$
7		line2y.y	$⊢ Y = \{⟨1, 0⟩, ⟨2, N⟩\}$
8	5	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to G = \{p \in P \| A p (1) + B p (2) = C\}$
9		1ex	$⊢ 1 \in V$
10		2ex	$⊢ 2 \in V$
11	9 10	pm3.2i	$⊢ (1 \in V \land 2 \in V)$
12		c0ex	$⊢ 0 \in V$
13	12	jctl	$⊢ M \in ℝ \to (0 \in V \land M \in ℝ)$
14		1ne2	$⊢ 1 \neq 2$
15	14	a1i	$⊢ M \in ℝ \to 1 \neq 2$
16		fprg	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ \{0, M\}$
17		0red	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to 0 \in ℝ$
18		simp2r	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to M \in ℝ$
19	17 18	prssd	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to \{0, M\} \subseteq ℝ$
20	16 19	fssd	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
21	11 13 15 20	mp3an2i	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
22	1	feq2i	$⊢ \{⟨1, 0⟩, ⟨2, M⟩\} : I ⟶ ℝ \leftrightarrow \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
23	21 22	sylibr	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} : I ⟶ ℝ$
24		reex	$⊢ ℝ \in V$
25		prex	$⊢ \{1, 2\} \in V$
26	1 25	eqeltri	$⊢ I \in V$
27	24 26	elmap	$⊢ \{⟨1, 0⟩, ⟨2, M⟩\} \in (ℝ^{I}) \leftrightarrow \{⟨1, 0⟩, ⟨2, M⟩\} : I ⟶ ℝ$
28	23 27	sylibr	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} \in (ℝ^{I})$
29	28 6 3	3eltr4g	$⊢ M \in ℝ \to X \in P$
30	29	3ad2ant1	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X \in P$
31	12	jctl	$⊢ N \in ℝ \to (0 \in V \land N \in ℝ)$
32	14	a1i	$⊢ N \in ℝ \to 1 \neq 2$
33		fprg	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land N \in ℝ) \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, N⟩\} : \{1, 2\} ⟶ \{0, N\}$
34	11 31 32 33	mp3an2i	$⊢ N \in ℝ \to \{⟨1, 0⟩, ⟨2, N⟩\} : \{1, 2\} ⟶ \{0, N\}$
35		0re	$⊢ 0 \in ℝ$
36		prssi	$⊢ (0 \in ℝ \land N \in ℝ) \to \{0, N\} \subseteq ℝ$
37	35 36	mpan	$⊢ N \in ℝ \to \{0, N\} \subseteq ℝ$
38	34 37	fssd	$⊢ N \in ℝ \to \{⟨1, 0⟩, ⟨2, N⟩\} : \{1, 2\} ⟶ ℝ$
39	1	feq2i	$⊢ \{⟨1, 0⟩, ⟨2, N⟩\} : I ⟶ ℝ \leftrightarrow \{⟨1, 0⟩, ⟨2, N⟩\} : \{1, 2\} ⟶ ℝ$
40	38 39	sylibr	$⊢ N \in ℝ \to \{⟨1, 0⟩, ⟨2, N⟩\} : I ⟶ ℝ$
41	24 26	pm3.2i	$⊢ (ℝ \in V \land I \in V)$
42		elmapg	$⊢ (ℝ \in V \land I \in V) \to (\{⟨1, 0⟩, ⟨2, N⟩\} \in (ℝ^{I}) \leftrightarrow \{⟨1, 0⟩, ⟨2, N⟩\} : I ⟶ ℝ)$
43	41 42	mp1i	$⊢ N \in ℝ \to (\{⟨1, 0⟩, ⟨2, N⟩\} \in (ℝ^{I}) \leftrightarrow \{⟨1, 0⟩, ⟨2, N⟩\} : I ⟶ ℝ)$
44	40 43	mpbird	$⊢ N \in ℝ \to \{⟨1, 0⟩, ⟨2, N⟩\} \in (ℝ^{I})$
45	44 7 3	3eltr4g	$⊢ N \in ℝ \to Y \in P$
46	45	3ad2ant2	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to Y \in P$
47	6	fveq1i	$⊢ X (1) = \{⟨1, 0⟩, ⟨2, M⟩\} (1)$
48	9 12 14	3pm3.2i	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2)$
49		fvpr1g	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} (1) = 0$
50	48 49	mp1i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to \{⟨1, 0⟩, ⟨2, M⟩\} (1) = 0$
51	47 50	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (1) = 0$
52	7	fveq1i	$⊢ Y (1) = \{⟨1, 0⟩, ⟨2, N⟩\} (1)$
53		fvpr1g	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, N⟩\} (1) = 0$
54	48 53	mp1i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to \{⟨1, 0⟩, ⟨2, N⟩\} (1) = 0$
55	52 54	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to Y (1) = 0$
56	51 55	eqtr4d	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (1) = Y (1)$
57		simp3	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to M \neq N$
58	6	fveq1i	$⊢ X (2) = \{⟨1, 0⟩, ⟨2, M⟩\} (2)$
59		simp1	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to M \in ℝ$
60	14	a1i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to 1 \neq 2$
61		fvpr2g	$⊢ (2 \in V \land M \in ℝ \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} (2) = M$
62	10 59 60 61	mp3an2i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to \{⟨1, 0⟩, ⟨2, M⟩\} (2) = M$
63	58 62	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (2) = M$
64	7	fveq1i	$⊢ Y (2) = \{⟨1, 0⟩, ⟨2, N⟩\} (2)$
65		simp2	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to N \in ℝ$
66		fvpr2g	$⊢ (2 \in V \land N \in ℝ \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, N⟩\} (2) = N$
67	10 65 60 66	mp3an2i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to \{⟨1, 0⟩, ⟨2, N⟩\} (2) = N$
68	64 67	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to Y (2) = N$
69	57 63 68	3netr4d	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (2) \neq Y (2)$
70	56 69	jca	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to (X (1) = Y (1) \land X (2) \neq Y (2))$
71	30 46 70	3jca	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to (X \in P \land Y \in P \land (X (1) = Y (1) \land X (2) \neq Y (2)))$
72	71	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (X \in P \land Y \in P \land (X (1) = Y (1) \land X (2) \neq Y (2)))$
73	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)\}$
74	72 73	syl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to X L Y = \{p \in P \| p (1) = X (1)\}$
75	8 74	eqeq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (G = X L Y \leftrightarrow \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| p (1) = X (1)\})$
76	48 49	ax-mp	$⊢ \{⟨1, 0⟩, ⟨2, M⟩\} (1) = 0$
77	47 76	eqtri	$⊢ X (1) = 0$
78	77	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to X (1) = 0$
79	78	eqeq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (p (1) = X (1) \leftrightarrow p (1) = 0)$
80	79	rabbidv	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to \{p \in P \| p (1) = X (1)\} = \{p \in P \| p (1) = 0\}$
81	80	eqeq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (\{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| p (1) = X (1)\} \leftrightarrow \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| p (1) = 0\})$
82		rabbi	$⊢ \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| p (1) = 0\}$
83	1 3	line2ylem	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$
84	83	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$
85		oveq1	$⊢ B = 0 \to B p (2) = 0 \cdot p (2)$
86	85	3ad2ant2	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to B p (2) = 0 \cdot p (2)$
87	86	oveq2d	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to A p (1) + B p (2) = A p (1) + 0 \cdot p (2)$
88		simp3	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to C = 0$
89	87 88	eqeq12d	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to (A p (1) + B p (2) = C \leftrightarrow A p (1) + 0 \cdot p (2) = 0)$
90	89	ad2antlr	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (A p (1) + B p (2) = C \leftrightarrow A p (1) + 0 \cdot p (2) = 0)$
91	1 3	rrx2pyel	$⊢ p \in P \to p (2) \in ℝ$
92	91	recnd	$⊢ p \in P \to p (2) \in ℂ$
93	92	mul02d	$⊢ p \in P \to 0 \cdot p (2) = 0$
94	93	adantl	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to 0 \cdot p (2) = 0$
95	94	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to A p (1) + 0 \cdot p (2) = A p (1) + 0$
96		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
97	96	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
98	97	ad3antrrr	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to A \in ℂ$
99	1 3	rrx2pxel	$⊢ p \in P \to p (1) \in ℝ$
100	99	recnd	$⊢ p \in P \to p (1) \in ℂ$
101	100	adantl	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to p (1) \in ℂ$
102	98 101	mulcld	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to A p (1) \in ℂ$
103	102	addid1d	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to A p (1) + 0 = A p (1)$
104	95 103	eqtrd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to A p (1) + 0 \cdot p (2) = A p (1)$
105	104	eqeq1d	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (A p (1) + 0 \cdot p (2) = 0 \leftrightarrow A p (1) = 0)$
106	98 101	mul0ord	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (A p (1) = 0 \leftrightarrow (A = 0 \lor p (1) = 0))$
107		eqneqall	$⊢ A = 0 \to (A \neq 0 \to p (1) = 0)$
108	107	com12	$⊢ A \neq 0 \to (A = 0 \to p (1) = 0)$
109	108	3ad2ant1	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to (A = 0 \to p (1) = 0)$
110	109	ad2antlr	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (A = 0 \to p (1) = 0)$
111		idd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (p (1) = 0 \to p (1) = 0)$
112	110 111	jaod	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to ((A = 0 \lor p (1) = 0) \to p (1) = 0)$
113		olc	$⊢ p (1) = 0 \to (A = 0 \lor p (1) = 0)$
114	112 113	impbid1	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to ((A = 0 \lor p (1) = 0) \leftrightarrow p (1) = 0)$
115	106 114	bitrd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (A p (1) = 0 \leftrightarrow p (1) = 0)$
116	90 105 115	3bitrd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \land p \in P) \to (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
117	116	ralrimiva	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \land (A \neq 0 \land B = 0 \land C = 0)) \to \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0)$
118	117	ex	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to ((A \neq 0 \land B = 0 \land C = 0) \to \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0))$
119	84 118	impbid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (1) = 0) \leftrightarrow (A \neq 0 \land B = 0 \land C = 0))$
120	82 119	bitr3id	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (\{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| p (1) = 0\} \leftrightarrow (A \neq 0 \land B = 0 \land C = 0))$
121	75 81 120	3bitrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (G = X L Y \leftrightarrow (A \neq 0 \land B = 0 \land C = 0))$

Metamath Proof Explorer

Theorem line2y

Proof