Metamath Proof Explorer

Theorem transportprops

Description: Calculate the defining properties of the transport function. (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		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⟩))$
2	1	eqcomd	$⊢ (N \in ℕ \land ((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⟩)) = ⟨A, B⟩ TransportTo ⟨C, D⟩$
3		transportcl	$⊢ (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⟩ \in 𝔼 (N)$
4		segconeu	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to \exists! r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)$
5		opeq2	$⊢ r = ⟨A, B⟩ TransportTo ⟨C, D⟩ \to ⟨C, r⟩ = ⟨C, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩$
6	5	breq2d	$⊢ r = ⟨A, B⟩ TransportTo ⟨C, D⟩ \to (D Btwn ⟨C, r⟩ \leftrightarrow D Btwn ⟨C, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩)$
7		opeq2	$⊢ r = ⟨A, B⟩ TransportTo ⟨C, D⟩ \to ⟨D, r⟩ = ⟨D, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩$
8	7	breq1d	$⊢ r = ⟨A, B⟩ TransportTo ⟨C, D⟩ \to (⟨D, r⟩ Cgr ⟨A, B⟩ \leftrightarrow ⟨D, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ Cgr ⟨A, B⟩)$
9	6 8	anbi12d	$⊢ r = ⟨A, B⟩ TransportTo ⟨C, D⟩ \to ((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \leftrightarrow (D Btwn ⟨C, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ \land ⟨D, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ Cgr ⟨A, B⟩))$
10	9	riota2	$⊢ (⟨A, B⟩ TransportTo ⟨C, D⟩ \in 𝔼 (N) \land \exists! r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) \to ((D Btwn ⟨C, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ \land ⟨D, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ Cgr ⟨A, B⟩) \leftrightarrow (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = ⟨A, B⟩ TransportTo ⟨C, D⟩)$
11	3 4 10	syl2anc	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to ((D Btwn ⟨C, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ \land ⟨D, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ Cgr ⟨A, B⟩) \leftrightarrow (ι r \in 𝔼 (N) \| (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)) = ⟨A, B⟩ TransportTo ⟨C, D⟩)$
12	2 11	mpbird	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to (D Btwn ⟨C, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ \land ⟨D, ⟨A, B⟩ TransportTo ⟨C, D⟩⟩ Cgr ⟨A, B⟩)$