fvtransport

Description: Calculate the value of the TransportTo function. This function takes four points, A through D , where C and D are distinct. It then returns the point that extends C D by the length of A B . (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	fvtransport	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to ⟨A, B⟩ TransportTo ⟨C, D⟩ = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$⊢ ⟨A, B⟩ TransportTo ⟨C, D⟩ = TransportTo (⟨⟨A, B⟩, ⟨C, D⟩⟩)$
2		opelxpi	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N))$
3	2	3ad2ant1	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to ⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N))$
4		opelxpi	$⊢ (C \in 𝔼 (N) \land D \in 𝔼 (N)) \to ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N))$
5	4	3ad2ant2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N))$
6		simp3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to C \neq D$
7		op1stg	$⊢ (C \in 𝔼 (N) \land D \in 𝔼 (N)) \to 1^{st} (⟨C, D⟩) = C$
8	7	3ad2ant2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to 1^{st} (⟨C, D⟩) = C$
9		op2ndg	$⊢ (C \in 𝔼 (N) \land D \in 𝔼 (N)) \to 2^{nd} (⟨C, D⟩) = D$
10	9	3ad2ant2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to 2^{nd} (⟨C, D⟩) = D$
11	6 8 10	3netr4d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)$
12	3 5 11	3jca	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to (⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N)) \land ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩))$
13	8	opeq1d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to ⟨1^{st} (⟨C, D⟩), r⟩ = ⟨C, r⟩$
14	10 13	breq12d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \leftrightarrow D Btwn ⟨C, r⟩)$
15	10	opeq1d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to ⟨2^{nd} (⟨C, D⟩), r⟩ = ⟨D, r⟩$
16	15	breq1d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to (⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩ \leftrightarrow ⟨D, r⟩ Cgr ⟨A, B⟩)$
17	14 16	anbi12d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to ((2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩) \leftrightarrow (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$
18	17	riotabidv	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$
19	18	eqcomd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))$
20	12 19	jca	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \to ((⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N)) \land ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
21		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
22	21	sqxpeqd	$⊢ n = N \to 𝔼 (n) \times 𝔼 (n) = 𝔼 (N) \times 𝔼 (N)$
23	22	eleq2d	$⊢ n = N \to (⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \leftrightarrow ⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N)))$
24	22	eleq2d	$⊢ n = N \to (⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \leftrightarrow ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N)))$
25	23 24	3anbi12d	$⊢ n = N \to ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \leftrightarrow (⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N)) \land ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)))$
26	21	riotaeqdv	$⊢ n = N \to (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))$
27	26	eqeq2d	$⊢ n = N \to ((ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)) \leftrightarrow (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
28	25 27	anbi12d	$⊢ n = N \to (((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))) \leftrightarrow ((⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N)) \land ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))))$
29	28	rspcev	$⊢ (N \in ℕ \land ((⟨A, B⟩ \in (𝔼 (N) \times 𝔼 (N)) \land ⟨C, D⟩ \in (𝔼 (N) \times 𝔼 (N)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (N) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))) \to \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
30	20 29	sylan2	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
31		df-br	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ TransportTo (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \leftrightarrow ⟨⟨⟨A, B⟩, ⟨C, D⟩⟩, (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))⟩ \in TransportTo$
32		df-transport	$⊢ TransportTo = \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\}$
33	32	eleq2i	$⊢ ⟨⟨⟨A, B⟩, ⟨C, D⟩⟩, (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))⟩ \in TransportTo \leftrightarrow ⟨⟨⟨A, B⟩, ⟨C, D⟩⟩, (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))⟩ \in \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\}$
34		opex	$⊢ ⟨A, B⟩ \in V$
35		opex	$⊢ ⟨C, D⟩ \in V$
36		riotaex	$⊢ (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \in V$
37		eleq1	$⊢ p = ⟨A, B⟩ \to (p \in (𝔼 (n) \times 𝔼 (n)) \leftrightarrow ⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)))$
38	37	3anbi1d	$⊢ p = ⟨A, B⟩ \to ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \leftrightarrow (⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)))$
39		breq2	$⊢ p = ⟨A, B⟩ \to (⟨2^{nd} (q), r⟩ Cgr p \leftrightarrow ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩)$
40	39	anbi2d	$⊢ p = ⟨A, B⟩ \to ((2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p) \leftrightarrow (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩))$
41	40	riotabidv	$⊢ p = ⟨A, B⟩ \to (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩))$
42	41	eqeq2d	$⊢ p = ⟨A, B⟩ \to (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \leftrightarrow x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩)))$
43	38 42	anbi12d	$⊢ p = ⟨A, B⟩ \to (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩))))$
44	43	rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩))))$
45		eleq1	$⊢ q = ⟨C, D⟩ \to (q \in (𝔼 (n) \times 𝔼 (n)) \leftrightarrow ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)))$
46		fveq2	$⊢ q = ⟨C, D⟩ \to 1^{st} (q) = 1^{st} (⟨C, D⟩)$
47		fveq2	$⊢ q = ⟨C, D⟩ \to 2^{nd} (q) = 2^{nd} (⟨C, D⟩)$
48	46 47	neeq12d	$⊢ q = ⟨C, D⟩ \to (1^{st} (q) \neq 2^{nd} (q) \leftrightarrow 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩))$
49	45 48	3anbi23d	$⊢ q = ⟨C, D⟩ \to ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \leftrightarrow (⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)))$
50	46	opeq1d	$⊢ q = ⟨C, D⟩ \to ⟨1^{st} (q), r⟩ = ⟨1^{st} (⟨C, D⟩), r⟩$
51	47 50	breq12d	$⊢ q = ⟨C, D⟩ \to (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \leftrightarrow 2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩)$
52	47	opeq1d	$⊢ q = ⟨C, D⟩ \to ⟨2^{nd} (q), r⟩ = ⟨2^{nd} (⟨C, D⟩), r⟩$
53	52	breq1d	$⊢ q = ⟨C, D⟩ \to (⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩ \leftrightarrow ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)$
54	51 53	anbi12d	$⊢ q = ⟨C, D⟩ \to ((2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩) \leftrightarrow (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))$
55	54	riotabidv	$⊢ q = ⟨C, D⟩ \to (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))$
56	55	eqeq2d	$⊢ q = ⟨C, D⟩ \to (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩)) \leftrightarrow x = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
57	49 56	anbi12d	$⊢ q = ⟨C, D⟩ \to (((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩))) \leftrightarrow ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))))$
58	57	rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr ⟨A, B⟩))) \leftrightarrow \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))))$
59		eqeq1	$⊢ x = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \to (x = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)) \leftrightarrow (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
60	59	anbi2d	$⊢ x = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \to (((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))) \leftrightarrow ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))))$
61	60	rexbidv	$⊢ x = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \to (\exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))) \leftrightarrow \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))))$
62	44 58 61	eloprabg	$⊢ (⟨A, B⟩ \in V \land ⟨C, D⟩ \in V \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \in V) \to (⟨⟨⟨A, B⟩, ⟨C, D⟩⟩, (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))⟩ \in \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\} \leftrightarrow \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))))$
63	34 35 36 62	mp3an	$⊢ ⟨⟨⟨A, B⟩, ⟨C, D⟩⟩, (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))⟩ \in \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\} \leftrightarrow \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
64	31 33 63	3bitri	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ TransportTo (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \leftrightarrow \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩)))$
65		funtransport	$⊢ Fun TransportTo$
66		funbrfv	$⊢ Fun TransportTo \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ TransportTo (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \to TransportTo (⟨⟨A, B⟩, ⟨C, D⟩⟩) = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)))$
67	65 66	ax-mp	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ TransportTo (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \to TransportTo (⟨⟨A, B⟩, ⟨C, D⟩⟩) = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$
68	64 67	sylbir	$⊢ \exists n \in ℕ ((⟨A, B⟩ \in (𝔼 (n) \times 𝔼 (n)) \land ⟨C, D⟩ \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (⟨C, D⟩) \neq 2^{nd} (⟨C, D⟩)) \land (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = (ι r \in 𝔼 (n) \| (2^{nd} (⟨C, D⟩) Btwn ⟨1^{st} (⟨C, D⟩), r⟩ \land ⟨2^{nd} (⟨C, D⟩), r⟩ Cgr ⟨A, B⟩))) \to TransportTo (⟨⟨A, B⟩, ⟨C, D⟩⟩) = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$
69	30 68	syl	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to TransportTo (⟨⟨A, B⟩, ⟨C, D⟩⟩) = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$
70	1 69	syl5eq	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to ⟨A, B⟩ TransportTo ⟨C, D⟩ = (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩))$

Metamath Proof Explorer

Theorem fvtransport

Proof