Metamath Proof Explorer

Theorem transportcl

Description: Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion transportcl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → A B TransportTo C D ∈ 𝔼 ⁡ N

Proof

Step Hyp Ref Expression
1 fvtransport ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → A B TransportTo C D = ι r ∈ 𝔼 ⁡ N | D Btwn C r ∧ D r Cgr A B
2 segconeu ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → ∃! r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B
3 riotacl ⊢ ∃! r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B → ι r ∈ 𝔼 ⁡ N | D Btwn C r ∧ D r Cgr A B ∈ 𝔼 ⁡ N
4 2 3 syl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → ι r ∈ 𝔼 ⁡ N | D Btwn C r ∧ D r Cgr A B ∈ 𝔼 ⁡ N
5 1 4 eqeltrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → A B TransportTo C D ∈ 𝔼 ⁡ N