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 = (0 ..^2)$
	line2.e	$⊢ E = I$
	line2.p	$⊢ P = ℝ^{I}$
	line2.l	$⊢ L = {Line}_{M} (E)$
	line2.g	$⊢ G = \{p \in P \| A p (0) + B p (1) = C\}$
	line2y.x	$⊢ X = ⟨“ 0 M ”⟩$
	line2y.y	$⊢ Y = ⟨“ 0 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 = (0 ..^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 (0) + B p (1) = C\}$
6		line2y.x	$⊢ X = ⟨“ 0 M ”⟩$
7		line2y.y	$⊢ Y = ⟨“ 0 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 (0) + B p (1) = C\}$
9		s2len	$⊢ \|⟨“ 0 M ”⟩\| = 2$
10	9	eqcomi	$⊢ 2 = \|⟨“ 0 M ”⟩\|$
11	10	a1i	$⊢ M \in ℝ \to 2 = \|⟨“ 0 M ”⟩\|$
12		0red	$⊢ M \in ℝ \to 0 \in ℝ$
13		id	$⊢ M \in ℝ \to M \in ℝ$
14	12 13	s2cld	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ \in Word ℝ$
15	11 14	wrdfd	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ : (0 ..^2) ⟶ ℝ$
16	1	feq2i	$⊢ ⟨“ 0 M ”⟩ : I ⟶ ℝ \leftrightarrow ⟨“ 0 M ”⟩ : (0 ..^2) ⟶ ℝ$
17	15 16	sylibr	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ : I ⟶ ℝ$
18		reex	$⊢ ℝ \in V$
19	1	ovexi	$⊢ I \in V$
20	18 19	elmap	$⊢ ⟨“ 0 M ”⟩ \in (ℝ^{I}) \leftrightarrow ⟨“ 0 M ”⟩ : I ⟶ ℝ$
21	17 20	sylibr	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ \in (ℝ^{I})$
22	21 6 3	3eltr4g	$⊢ M \in ℝ \to X \in P$
23	22	3ad2ant1	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X \in P$
24		s2len	$⊢ \|⟨“ 0 N ”⟩\| = 2$
25	24	eqcomi	$⊢ 2 = \|⟨“ 0 N ”⟩\|$
26	25	a1i	$⊢ N \in ℝ \to 2 = \|⟨“ 0 N ”⟩\|$
27		0red	$⊢ N \in ℝ \to 0 \in ℝ$
28		id	$⊢ N \in ℝ \to N \in ℝ$
29	27 28	s2cld	$⊢ N \in ℝ \to ⟨“ 0 N ”⟩ \in Word ℝ$
30	26 29	wrdfd	$⊢ N \in ℝ \to ⟨“ 0 N ”⟩ : (0 ..^2) ⟶ ℝ$
31	1	feq2i	$⊢ ⟨“ 0 N ”⟩ : I ⟶ ℝ \leftrightarrow ⟨“ 0 N ”⟩ : (0 ..^2) ⟶ ℝ$
32	30 31	sylibr	$⊢ N \in ℝ \to ⟨“ 0 N ”⟩ : I ⟶ ℝ$
33	18 19	pm3.2i	$⊢ (ℝ \in V \land I \in V)$
34		elmapg	$⊢ (ℝ \in V \land I \in V) \to (⟨“ 0 N ”⟩ \in (ℝ^{I}) \leftrightarrow ⟨“ 0 N ”⟩ : I ⟶ ℝ)$
35	33 34	mp1i	$⊢ N \in ℝ \to (⟨“ 0 N ”⟩ \in (ℝ^{I}) \leftrightarrow ⟨“ 0 N ”⟩ : I ⟶ ℝ)$
36	32 35	mpbird	$⊢ N \in ℝ \to ⟨“ 0 N ”⟩ \in (ℝ^{I})$
37	36 7 3	3eltr4g	$⊢ N \in ℝ \to Y \in P$
38	37	3ad2ant2	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to Y \in P$
39	6	fveq1i	$⊢ X (0) = ⟨“ 0 M ”⟩ (0)$
40		0re	$⊢ 0 \in ℝ$
41		s2fv0	$⊢ 0 \in ℝ \to ⟨“ 0 M ”⟩ (0) = 0$
42	40 41	mp1i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to ⟨“ 0 M ”⟩ (0) = 0$
43	39 42	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (0) = 0$
44	7	fveq1i	$⊢ Y (0) = ⟨“ 0 N ”⟩ (0)$
45		s2fv0	$⊢ 0 \in ℝ \to ⟨“ 0 N ”⟩ (0) = 0$
46	40 45	mp1i	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to ⟨“ 0 N ”⟩ (0) = 0$
47	44 46	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to Y (0) = 0$
48	43 47	eqtr4d	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (0) = Y (0)$
49		simp3	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to M \neq N$
50	6	fveq1i	$⊢ X (1) = ⟨“ 0 M ”⟩ (1)$
51		s2fv1	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ (1) = M$
52	51	3ad2ant1	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to ⟨“ 0 M ”⟩ (1) = M$
53	50 52	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (1) = M$
54	7	fveq1i	$⊢ Y (1) = ⟨“ 0 N ”⟩ (1)$
55		s2fv1	$⊢ N \in ℝ \to ⟨“ 0 N ”⟩ (1) = N$
56	55	3ad2ant2	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to ⟨“ 0 N ”⟩ (1) = N$
57	54 56	eqtrid	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to Y (1) = N$
58	49 53 57	3netr4d	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to X (1) \neq Y (1)$
59	48 58	jca	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to (X (0) = Y (0) \land X (1) \neq Y (1))$
60	23 38 59	3jca	$⊢ (M \in ℝ \land N \in ℝ \land M \neq N) \to (X \in P \land Y \in P \land (X (0) = Y (0) \land X (1) \neq Y (1)))$
61	60	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 (0) = Y (0) \land X (1) \neq Y (1)))$
62	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)\}$
63	61 62	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 (0) = X (0)\}$
64	8 63	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 (0) + B p (1) = C\} = \{p \in P \| p (0) = X (0)\})$
65	40 41	ax-mp	$⊢ ⟨“ 0 M ”⟩ (0) = 0$
66	39 65	eqtri	$⊢ X (0) = 0$
67	66	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to X (0) = 0$
68	67	eqeq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to (p (0) = X (0) \leftrightarrow p (0) = 0)$
69	68	rabbidv	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (M \in ℝ \land N \in ℝ \land M \neq N)) \to \{p \in P \| p (0) = X (0)\} = \{p \in P \| p (0) = 0\}$
70	69	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 (0) + B p (1) = C\} = \{p \in P \| p (0) = X (0)\} \leftrightarrow \{p \in P \| A p (0) + B p (1) = C\} = \{p \in P \| p (0) = 0\})$
71		rabbi	$⊢ \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow \{p \in P \| A p (0) + B p (1) = C\} = \{p \in P \| p (0) = 0\}$
72	1 3	line2ylem	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (0) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$
73	72	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 (0) + B p (1) = C \leftrightarrow p (0) = 0) \to (A \neq 0 \land B = 0 \land C = 0))$
74		oveq1	$⊢ B = 0 \to B p (1) = 0 \cdot p (1)$
75	74	3ad2ant2	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to B p (1) = 0 \cdot p (1)$
76	75	oveq2d	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to A p (0) + B p (1) = A p (0) + 0 \cdot p (1)$
77		simp3	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to C = 0$
78	76 77	eqeq12d	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to (A p (0) + B p (1) = C \leftrightarrow A p (0) + 0 \cdot p (1) = 0)$
79	78	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 (0) + B p (1) = C \leftrightarrow A p (0) + 0 \cdot p (1) = 0)$
80	1 3	rrx2pyel	$⊢ p \in P \to p (1) \in ℝ$
81	80	recnd	$⊢ p \in P \to p (1) \in ℂ$
82	81	mul02d	$⊢ p \in P \to 0 \cdot p (1) = 0$
83	82	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 (1) = 0$
84	83	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 (0) + 0 \cdot p (1) = A p (0) + 0$
85		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
86	85	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℂ$
87	86	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 ℂ$
88	1 3	rrx2pxel	$⊢ p \in P \to p (0) \in ℝ$
89	88	recnd	$⊢ p \in P \to p (0) \in ℂ$
90	89	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 (0) \in ℂ$
91	87 90	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 (0) \in ℂ$
92	91	addridd	$⊢ ((((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 (0) + 0 = A p (0)$
93	84 92	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 (0) + 0 \cdot p (1) = A p (0)$
94	93	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 (0) + 0 \cdot p (1) = 0 \leftrightarrow A p (0) = 0)$
95	87 90	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 (0) = 0 \leftrightarrow (A = 0 \lor p (0) = 0))$
96		eqneqall	$⊢ A = 0 \to (A \neq 0 \to p (0) = 0)$
97	96	com12	$⊢ A \neq 0 \to (A = 0 \to p (0) = 0)$
98	97	3ad2ant1	$⊢ (A \neq 0 \land B = 0 \land C = 0) \to (A = 0 \to p (0) = 0)$
99	98	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 (0) = 0)$
100		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 (0) = 0 \to p (0) = 0)$
101	99 100	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 (0) = 0) \to p (0) = 0)$
102		olc	$⊢ p (0) = 0 \to (A = 0 \lor p (0) = 0)$
103	101 102	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 (0) = 0) \leftrightarrow p (0) = 0)$
104	95 103	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 (0) = 0 \leftrightarrow p (0) = 0)$
105	79 94 104	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 (0) + B p (1) = C \leftrightarrow p (0) = 0)$
106	105	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 (0) + B p (1) = C \leftrightarrow p (0) = 0)$
107	106	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 (0) + B p (1) = C \leftrightarrow p (0) = 0))$
108	73 107	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 (0) + B p (1) = C \leftrightarrow p (0) = 0) \leftrightarrow (A \neq 0 \land B = 0 \land C = 0))$
109	71 108	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 (0) + B p (1) = C\} = \{p \in P \| p (0) = 0\} \leftrightarrow (A \neq 0 \land B = 0 \land C = 0))$
110	64 70 109	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