| Step | Hyp | Ref
| Expression |
| 1 | | lines.l |
. 2
⊢ 𝐿 = (LineM‘𝑊) |
| 2 | | df-line 48650 |
. . 3
⊢
LineM = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦))})) |
| 3 | | lines.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑊) |
| 4 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑊 = 𝑤 → (Base‘𝑊) = (Base‘𝑤)) |
| 5 | 3, 4 | eqtrid 2789 |
. . . . . 6
⊢ (𝑊 = 𝑤 → 𝐵 = (Base‘𝑤)) |
| 6 | 5 | difeq1d 4125 |
. . . . . 6
⊢ (𝑊 = 𝑤 → (𝐵 ∖ {𝑥}) = ((Base‘𝑤) ∖ {𝑥})) |
| 7 | | lines.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑆) |
| 8 | | lines.s |
. . . . . . . . . . 11
⊢ 𝑆 = (Scalar‘𝑊) |
| 9 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑊 = 𝑤 → (Scalar‘𝑊) = (Scalar‘𝑤)) |
| 10 | 8, 9 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑊 = 𝑤 → 𝑆 = (Scalar‘𝑤)) |
| 11 | 10 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑊 = 𝑤 → (Base‘𝑆) = (Base‘(Scalar‘𝑤))) |
| 12 | 7, 11 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝑊 = 𝑤 → 𝐾 = (Base‘(Scalar‘𝑤))) |
| 13 | | lines.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝑊) |
| 14 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑊 = 𝑤 → (+g‘𝑊) = (+g‘𝑤)) |
| 15 | 13, 14 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑊 = 𝑤 → + =
(+g‘𝑤)) |
| 16 | | lines.p |
. . . . . . . . . . . 12
⊢ · = (
·𝑠 ‘𝑊) |
| 17 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑊 = 𝑤 → ( ·𝑠
‘𝑊) = (
·𝑠 ‘𝑤)) |
| 18 | 16, 17 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝑊 = 𝑤 → · = (
·𝑠 ‘𝑤)) |
| 19 | | lines.m |
. . . . . . . . . . . . . 14
⊢ − =
(-g‘𝑆) |
| 20 | 8 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(-g‘𝑆) = (-g‘(Scalar‘𝑊)) |
| 21 | 19, 20 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ − =
(-g‘(Scalar‘𝑊)) |
| 22 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑊 = 𝑤 →
(-g‘(Scalar‘𝑊)) =
(-g‘(Scalar‘𝑤))) |
| 23 | 21, 22 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝑊 = 𝑤 → − =
(-g‘(Scalar‘𝑤))) |
| 24 | | lines.1 |
. . . . . . . . . . . . . 14
⊢ 1 =
(1r‘𝑆) |
| 25 | 8 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝑆) = (1r‘(Scalar‘𝑊)) |
| 26 | 24, 25 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 1 =
(1r‘(Scalar‘𝑊)) |
| 27 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑊 = 𝑤 →
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑤))) |
| 28 | 26, 27 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝑊 = 𝑤 → 1 =
(1r‘(Scalar‘𝑤))) |
| 29 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑊 = 𝑤 → 𝑡 = 𝑡) |
| 30 | 23, 28, 29 | oveq123d 7452 |
. . . . . . . . . . 11
⊢ (𝑊 = 𝑤 → ( 1 − 𝑡) = ((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)) |
| 31 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝑊 = 𝑤 → 𝑥 = 𝑥) |
| 32 | 18, 30, 31 | oveq123d 7452 |
. . . . . . . . . 10
⊢ (𝑊 = 𝑤 → (( 1 − 𝑡) · 𝑥) =
(((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)) |
| 33 | 18 | oveqd 7448 |
. . . . . . . . . 10
⊢ (𝑊 = 𝑤 → (𝑡 · 𝑦) = (𝑡( ·𝑠
‘𝑤)𝑦)) |
| 34 | 15, 32, 33 | oveq123d 7452 |
. . . . . . . . 9
⊢ (𝑊 = 𝑤 → ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦)) =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦))) |
| 35 | 34 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑊 = 𝑤 → (𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦)) ↔ 𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦)))) |
| 36 | 12, 35 | rexeqbidv 3347 |
. . . . . . 7
⊢ (𝑊 = 𝑤 → (∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦)) ↔ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦)))) |
| 37 | 5, 36 | rabeqbidv 3455 |
. . . . . 6
⊢ (𝑊 = 𝑤 → {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))} = {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦))}) |
| 38 | 5, 6, 37 | mpoeq123dv 7508 |
. . . . 5
⊢ (𝑊 = 𝑤 → (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))}) = (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦))})) |
| 39 | 38 | eqcomd 2743 |
. . . 4
⊢ (𝑊 = 𝑤 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))})) |
| 40 | 39 | eqcoms 2745 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 =
((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠
‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠
‘𝑤)𝑦))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))})) |
| 41 | | elex 3501 |
. . 3
⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ V) |
| 42 | 3 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 43 | 42 | difexi 5330 |
. . . . 5
⊢ (𝐵 ∖ {𝑥}) ∈ V |
| 44 | 42, 43 | mpoex 8104 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))}) ∈ V |
| 45 | 44 | a1i 11 |
. . 3
⊢ (𝑊 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))}) ∈ V) |
| 46 | 2, 40, 41, 45 | fvmptd3 7039 |
. 2
⊢ (𝑊 ∈ 𝑉 → (LineM‘𝑊) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))})) |
| 47 | 1, 46 | eqtrid 2789 |
1
⊢ (𝑊 ∈ 𝑉 → 𝐿 = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑝 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝐾 𝑝 = ((( 1 − 𝑡) · 𝑥) + (𝑡 · 𝑦))})) |