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	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fvtransport	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
2		segconeu	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
3		riotacl	⊢ ( ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
4	2 3	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
5	1 4	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ( 𝔼 ‘ 𝑁 ) )