Metamath Proof Explorer

Theorem lines

Description: The lines passing through two different points in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023)

Ref Expression
Hypotheses lines.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
lines.l ⊢ 𝐿 = ( LineM ‘ 𝑊 )
lines.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
lines.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
lines.p ⊢ · = ( ·𝑠 ‘ 𝑊 )
lines.a ⊢ + = ( +g ‘ 𝑊 )
lines.m ⊢ − = ( -g ‘ 𝑆 )
lines.1 ⊢ 1 = ( 1r ‘ 𝑆 )
Assertion lines ( 𝑊 ∈ 𝑉 → 𝐿 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝐾 𝑝 = ( ( ( 1 − 𝑡 ) · 𝑥 ) + ( 𝑡 · 𝑦 ) ) } ) )

Proof

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