Step |
Hyp |
Ref |
Expression |
0 |
|
cline |
⊢ LineM |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑤 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑤 ) |
7 |
|
vy |
⊢ 𝑦 |
8 |
3
|
cv |
⊢ 𝑥 |
9 |
8
|
csn |
⊢ { 𝑥 } |
10 |
6 9
|
cdif |
⊢ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) |
11 |
|
vp |
⊢ 𝑝 |
12 |
|
vt |
⊢ 𝑡 |
13 |
|
csca |
⊢ Scalar |
14 |
5 13
|
cfv |
⊢ ( Scalar ‘ 𝑤 ) |
15 |
14 4
|
cfv |
⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) ) |
16 |
11
|
cv |
⊢ 𝑝 |
17 |
|
cur |
⊢ 1r |
18 |
14 17
|
cfv |
⊢ ( 1r ‘ ( Scalar ‘ 𝑤 ) ) |
19 |
|
csg |
⊢ -g |
20 |
14 19
|
cfv |
⊢ ( -g ‘ ( Scalar ‘ 𝑤 ) ) |
21 |
12
|
cv |
⊢ 𝑡 |
22 |
18 21 20
|
co |
⊢ ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) |
23 |
|
cvsca |
⊢ ·𝑠 |
24 |
5 23
|
cfv |
⊢ ( ·𝑠 ‘ 𝑤 ) |
25 |
22 8 24
|
co |
⊢ ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) |
26 |
|
cplusg |
⊢ +g |
27 |
5 26
|
cfv |
⊢ ( +g ‘ 𝑤 ) |
28 |
7
|
cv |
⊢ 𝑦 |
29 |
21 28 24
|
co |
⊢ ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) |
30 |
25 29 27
|
co |
⊢ ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) |
31 |
16 30
|
wceq |
⊢ 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) |
32 |
31 12 15
|
wrex |
⊢ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) |
33 |
32 11 6
|
crab |
⊢ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } |
34 |
3 7 6 10 33
|
cmpo |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) |
35 |
1 2 34
|
cmpt |
⊢ ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) ) |
36 |
0 35
|
wceq |
⊢ LineM = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( ( Base ‘ 𝑤 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝑤 ) ) ( -g ‘ ( Scalar ‘ 𝑤 ) ) 𝑡 ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) ( 𝑡 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) } ) ) |