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