Step |
Hyp |
Ref |
Expression |
1 |
|
lines.b |
|- B = ( Base ` W ) |
2 |
|
lines.l |
|- L = ( LineM ` W ) |
3 |
|
lines.s |
|- S = ( Scalar ` W ) |
4 |
|
lines.k |
|- K = ( Base ` S ) |
5 |
|
lines.p |
|- .x. = ( .s ` W ) |
6 |
|
lines.a |
|- .+ = ( +g ` W ) |
7 |
|
lines.m |
|- .- = ( -g ` S ) |
8 |
|
lines.1 |
|- .1. = ( 1r ` S ) |
9 |
|
df-line |
|- LineM = ( w e. _V |-> ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) ) |
10 |
|
fveq2 |
|- ( W = w -> ( Base ` W ) = ( Base ` w ) ) |
11 |
1 10
|
syl5eq |
|- ( W = w -> B = ( Base ` w ) ) |
12 |
11
|
difeq1d |
|- ( W = w -> ( B \ { x } ) = ( ( Base ` w ) \ { x } ) ) |
13 |
|
fveq2 |
|- ( W = w -> ( Scalar ` W ) = ( Scalar ` w ) ) |
14 |
3 13
|
syl5eq |
|- ( W = w -> S = ( Scalar ` w ) ) |
15 |
14
|
fveq2d |
|- ( W = w -> ( Base ` S ) = ( Base ` ( Scalar ` w ) ) ) |
16 |
4 15
|
syl5eq |
|- ( W = w -> K = ( Base ` ( Scalar ` w ) ) ) |
17 |
|
fveq2 |
|- ( W = w -> ( +g ` W ) = ( +g ` w ) ) |
18 |
6 17
|
syl5eq |
|- ( W = w -> .+ = ( +g ` w ) ) |
19 |
|
fveq2 |
|- ( W = w -> ( .s ` W ) = ( .s ` w ) ) |
20 |
5 19
|
syl5eq |
|- ( W = w -> .x. = ( .s ` w ) ) |
21 |
3
|
fveq2i |
|- ( -g ` S ) = ( -g ` ( Scalar ` W ) ) |
22 |
7 21
|
eqtri |
|- .- = ( -g ` ( Scalar ` W ) ) |
23 |
|
2fveq3 |
|- ( W = w -> ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` w ) ) ) |
24 |
22 23
|
syl5eq |
|- ( W = w -> .- = ( -g ` ( Scalar ` w ) ) ) |
25 |
3
|
fveq2i |
|- ( 1r ` S ) = ( 1r ` ( Scalar ` W ) ) |
26 |
8 25
|
eqtri |
|- .1. = ( 1r ` ( Scalar ` W ) ) |
27 |
|
2fveq3 |
|- ( W = w -> ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` w ) ) ) |
28 |
26 27
|
syl5eq |
|- ( W = w -> .1. = ( 1r ` ( Scalar ` w ) ) ) |
29 |
|
eqidd |
|- ( W = w -> t = t ) |
30 |
24 28 29
|
oveq123d |
|- ( W = w -> ( .1. .- t ) = ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ) |
31 |
|
eqidd |
|- ( W = w -> x = x ) |
32 |
20 30 31
|
oveq123d |
|- ( W = w -> ( ( .1. .- t ) .x. x ) = ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ) |
33 |
20
|
oveqd |
|- ( W = w -> ( t .x. y ) = ( t ( .s ` w ) y ) ) |
34 |
18 32 33
|
oveq123d |
|- ( W = w -> ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) ) |
35 |
34
|
eqeq2d |
|- ( W = w -> ( p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) <-> p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) ) ) |
36 |
16 35
|
rexeqbidv |
|- ( W = w -> ( E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) <-> E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) ) ) |
37 |
11 36
|
rabeqbidv |
|- ( W = w -> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } = { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) |
38 |
11 12 37
|
mpoeq123dv |
|- ( W = w -> ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) = ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) ) |
39 |
38
|
eqcomd |
|- ( W = w -> ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) ) |
40 |
39
|
eqcoms |
|- ( w = W -> ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) ) |
41 |
|
elex |
|- ( W e. V -> W e. _V ) |
42 |
1
|
fvexi |
|- B e. _V |
43 |
42
|
difexi |
|- ( B \ { x } ) e. _V |
44 |
42 43
|
mpoex |
|- ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) e. _V |
45 |
44
|
a1i |
|- ( W e. V -> ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) e. _V ) |
46 |
9 40 41 45
|
fvmptd3 |
|- ( W e. V -> ( LineM ` W ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) ) |
47 |
2 46
|
syl5eq |
|- ( W e. V -> L = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) ) |