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

Definition df-ibcg 25356
 Description: Incidence-Betweenness Geometry plus congruence axioms. (Here is an excerpt of Aitken's handout.) Axiom (C-1). Segment congruence is an equivalence relation for line segments. Axiom (C-2). Suppose that is a line segment and is a ray. Then there is a unique point on , distinct from , such that . The next axiom concerns copying dividing or intermediate points on a segment. Axiom (C-3). Suppose that and are congruent line segments. If B is a point such that , then there is a point such that , , and . Axiom (C-4). Angle congruence is an equivalence relation for angles. Axiom (C-5). (Copying an angle) Suppose is an angle, and is a ray. Then on any given side of , there is a unique ray such that . Axiom (C-6). (Copying a triangle) Suppose is a triangle, and is a segment such that . Then on any given side of , there is a point such that . (For my private use only. Don't use.) Axiom C-1 C-2, C-3, C-4, C-5, C-6 of [AitkenIBCG] p. 2 . (Contributed by FL, 1-Apr-2016.)
Assertion
Ref Expression
df-ibcg Ibcg Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
Distinct variable group:   ,,,,,,,,,,,,,,,,,,,

Detailed syntax breakdown of Definition df-ibcg
StepHypRef Expression
1 cibcg 25347 . 2 Ibcg
2 vy . . . . . . . . . . . . . . . . . . 19
32cv 1618 . . . . . . . . . . . . . . . . . 18
4 vs . . . . . . . . . . . . . . . . . . 19
54cv 1618 . . . . . . . . . . . . . . . . . 18
63, 5wer 6543 . . . . . . . . . . . . . . . . 17
7 vu . . . . . . . . . . . . . . . . . . . 20
87cv 1618 . . . . . . . . . . . . . . . . . . 19
9 vw . . . . . . . . . . . . . . . . . . . 20
109cv 1618 . . . . . . . . . . . . . . . . . . 19
118, 10cima 4583 . . . . . . . . . . . . . . . . . 18
12 vo . . . . . . . . . . . . . . . . . . 19
1312cv 1618 . . . . . . . . . . . . . . . . . 18
1411, 13wer 6543 . . . . . . . . . . . . . . . . 17
15 vd . . . . . . . . . . . . . . . . . . . . . 22
1615cv 1618 . . . . . . . . . . . . . . . . . . . . 21
17 ve . . . . . . . . . . . . . . . . . . . . . 22
1817cv 1618 . . . . . . . . . . . . . . . . . . . . 21
1916, 18wne 2412 . . . . . . . . . . . . . . . . . . . 20
20 va . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2120cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . 26
22 vb . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2322cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2421, 23wne 2412 . . . . . . . . . . . . . . . . . . . . . . . . 25
25 vf . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2625cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2726, 16wne 2412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
28 vt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2928cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3021, 23, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3116, 26, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3230, 31, 5wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3327, 32wa 360 . . . . . . . . . . . . . . . . . . . . . . . . . 26
34 vr . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3534cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3616, 18, 35co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3733, 25, 36wreu 2511 . . . . . . . . . . . . . . . . . . . . . . . . 25
3824, 37wi 6 . . . . . . . . . . . . . . . . . . . . . . . 24
39 vc . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4039cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
41 vq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4241cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4321, 23, 42co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4440, 43wcel 1621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4516, 18, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4630, 45, 5wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4744, 46wa 360 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4816, 18, 42co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4926, 48wcel 1621 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5021, 40, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5150, 31, 5wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5240, 23, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5326, 18, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5452, 53, 5wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5549, 51, 54w3a 939 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
56 vp . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5756cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5855, 25, 57wrex 2510 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5947, 58wi 6 . . . . . . . . . . . . . . . . . . . . . . . . 25
6059, 39, 57wral 2509 . . . . . . . . . . . . . . . . . . . . . . . 24
6138, 60wa 360 . . . . . . . . . . . . . . . . . . . . . . 23
6261, 22, 57wral 2509 . . . . . . . . . . . . . . . . . . . . . 22
6362, 20, 57wral 2509 . . . . . . . . . . . . . . . . . . . . 21
6421, 8cfv 4592 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6518, 16, 26cs3 11369 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6665, 8cfv 4592 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6764, 66, 13wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . . 25
6867, 25, 23wreu 2511 . . . . . . . . . . . . . . . . . . . . . . . 24
69 vl . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7069cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7116, 18, 70co 5710 . . . . . . . . . . . . . . . . . . . . . . . . 25
72 vx . . . . . . . . . . . . . . . . . . . . . . . . . 26
7372cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . 25
7471, 73cfv 4592 . . . . . . . . . . . . . . . . . . . . . . . 24
7568, 22, 74wral 2509 . . . . . . . . . . . . . . . . . . . . . . 23
76 c1 8618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7776, 21cfv 4592 . . . . . . . . . . . . . . . . . . . . . . . . . 26
78 c2 9675 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7978, 21cfv 4592 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8077, 79, 29co 5710 . . . . . . . . . . . . . . . . . . . . . . . . 25
8180, 45, 5wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . 24
8216, 18, 26cs3 11369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83 vv . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8483cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8582, 84cfv 4592 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
86 vz . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8786cv 1618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8821, 85, 87wbr 3920 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8988, 25, 23wrex 2510 . . . . . . . . . . . . . . . . . . . . . . . . 25
9089, 22, 74wral 2509 . . . . . . . . . . . . . . . . . . . . . . . 24
9181, 90wi 6 . . . . . . . . . . . . . . . . . . . . . . 23
9275, 91wa 360 . . . . . . . . . . . . . . . . . . . . . 22
9392, 20, 10wral 2509 . . . . . . . . . . . . . . . . . . . . 21
9463, 93wa 360 . . . . . . . . . . . . . . . . . . . 20
9519, 94wi 6 . . . . . . . . . . . . . . . . . . 19
9695, 17, 57wral 2509 . . . . . . . . . . . . . . . . . 18
9796, 15, 57wral 2509 . . . . . . . . . . . . . . . . 17
986, 14, 97w3a 939 . . . . . . . . . . . . . . . 16
99 vg . . . . . . . . . . . . . . . . . 18
10099cv 1618 . . . . . . . . . . . . . . . . 17
101 ctrcng 25327 . . . . . . . . . . . . . . . . 17 trcng
102100, 101cfv 4592 . . . . . . . . . . . . . . . 16 trcng
10398, 86, 102wsbc 2921 . . . . . . . . . . . . . . 15 trcng
104 cSeg 25314 . . . . . . . . . . . . . . . 16 Segments
105100, 104cfv 4592 . . . . . . . . . . . . . . 15 Segments
106103, 2, 105wsbc 2921 . . . . . . . . . . . . . 14 Segments trcng
107 chalfp 25336 . . . . . . . . . . . . . . 15 Halfplane
108100, 107cfv 4592 . . . . . . . . . . . . . 14 Halfplane
109106, 72, 108wsbc 2921 . . . . . . . . . . . . 13 Halfplane Segments trcng
110 c3 9676 . . . . . . . . . . . . . 14
111 cdwords 25150 . . . . . . . . . . . . . 14 dWords
11257, 110, 111co 5710 . . . . . . . . . . . . 13 dWords
113109, 9, 112wsbc 2921 . . . . . . . . . . . 12 dWords Halfplane Segments trcng
114 ctriangle 25325 . . . . . . . . . . . . 13 triangle
115100, 114cfv 4592 . . . . . . . . . . . 12 triangle
116113, 83, 115wsbc 2921 . . . . . . . . . . 11 triangle dWords Halfplane Segments trcng
117 cangle 25323 . . . . . . . . . . . 12 angle
118100, 117cfv 4592 . . . . . . . . . . 11 angle
119116, 7, 118wsbc 2921 . . . . . . . . . 10 angle triangle dWords Halfplane Segments trcng
120 cline 25242 . . . . . . . . . . 11
121100, 120cfv 4592 . . . . . . . . . 10
122119, 69, 121wsbc 2921 . . . . . . . . 9 angle triangle dWords Halfplane Segments trcng
123 cseg 25296 . . . . . . . . . 10
124100, 123cfv 4592 . . . . . . . . 9
125122, 28, 124wsbc 2921 . . . . . . . 8 angle triangle dWords Halfplane Segments trcng
126 csegc 25346 . . . . . . . . 9 segc
127100, 126cfv 4592 . . . . . . . 8 segc
128125, 4, 127wsbc 2921 . . . . . . 7 segc angle triangle dWords Halfplane Segments trcng
129 cray2 25317 . . . . . . . 8 ray
130100, 129cfv 4592 . . . . . . 7 ray
131128, 34, 130wsbc 2921 . . . . . 6 ray segc angle triangle dWords Halfplane Segments trcng
132 cbtw 25272 . . . . . . 7 btw
133100, 132cfv 4592 . . . . . 6 btw
134131, 41, 133wsbc 2921 . . . . 5 btw ray segc angle triangle dWords Halfplane Segments trcng
135 cpoints 25222 . . . . . 6 PPoints
136100, 135cfv 4592 . . . . 5 PPoints
137134, 56, 136wsbc 2921 . . . 4 PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
138 cangc 25349 . . . . 5 angc
139100, 138cfv 4592 . . . 4 angc
140137, 12, 139wsbc 2921 . . 3 angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
141 cibg 25273 . . 3 Ibg
142140, 99, 141crab 2512 . 2 Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
1431, 142wceq 1619 1 Ibcg Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
 Colors of variables: wff set class This definition is referenced by:  isibcg  25357
 Copyright terms: Public domain W3C validator