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

Proof

Step	Hyp	Ref	Expression
1		fvtransport	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
2	1	eqcomd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) )
3		transportcl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ( 𝔼 ‘ 𝑁 ) )
4		segconeu	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
5		opeq2	⊢ ( 𝑟 = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) → ⟨ 𝐶 , 𝑟 ⟩ = ⟨ 𝐶 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ )
6	5	breq2d	⊢ ( 𝑟 = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) → ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ↔ 𝐷 Btwn ⟨ 𝐶 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ ) )
7		opeq2	⊢ ( 𝑟 = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) → ⟨ 𝐷 , 𝑟 ⟩ = ⟨ 𝐷 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ )
8	7	breq1d	⊢ ( 𝑟 = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) → ( ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐷 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
9	6 8	anbi12d	⊢ ( 𝑟 = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) → ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐷 Btwn ⟨ 𝐶 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ ∧ ⟨ 𝐷 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
10	9	riota2	⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 𝐷 Btwn ⟨ 𝐶 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ ∧ ⟨ 𝐷 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ) )
11	3 4 10	syl2anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝐷 Btwn ⟨ 𝐶 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ ∧ ⟨ 𝐷 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ) )
12	2 11	mpbird	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝐷 Btwn ⟨ 𝐶 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ ∧ ⟨ 𝐷 , ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )