Metamath Proof Explorer

Table of Contents - 15.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. tglnne0
    23. tglnpt2
    24. tglineintmo
    25. tglineineq
    26. tglineneq
    27. tglineinteq
    28. ncolncol
    29. coltr
    30. coltr3
    31. colline
    32. tglowdim2l
    33. tglowdim2ln
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. hlperpnel
    34. perprag
    35. perpdragALT
    36. perpdrag
    37. colperp
    38. colperpexlem1
    39. colperpexlem2
    40. colperpexlem3
    41. colperpex
    42. mideulem2
    43. opphllem
    44. mideulem
    45. midex
    46. 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. outpasch
    18. hlpasch
    19. chpg
    20. df-hpg
    21. ishpg
    22. hpgbr
    23. hpgne1
    24. hpgne2
    25. lnopp2hpgb
    26. lnoppnhpg
    27. hpgerlem
    28. hpgid
    29. hpgcom
    30. hpgtr
    31. colopp
    32. colhp
    33. hphl
14. 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. trgcopy
    34. trgcopyeulem
    35. trgcopyeu
15. 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
16. 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
17. Congruence Theorems
    1. tgsas1
    2. tgsas
    3. tgsas2
    4. tgsas3
    5. tgasa1
    6. tgasa
    7. tgsss1
    8. tgsss2
    9. tgsss3
    10. dfcgrg2
    11. isoas
18. Equilateral triangles
    1. ceqlg
    2. df-eqlg
    3. iseqlg
    4. iseqlgd