Metamath Proof Explorer

Theorem fvline

Description: Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fvline ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→ALineB=x|xColinearAB

Proof

Step Hyp Ref Expression
1 eqid ⊢ABColinear-1=ABColinear-1
2 fveq2 ⊢n=N→𝔼⁡n=𝔼⁡N
3 2 eleq2d ⊢n=N→A∈𝔼⁡n↔A∈𝔼⁡N
4 2 eleq2d ⊢n=N→B∈𝔼⁡n↔B∈𝔼⁡N
5 3 4 3anbi12d ⊢n=N→A∈𝔼⁡n∧B∈𝔼⁡n∧A≠B↔A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B
6 5 anbi1d ⊢n=N→A∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1↔A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧ABColinear-1=ABColinear-1
7 6 rspcev ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧ABColinear-1=ABColinear-1→∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
8 1 7 mpanr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
9 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→A∈𝔼⁡N
10 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→B∈𝔼⁡N
11 colinearex ⊢Colinear∈V
12 11 cnvex ⊢Colinear-1∈V
13 ecexg ⊢Colinear-1∈V→ABColinear-1∈V
14 12 13 ax-mp ⊢ABColinear-1∈V
15 eleq1 ⊢a=A→a∈𝔼⁡n↔A∈𝔼⁡n
16 neeq1 ⊢a=A→a≠b↔A≠b
17 15 16 3anbi13d ⊢a=A→a∈𝔼⁡n∧b∈𝔼⁡n∧a≠b↔A∈𝔼⁡n∧b∈𝔼⁡n∧A≠b
18 opeq1 ⊢a=A→ab=Ab
19 18 eceq1d ⊢a=A→abColinear-1=AbColinear-1
20 19 eqeq2d ⊢a=A→l=abColinear-1↔l=AbColinear-1
21 17 20 anbi12d ⊢a=A→a∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1↔A∈𝔼⁡n∧b∈𝔼⁡n∧A≠b∧l=AbColinear-1
22 21 rexbidv ⊢a=A→∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1↔∃n∈ℕA∈𝔼⁡n∧b∈𝔼⁡n∧A≠b∧l=AbColinear-1
23 eleq1 ⊢b=B→b∈𝔼⁡n↔B∈𝔼⁡n
24 neeq2 ⊢b=B→A≠b↔A≠B
25 23 24 3anbi23d ⊢b=B→A∈𝔼⁡n∧b∈𝔼⁡n∧A≠b↔A∈𝔼⁡n∧B∈𝔼⁡n∧A≠B
26 opeq2 ⊢b=B→Ab=AB
27 26 eceq1d ⊢b=B→AbColinear-1=ABColinear-1
28 27 eqeq2d ⊢b=B→l=AbColinear-1↔l=ABColinear-1
29 25 28 anbi12d ⊢b=B→A∈𝔼⁡n∧b∈𝔼⁡n∧A≠b∧l=AbColinear-1↔A∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧l=ABColinear-1
30 29 rexbidv ⊢b=B→∃n∈ℕA∈𝔼⁡n∧b∈𝔼⁡n∧A≠b∧l=AbColinear-1↔∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧l=ABColinear-1
31 eqeq1 ⊢l=ABColinear-1→l=ABColinear-1↔ABColinear-1=ABColinear-1
32 31 anbi2d ⊢l=ABColinear-1→A∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧l=ABColinear-1↔A∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
33 32 rexbidv ⊢l=ABColinear-1→∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧l=ABColinear-1↔∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
34 22 30 33 eloprabg ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧ABColinear-1∈V→ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1↔∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
35 14 34 mp3an3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N→ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1↔∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
36 9 10 35 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1↔∃n∈ℕA∈𝔼⁡n∧B∈𝔼⁡n∧A≠B∧ABColinear-1=ABColinear-1
37 8 36 mpbird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1
38 df-ov ⊢ALineB=Line⁡AB
39 df-br ⊢ABLineABColinear-1↔ABABColinear-1∈Line
40 df-line2 ⊢Line=abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1
41 40 eleq2i ⊢ABABColinear-1∈Line↔ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1
42 39 41 bitri ⊢ABLineABColinear-1↔ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1
43 funline ⊢Fun⁡Line
44 funbrfv ⊢Fun⁡Line→ABLineABColinear-1→Line⁡AB=ABColinear-1
45 43 44 ax-mp ⊢ABLineABColinear-1→Line⁡AB=ABColinear-1
46 42 45 sylbir ⊢ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1→Line⁡AB=ABColinear-1
47 38 46 eqtrid ⊢ABABColinear-1∈abl|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧a≠b∧l=abColinear-1→ALineB=ABColinear-1
48 37 47 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→ALineB=ABColinear-1
49 opex ⊢AB∈V
50 dfec2 ⊢AB∈V→ABColinear-1=x|ABColinear-1x
51 49 50 ax-mp ⊢ABColinear-1=x|ABColinear-1x
52 vex ⊢x∈V
53 49 52 brcnv ⊢ABColinear-1x↔xColinearAB
54 53 abbii ⊢x|ABColinear-1x=x|xColinearAB
55 51 54 eqtri ⊢ABColinear-1=x|xColinearAB
56 48 55 eqtrdi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B→ALineB=x|xColinearAB