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