Step |
Hyp |
Ref |
Expression |
1 |
|
rrxlines.e |
⊢ 𝐸 = ( ℝ^ ‘ 𝐼 ) |
2 |
|
rrxlines.p |
⊢ 𝑃 = ( ℝ ↑m 𝐼 ) |
3 |
|
rrxlines.l |
⊢ 𝐿 = ( LineM ‘ 𝐸 ) |
4 |
|
rrxlines.m |
⊢ · = ( ·𝑠 ‘ 𝐸 ) |
5 |
|
rrxlines.a |
⊢ + = ( +g ‘ 𝐸 ) |
6 |
1
|
fvexi |
⊢ 𝐸 ∈ V |
7 |
|
eqid |
⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 ) |
8 |
|
eqid |
⊢ ( Scalar ‘ 𝐸 ) = ( Scalar ‘ 𝐸 ) |
9 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝐸 ) ) = ( Base ‘ ( Scalar ‘ 𝐸 ) ) |
10 |
|
eqid |
⊢ ( -g ‘ ( Scalar ‘ 𝐸 ) ) = ( -g ‘ ( Scalar ‘ 𝐸 ) ) |
11 |
|
eqid |
⊢ ( 1r ‘ ( Scalar ‘ 𝐸 ) ) = ( 1r ‘ ( Scalar ‘ 𝐸 ) ) |
12 |
7 3 8 9 4 5 10 11
|
lines |
⊢ ( 𝐸 ∈ V → 𝐿 = ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑦 ∈ ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) ) |
13 |
6 12
|
mp1i |
⊢ ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑦 ∈ ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) ) |
14 |
|
id |
⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin ) |
15 |
14 1 7
|
rrxbasefi |
⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = ( ℝ ↑m 𝐼 ) ) |
16 |
15 2
|
eqtr4di |
⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝐸 ) = 𝑃 ) |
17 |
16
|
difeq1d |
⊢ ( 𝐼 ∈ Fin → ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑥 } ) ) |
18 |
1
|
rrxsca |
⊢ ( 𝐼 ∈ Fin → ( Scalar ‘ 𝐸 ) = ℝfld ) |
19 |
18
|
fveq2d |
⊢ ( 𝐼 ∈ Fin → ( Base ‘ ( Scalar ‘ 𝐸 ) ) = ( Base ‘ ℝfld ) ) |
20 |
|
rebase |
⊢ ℝ = ( Base ‘ ℝfld ) |
21 |
19 20
|
eqtr4di |
⊢ ( 𝐼 ∈ Fin → ( Base ‘ ( Scalar ‘ 𝐸 ) ) = ℝ ) |
22 |
18
|
fveq2d |
⊢ ( 𝐼 ∈ Fin → ( 1r ‘ ( Scalar ‘ 𝐸 ) ) = ( 1r ‘ ℝfld ) ) |
23 |
|
re1r |
⊢ 1 = ( 1r ‘ ℝfld ) |
24 |
22 23
|
eqtr4di |
⊢ ( 𝐼 ∈ Fin → ( 1r ‘ ( Scalar ‘ 𝐸 ) ) = 1 ) |
25 |
24
|
oveq1d |
⊢ ( 𝐼 ∈ Fin → ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) ) |
26 |
25
|
adantr |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) ) |
27 |
18
|
fveq2d |
⊢ ( 𝐼 ∈ Fin → ( -g ‘ ( Scalar ‘ 𝐸 ) ) = ( -g ‘ ℝfld ) ) |
28 |
27
|
oveqd |
⊢ ( 𝐼 ∈ Fin → ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ℝfld ) 𝑡 ) ) |
29 |
28
|
adantr |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( 1 ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 ( -g ‘ ℝfld ) 𝑡 ) ) |
30 |
21
|
eleq2d |
⊢ ( 𝐼 ∈ Fin → ( 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ↔ 𝑡 ∈ ℝ ) ) |
31 |
|
1re |
⊢ 1 ∈ ℝ |
32 |
|
eqid |
⊢ ( -g ‘ ℝfld ) = ( -g ‘ ℝfld ) |
33 |
32
|
resubgval |
⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) = ( 1 ( -g ‘ ℝfld ) 𝑡 ) ) |
34 |
33
|
eqcomd |
⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) ) |
35 |
31 34
|
mpan |
⊢ ( 𝑡 ∈ ℝ → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) ) |
36 |
30 35
|
syl6bi |
⊢ ( 𝐼 ∈ Fin → ( 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) ) ) |
37 |
36
|
imp |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( 1 ( -g ‘ ℝfld ) 𝑡 ) = ( 1 − 𝑡 ) ) |
38 |
26 29 37
|
3eqtrd |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) = ( 1 − 𝑡 ) ) |
39 |
38
|
oveq1d |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) = ( ( 1 − 𝑡 ) · 𝑥 ) ) |
40 |
39
|
oveq1d |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ) |
41 |
40
|
eqeq2d |
⊢ ( ( 𝐼 ∈ Fin ∧ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) ) → ( 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ) ) |
42 |
21 41
|
rexeqbidva |
⊢ ( 𝐼 ∈ Fin → ( ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ↔ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) ) ) |
43 |
16 42
|
rabeqbidv |
⊢ ( 𝐼 ∈ Fin → { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } = { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) |
44 |
16 17 43
|
mpoeq123dv |
⊢ ( 𝐼 ∈ Fin → ( 𝑥 ∈ ( Base ‘ 𝐸 ) , 𝑦 ∈ ( ( Base ‘ 𝐸 ) ∖ { 𝑥 } ) ↦ { 𝑝 ∈ ( Base ‘ 𝐸 ) ∣ ∃ 𝑡 ∈ ( Base ‘ ( Scalar ‘ 𝐸 ) ) 𝑝 = ( ( ( ( 1r ‘ ( Scalar ‘ 𝐸 ) ) ( -g ‘ ( Scalar ‘ 𝐸 ) ) 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) ) |
45 |
13 44
|
eqtrd |
⊢ ( 𝐼 ∈ Fin → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ∃ 𝑡 ∈ ℝ 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) ) |