Theorem ttgelitv

Description: Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

	Ref	Expression
Hypotheses	ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgitvval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	ttgitvval.b	⊢ 𝑃 = ( Base ‘ 𝐻 )
	ttgitvval.m	⊢ − = ( -g ‘ 𝐻 )
	ttgitvval.s	⊢ · = ( ·𝑠 ‘ 𝐻 )
	ttgelitv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	ttgelitv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	ttgelitv.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
	ttgelitv.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
Assertion	ttgelitv	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑍 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgitvval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		ttgitvval.b	⊢ 𝑃 = ( Base ‘ 𝐻 )
4		ttgitvval.m	⊢ − = ( -g ‘ 𝐻 )
5		ttgitvval.s	⊢ · = ( ·𝑠 ‘ 𝐻 )
6		ttgelitv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7		ttgelitv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8		ttgelitv.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
9		ttgelitv.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
10	1 2 3 4 5	ttgitvval	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } )
11	8 6 7 10	syl3anc	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } )
12	11	eleq2d	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } ) )
13		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 − 𝑋 ) = ( 𝑍 − 𝑋 ) )
14	13	eqeq1d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ↔ ( 𝑍 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )
15	14	rexbidv	⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑍 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )
16	15	elrab	⊢ ( 𝑍 ∈ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } ↔ ( 𝑍 ∈ 𝑃 ∧ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑍 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )
17	12 16	bitrdi	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝑍 ∈ 𝑃 ∧ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑍 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) ) )
18	9 17	mpbirand	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑍 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )