Metamath Proof Explorer


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 ) ( 𝑍 𝑋 ) = ( 𝑘 · ( 𝑌 𝑋 ) ) ) )