Step |
Hyp |
Ref |
Expression |
1 |
|
ttgval.n |
|- G = ( toTG ` H ) |
2 |
|
ttgitvval.i |
|- I = ( Itv ` G ) |
3 |
|
ttgitvval.b |
|- P = ( Base ` H ) |
4 |
|
ttgitvval.m |
|- .- = ( -g ` H ) |
5 |
|
ttgitvval.s |
|- .x. = ( .s ` H ) |
6 |
|
ttgelitv.x |
|- ( ph -> X e. P ) |
7 |
|
ttgelitv.y |
|- ( ph -> Y e. P ) |
8 |
|
ttgelitv.h |
|- ( ph -> H e. V ) |
9 |
|
ttgelitv.z |
|- ( ph -> Z e. P ) |
10 |
1 2 3 4 5
|
ttgitvval |
|- ( ( H e. V /\ X e. P /\ Y e. P ) -> ( X I Y ) = { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } ) |
11 |
8 6 7 10
|
syl3anc |
|- ( ph -> ( X I Y ) = { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } ) |
12 |
11
|
eleq2d |
|- ( ph -> ( Z e. ( X I Y ) <-> Z e. { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } ) ) |
13 |
|
oveq1 |
|- ( z = Z -> ( z .- X ) = ( Z .- X ) ) |
14 |
13
|
eqeq1d |
|- ( z = Z -> ( ( z .- X ) = ( k .x. ( Y .- X ) ) <-> ( Z .- X ) = ( k .x. ( Y .- X ) ) ) ) |
15 |
14
|
rexbidv |
|- ( z = Z -> ( E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) <-> E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) ) |
16 |
15
|
elrab |
|- ( Z e. { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } <-> ( Z e. P /\ E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) ) |
17 |
12 16
|
bitrdi |
|- ( ph -> ( Z e. ( X I Y ) <-> ( Z e. P /\ E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) ) ) |
18 |
9 17
|
mpbirand |
|- ( ph -> ( Z e. ( X I Y ) <-> E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) ) |