Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isibg2 Unicode version

Theorem isibg2 26213
 Description: The predicate "is an incidence-betweenness geometry". B-1 If is between and then it is between and and , , are collinear and distinct. B-2 If and are distinct, then there are points , , such that is before and , is between and , is after and . B-3 If three points , , are collinear and distinct then exactly one of the followings occurs: is between and , is between and , is between and . B-4 "Being on the same side" is a transitive relation. If and are not on the same side of and and are not on the same side of then and are on the same side of . (For my private use only. Don't use.) (Contributed by FL, 1-Apr-2016.)
Hypotheses
Ref Expression
isibg.1 PPoints
isibg.2 PLines
isibg.3 btw
isibg.6 coln
Assertion
Ref Expression
isibg2 Ibg Ig
Distinct variable groups:   ,,,,,,,   ,,,,,,   ,,,   ,,,,
Allowed substitution hints:   (,,,)   ()   (,,,,,,)   (,,)

Proof of Theorem isibg2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5541 . . . . . 6 PPoints PPoints
2 fveq2 5541 . . . . . . 7 PLines PLines
3 dfsbcq 3006 . . . . . . 7 PLines PLines PLines coln btw PLines coln btw
42, 3syl 15 . . . . . 6 PLines coln btw PLines coln btw
51, 4sbcbidv2 25072 . . . . 5 PPoints PLines coln btw PPoints PLines coln btw
6 fveq2 5541 . . . . . . . 8 coln coln
7 fveq2 5541 . . . . . . . . 9 btw btw
8 dfsbcq 3006 . . . . . . . . 9 btw btw btw btw
97, 8syl 15 . . . . . . . 8 btw btw
106, 9sbcbidv2 25072 . . . . . . 7 coln btw coln btw
1110sbcbidv 3058 . . . . . 6 PLines coln btw PLines coln btw
1211sbcbidv 3058 . . . . 5 PPoints PLines coln btw PPoints PLines coln btw
135, 12bitrd 244 . . . 4 PPoints PLines coln btw PPoints PLines coln btw
14 isibg.1 . . . . . . 7 PPoints
1514eqcomi 2300 . . . . . 6 PPoints
16 dfsbcq 3006 . . . . . 6 PPoints PPoints PLines coln btw PLines coln btw
1715, 16ax-mp 8 . . . . 5 PPoints PLines coln btw PLines coln btw
18 fvex 5555 . . . . . . . 8 PPoints
1914, 18eqeltri 2366 . . . . . . 7
20 isibg.2 . . . . . . . . . 10 PLines
2120eqcomi 2300 . . . . . . . . 9 PLines
22 dfsbcq 3006 . . . . . . . . 9 PLines PLines coln btw coln btw
2321, 22ax-mp 8 . . . . . . . 8 PLines coln btw coln btw
2423sbcbiiOLD 3060 . . . . . . 7 PLines coln btw coln btw
2519, 24ax-mp 8 . . . . . 6 PLines coln btw coln btw
26 fvex 5555 . . . . . . . . . 10 PLines
2720, 26eqeltri 2366 . . . . . . . . 9
28 isibg.6 . . . . . . . . . . . . 13 coln
2928eqcomi 2300 . . . . . . . . . . . 12 coln
30 dfsbcq 3006 . . . . . . . . . . . 12 coln coln btw btw
3129, 30ax-mp 8 . . . . . . . . . . 11 coln btw btw
32 fvex 5555 . . . . . . . . . . . . 13 coln
3328, 32eqeltri 2366 . . . . . . . . . . . 12
34 isibg.3 . . . . . . . . . . . . . . 15 btw
3534eqcomi 2300 . . . . . . . . . . . . . 14 btw
36 dfsbcq 3006 . . . . . . . . . . . . . 14 btw btw
3735, 36ax-mp 8 . . . . . . . . . . . . 13 btw
3837sbcbiiOLD 3060 . . . . . . . . . . . 12 btw
3933, 38ax-mp 8 . . . . . . . . . . 11 btw
4031, 39bitri 240 . . . . . . . . . 10 coln btw
4140sbcbiiOLD 3060 . . . . . . . . 9 coln btw
4227, 41ax-mp 8 . . . . . . . 8 coln btw
4342sbcbiiOLD 3060 . . . . . . 7 coln btw
4419, 43ax-mp 8 . . . . . 6 coln btw