fvline

Description: Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	fvline	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \| x Colinear ⟨A, B⟩\}$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}$
2		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
3	2	eleq2d	$⊢ n = N \to (A \in 𝔼 (n) \leftrightarrow A \in 𝔼 (N))$
4	2	eleq2d	$⊢ n = N \to (B \in 𝔼 (n) \leftrightarrow B \in 𝔼 (N))$
5	3 4	3anbi12d	$⊢ n = N \to ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \leftrightarrow (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B))$
6	5	anbi1d	$⊢ n = N \to (((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}) \leftrightarrow ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}))$
7	6	rspcev	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1})) \to \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1})$
8	1 7	mpanr2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1})$
9		simpr1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A \in 𝔼 (N)$
10		simpr2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to B \in 𝔼 (N)$
11		colinearex	$⊢ Colinear \in V$
12	11	cnvex	$⊢ {Colinear}^{-1} \in V$
13		ecexg	$⊢ {Colinear}^{-1} \in V \to [⟨A, B⟩] {Colinear}^{-1} \in V$
14	12 13	ax-mp	$⊢ [⟨A, B⟩] {Colinear}^{-1} \in V$
15		eleq1	$⊢ a = A \to (a \in 𝔼 (n) \leftrightarrow A \in 𝔼 (n))$
16		neeq1	$⊢ a = A \to (a \neq b \leftrightarrow A \neq b)$
17	15 16	3anbi13d	$⊢ a = A \to ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \leftrightarrow (A \in 𝔼 (n) \land b \in 𝔼 (n) \land A \neq b))$
18		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
19	18	eceq1d	$⊢ a = A \to [⟨a, b⟩] {Colinear}^{-1} = [⟨A, b⟩] {Colinear}^{-1}$
20	19	eqeq2d	$⊢ a = A \to (l = [⟨a, b⟩] {Colinear}^{-1} \leftrightarrow l = [⟨A, b⟩] {Colinear}^{-1})$
21	17 20	anbi12d	$⊢ a = A \to (((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow ((A \in 𝔼 (n) \land b \in 𝔼 (n) \land A \neq b) \land l = [⟨A, b⟩] {Colinear}^{-1}))$
22	21	rexbidv	$⊢ a = A \to (\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land b \in 𝔼 (n) \land A \neq b) \land l = [⟨A, b⟩] {Colinear}^{-1}))$
23		eleq1	$⊢ b = B \to (b \in 𝔼 (n) \leftrightarrow B \in 𝔼 (n))$
24		neeq2	$⊢ b = B \to (A \neq b \leftrightarrow A \neq B)$
25	23 24	3anbi23d	$⊢ b = B \to ((A \in 𝔼 (n) \land b \in 𝔼 (n) \land A \neq b) \leftrightarrow (A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B))$
26		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
27	26	eceq1d	$⊢ b = B \to [⟨A, b⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}$
28	27	eqeq2d	$⊢ b = B \to (l = [⟨A, b⟩] {Colinear}^{-1} \leftrightarrow l = [⟨A, B⟩] {Colinear}^{-1})$
29	25 28	anbi12d	$⊢ b = B \to (((A \in 𝔼 (n) \land b \in 𝔼 (n) \land A \neq b) \land l = [⟨A, b⟩] {Colinear}^{-1}) \leftrightarrow ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land l = [⟨A, B⟩] {Colinear}^{-1}))$
30	29	rexbidv	$⊢ b = B \to (\exists n \in ℕ ((A \in 𝔼 (n) \land b \in 𝔼 (n) \land A \neq b) \land l = [⟨A, b⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land l = [⟨A, B⟩] {Colinear}^{-1}))$
31		eqeq1	$⊢ l = [⟨A, B⟩] {Colinear}^{-1} \to (l = [⟨A, B⟩] {Colinear}^{-1} \leftrightarrow [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1})$
32	31	anbi2d	$⊢ l = [⟨A, B⟩] {Colinear}^{-1} \to (((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land l = [⟨A, B⟩] {Colinear}^{-1}) \leftrightarrow ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}))$
33	32	rexbidv	$⊢ l = [⟨A, B⟩] {Colinear}^{-1} \to (\exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land l = [⟨A, B⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}))$
34	22 30 33	eloprabg	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land [⟨A, B⟩] {Colinear}^{-1} \in V) \to (⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\} \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}))$
35	14 34	mp3an3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\} \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}))$
36	9 10 35	syl2anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to (⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\} \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land B \in 𝔼 (n) \land A \neq B) \land [⟨A, B⟩] {Colinear}^{-1} = [⟨A, B⟩] {Colinear}^{-1}))$
37	8 36	mpbird	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
38		df-ov	$⊢ A Line B = Line (⟨A, B⟩)$
39		df-br	$⊢ ⟨A, B⟩ Line [⟨A, B⟩] {Colinear}^{-1} \leftrightarrow ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in Line$
40		df-line2	$⊢ Line = \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
41	40	eleq2i	$⊢ ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in Line \leftrightarrow ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
42	39 41	bitri	$⊢ ⟨A, B⟩ Line [⟨A, B⟩] {Colinear}^{-1} \leftrightarrow ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
43		funline	$⊢ Fun Line$
44		funbrfv	$⊢ Fun Line \to (⟨A, B⟩ Line [⟨A, B⟩] {Colinear}^{-1} \to Line (⟨A, B⟩) = [⟨A, B⟩] {Colinear}^{-1})$
45	43 44	ax-mp	$⊢ ⟨A, B⟩ Line [⟨A, B⟩] {Colinear}^{-1} \to Line (⟨A, B⟩) = [⟨A, B⟩] {Colinear}^{-1}$
46	42 45	sylbir	$⊢ ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\} \to Line (⟨A, B⟩) = [⟨A, B⟩] {Colinear}^{-1}$
47	38 46	syl5eq	$⊢ ⟨⟨A, B⟩, [⟨A, B⟩] {Colinear}^{-1}⟩ \in \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\} \to A Line B = [⟨A, B⟩] {Colinear}^{-1}$
48	37 47	syl	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = [⟨A, B⟩] {Colinear}^{-1}$
49		opex	$⊢ ⟨A, B⟩ \in V$
50		dfec2	$⊢ ⟨A, B⟩ \in V \to [⟨A, B⟩] {Colinear}^{-1} = \{x \| ⟨A, B⟩ {Colinear}^{-1} x\}$
51	49 50	ax-mp	$⊢ [⟨A, B⟩] {Colinear}^{-1} = \{x \| ⟨A, B⟩ {Colinear}^{-1} x\}$
52		vex	$⊢ x \in V$
53	49 52	brcnv	$⊢ ⟨A, B⟩ {Colinear}^{-1} x \leftrightarrow x Colinear ⟨A, B⟩$
54	53	abbii	$⊢ \{x \| ⟨A, B⟩ {Colinear}^{-1} x\} = \{x \| x Colinear ⟨A, B⟩\}$
55	51 54	eqtri	$⊢ [⟨A, B⟩] {Colinear}^{-1} = \{x \| x Colinear ⟨A, B⟩\}$
56	48 55	eqtrdi	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \| x Colinear ⟨A, B⟩\}$

Metamath Proof Explorer

Theorem fvline

Proof