Metamath Proof Explorer

Table of Contents - 16.2. Tarskian Geometry

1. Congruence
   1. tgcgrcomimp
   2. tgcgrcomr
   3. tgcgrcoml
   4. tgcgrcomlr
   5. tgcgreqb
   6. tgcgreq
   7. tgcgrneq
   8. tgcgrtriv
   9. tgcgrextend
   10. tgsegconeq
2. Dimension
   1. tglowdim1
   2. tglowdim1i
   3. tgldimor
   4. tgldim0eq
   5. tgldim0itv
   6. tgldim0cgr
   7. tgbtwndiff
   8. tgdim01
3. Betweenness and Congruence
   1. tgifscgr
   2. tgcgrsub
4. Congruence of a series of points
   1. ccgrg
   2. df-cgrg
   3. iscgrg
   4. iscgrgd
   5. iscgrglt
   6. trgcgrg
   7. trgcgr
   8. ercgrg
   9. tgcgrxfr
   10. cgr3id
   11. cgr3simp1
   12. cgr3simp2
   13. cgr3simp3
   14. cgr3swap12
   15. cgr3swap23
   16. cgr3swap13
   17. cgr3rotr
   18. cgr3rotl
   19. trgcgrcom
   20. cgr3tr
   21. tgbtwnxfr
   22. tgcgr4
5. Motions
   1. cismt
   2. df-ismt
   3. isismt
   4. ismot
   5. motcgr
   6. idmot
   7. motf1o
   8. motcl
   9. motco
   10. cnvmot
   11. motplusg
   12. motgrp
   13. motcgrg
   14. motcgr3
6. Colinearity
   1. tglng
   2. tglnfn
   3. tglnunirn
   4. tglnpt
   5. tglngne
   6. tglngval
   7. tglnssp
   8. tgellng
   9. tgcolg
   10. btwncolg1
   11. btwncolg2
   12. btwncolg3
   13. colcom
   14. colrot1
   15. colrot2
   16. ncolcom
   17. ncolrot1
   18. ncolrot2
   19. tgdim01ln
   20. ncoltgdim2
   21. lnxfr
   22. lnext
   23. tgfscgr
   24. lncgr
   25. lnid
   26. tgidinside
7. Connectivity of betweenness
   1. tgbtwnconn1lem1
   2. tgbtwnconn1lem2
   3. tgbtwnconn1lem3
   4. tgbtwnconn1
   5. tgbtwnconn2
   6. tgbtwnconn3
   7. tgbtwnconnln3
   8. tgbtwnconn22
   9. tgbtwnconnln1
   10. tgbtwnconnln2
8. Less-than relation in geometric congruences
   1. cleg
   2. df-leg
   3. legval
   4. legov
   5. legov2
   6. legid
   7. btwnleg
   8. legtrd
   9. legtri3
   10. legtrid
   11. leg0
   12. legeq
   13. legbtwn
   14. tgcgrsub2
   15. ltgseg
   16. ltgov
   17. legov3
   18. legso
9. Rays
   1. chlg
   2. df-hlg
   3. ishlg
   4. hlcomb
   5. hlcomd
   6. hlne1
   7. hlne2
   8. hlln
   9. hleqnid
   10. hlid
   11. hltr
   12. hlbtwn
   13. btwnhl1
   14. btwnhl2
   15. btwnhl
   16. lnhl
   17. hlcgrex
   18. hlcgreulem
   19. hlcgreu
10. Lines
    1. btwnlng1
    2. btwnlng2
    3. btwnlng3
    4. lncom
    5. lnrot1
    6. lnrot2
    7. ncolne1
    8. ncolne2
    9. tgisline
    10. tglnne
    11. tglndim0
    12. tgelrnln
    13. tglineeltr
    14. tglineelsb2
    15. tglinerflx1
    16. tglinerflx2
    17. tglinecom
    18. tglinethru
    19. tghilberti1
    20. tghilberti2
    21. tglinethrueu
    22. tglinesseq
    23. tglnne0
    24. tglineintmo
    25. tglineineq
    26. tglineinsn
    27. tglineneq
    28. tglineinteq
    29. ncolncol
    30. coltr
    31. coltr3
    32. colline
    33. tglowdim2l
    34. tglowdim2ln
    35. tglnpt2
    36. tglnpt3
    37. tglnpt4
11. Point inversions
    1. cmir
    2. df-mir
    3. mirreu3
    4. mirval
    5. mirfv
    6. mircgr
    7. mirbtwn
    8. ismir
    9. mirf
    10. mircl
    11. mirmir
    12. mircom
    13. mirreu
    14. mireq
    15. mirinv
    16. mirne
    17. mircinv
    18. mirf1o
    19. miriso
    20. mirbtwni
    21. mirbtwnb
    22. mircgrs
    23. mirmir2
    24. mirmot
    25. mirln
    26. mirln2
    27. mirconn
    28. mirhl
    29. mirbtwnhl
    30. mirhl2
    31. mircgrextend
    32. mirtrcgr
    33. mirauto
    34. miduniq
    35. miduniq1
    36. miduniq2
    37. colmid
    38. symquadlem
    39. krippenlem
    40. krippen
    41. midexlem
12. Right angles
    1. crag
    2. df-rag
    3. cperpg
    4. df-perpg
    5. israg
    6. ragcom
    7. ragcol
    8. ragmir
    9. mirrag
    10. ragtrivb
    11. ragflat2
    12. ragflat
    13. ragtriva
    14. ragflat3
    15. ragcgr
    16. motrag
    17. ragncol
    18. perpln1
    19. perpln2
    20. isperp
    21. perpcom
    22. perpneq
    23. isperp2
    24. isperp2d
    25. ragperp
    26. footexALT
    27. footexlem1
    28. footexlem2
    29. footex
    30. foot
    31. footne
    32. footeq
    33. perpin
    34. hlperpnel
    35. perprag
    36. perpdragALT
    37. perpdrag
    38. colperp
    39. colperpexlem1
    40. colperpexlem2
    41. colperpexlem3
    42. colperpex
    43. mideulem2
    44. opphllem
    45. mideulem
    46. midex
    47. mideu
13. Half-planes
    1. islnopp
    2. islnoppd
    3. oppne1
    4. oppne2
    5. oppne3
    6. oppcom
    7. opptgdim2
    8. oppnid
    9. opphllem1
    10. opphllem2
    11. opphllem3
    12. opphllem4
    13. opphllem5
    14. opphllem6
    15. oppperpex
    16. opphl
    17. oppmir
    18. outpasch
    19. hlpasch
    20. chpg
    21. df-hpg
    22. ishpg
    23. hpgbr
    24. hpgne1
    25. hpgne2
    26. lnopp2hpgb
    27. lnoppnhpg
    28. hpgerlem
    29. hpgid
    30. hpgcom
    31. hpgtr
    32. colopp
    33. colhp
    34. hphl
14. Planes
    1. cplng
    2. df-plng
    3. tgplnfn
    4. tgelrnpln
    5. plngval
    6. isplng
    7. plngrnssp
    8. elplng
    9. plngssp
    10. elplngid
    11. elplnglnid
    12. lnincplng
    13. plngcplem
    14. plngcp
    15. plngrotlem1
    16. plngrotlem2
    17. plngrotlem3
    18. plngrot
    19. lnssplnglem
    20. lnssplng
    21. lnssplng1
    22. plngmiropp
    23. mirplncl
    24. hpgssplng
    25. plng3p
    26. nhpmirhp
15. Midpoints and Line Mirroring
    1. cmid
    2. clmi
    3. df-mid
    4. df-lmi
    5. midf
    6. midcl
    7. ismidb
    8. midbtwn
    9. midcgr
    10. midid
    11. midcom
    12. mirmid
    13. lmieu
    14. lmif
    15. lmicl
    16. islmib
    17. lmicom
    18. lmilmi
    19. lmireu
    20. lmieq
    21. lmiinv
    22. lmicinv
    23. lmimid
    24. lmif1o
    25. lmiisolem
    26. lmiiso
    27. lmimot
    28. hypcgrlem1
    29. hypcgrlem2
    30. hypcgr
    31. lmiopp
    32. lnperpex
    33. lnperpexs
    34. trgcopy
    35. trgcopyeulem
    36. trgcopyeu
16. Congruence of angles
    1. ccgra
    2. df-cgra
    3. iscgra
    4. iscgra1
    5. iscgrad
    6. cgrane1
    7. cgrane2
    8. cgrane3
    9. cgrane4
    10. cgrahl1
    11. cgrahl2
    12. cgracgr
    13. cgraid
    14. cgraswap
    15. cgrcgra
    16. cgracom
    17. cgratr
    18. flatcgra
    19. cgraswaplr
    20. cgrabtwn
    21. cgrahl
    22. cgracol
    23. cgrancol
    24. dfcgra2
    25. sacgr
    26. oacgr
    27. acopy
    28. acopyeu
    29. ragcgra
    30. ragraghl
    31. perpeqlem
    32. perpeq
17. Angle Comparisons
    1. cinag
    2. cleag
    3. df-inag
    4. isinag
    5. isinagd
    6. inagflat
    7. inagswap
    8. inagne1
    9. inagne2
    10. inagne3
    11. inaghl
    12. df-leag
    13. isleag
    14. isleagd
    15. leagne1
    16. leagne2
    17. leagne3
    18. leagne4
    19. cgrg3col4
18. Congruence Theorems
    1. tgsas1
    2. tgsas
    3. tgsas2
    4. tgsas3
    5. tgasa1
    6. tgasa
    7. tgsss1
    8. tgsss2
    9. tgsss3
    10. dfcgrg2
    11. isoas
19. Equilateral triangles
    1. ceqlg
    2. df-eqlg
    3. iseqlg
    4. iseqlgd
20. Parallel lines
    1. cprlng
    2. df-prlng
    3. brprlng
    4. prlngd
    5. prlngref
    6. prlngsym
    7. prlngrcl1
    8. prlngrcl2
    9. prlngin0
    10. prlngpln
    11. prlnghpg
    12. prlngpln3
    13. perpprlng
    14. prlngex
    15. prlngmolem1
    16. prlngmolem2
    17. prlngmo
    18. prlngeu