Metamath Proof Explorer


Definition df-lng

Description: Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019) Use its index-independent form lngid instead. (New usage is discouraged.)

Ref Expression
Assertion df-lng
|- LineG = Slot ; 1 7

Detailed syntax breakdown

Step Hyp Ref Expression
0 clng
 |-  LineG
1 c1
 |-  1
2 c7
 |-  7
3 1 2 cdc
 |-  ; 1 7
4 3 cslot
 |-  Slot ; 1 7
5 0 4 wceq
 |-  LineG = Slot ; 1 7