Theorem ttgitvval

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	⊢ · = ( ·𝑠 ‘ 𝐻 )
Assertion	ttgitvval	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 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	1 3 4 5 2	ttgval	⊢ ( 𝐻 ∈ 𝑉 → ( 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝑃 , 𝑦 ∈ 𝑃 ↦ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝑃 , 𝑦 ∈ 𝑃 ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) ∧ 𝐼 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ 𝑃 ↦ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) )
7	6	simprd	⊢ ( 𝐻 ∈ 𝑉 → 𝐼 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ 𝑃 ↦ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
8	7	3ad2ant1	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐼 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ 𝑃 ↦ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
9		simprl	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
10	9	oveq2d	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑧 − 𝑥 ) = ( 𝑧 − 𝑋 ) )
11		simprr	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
12	11 9	oveq12d	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑦 − 𝑥 ) = ( 𝑌 − 𝑋 ) )
13	12	oveq2d	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑘 · ( 𝑦 − 𝑥 ) ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) )
14	10 13	eqeq12d	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ↔ ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )
15	14	rexbidv	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )
16	15	rabbidv	⊢ ( ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } = { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } )
17		simp2	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑋 ∈ 𝑃 )
18		simp3	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑌 ∈ 𝑃 )
19	3	fvexi	⊢ 𝑃 ∈ V
20	19	rabex	⊢ { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } ∈ V
21	20	a1i	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } ∈ V )
22	8 16 17 18 21	ovmpod	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) } )