Metamath Proof Explorer

Definition df-lng

Description: Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019)

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