Metamath Proof Explorer


Theorem segconeq

Description: Two points that satisfy the conclusion of axsegcon are identical. Uniqueness portion of Theorem 2.12 of Schwabhauser p. 29. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion segconeq N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C X = Y

Proof

Step Hyp Ref Expression
1 simpr2l N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q X
2 1 1 jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q X A Btwn Q X
3 simpl1 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C N
4 simpl31 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q 𝔼 N
5 simpl21 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A 𝔼 N
6 3 4 5 cgrrflxd N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q A Cgr Q A
7 simpl32 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C X 𝔼 N
8 3 5 7 cgrrflxd N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A X Cgr A X
9 6 8 jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q A Cgr Q A A X Cgr A X
10 simpl33 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Y 𝔼 N
11 4 5 10 3jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q 𝔼 N A 𝔼 N Y 𝔼 N
12 4 5 7 3jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q 𝔼 N A 𝔼 N X 𝔼 N
13 3 11 12 3jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C N Q 𝔼 N A 𝔼 N Y 𝔼 N Q 𝔼 N A 𝔼 N X 𝔼 N
14 simpr3l N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q Y
15 14 1 jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q Y A Btwn Q X
16 simpl22 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C B 𝔼 N
17 simpl23 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C C 𝔼 N
18 simpr3r N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Y Cgr B C
19 cgrcom N A 𝔼 N Y 𝔼 N B 𝔼 N C 𝔼 N A Y Cgr B C B C Cgr A Y
20 3 5 10 16 17 19 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Y Cgr B C B C Cgr A Y
21 18 20 mpbid N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C B C Cgr A Y
22 simpr2r N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A X Cgr B C
23 cgrcom N A 𝔼 N X 𝔼 N B 𝔼 N C 𝔼 N A X Cgr B C B C Cgr A X
24 3 5 7 16 17 23 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A X Cgr B C B C Cgr A X
25 22 24 mpbid N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C B C Cgr A X
26 3 16 17 5 10 5 7 21 25 cgrtr4d N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Y Cgr A X
27 15 6 26 jca32 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q Y A Btwn Q X Q A Cgr Q A A Y Cgr A X
28 cgrextend N Q 𝔼 N A 𝔼 N Y 𝔼 N Q 𝔼 N A 𝔼 N X 𝔼 N A Btwn Q Y A Btwn Q X Q A Cgr Q A A Y Cgr A X Q Y Cgr Q X
29 13 27 28 sylc N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q Y Cgr Q X
30 29 26 jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q Y Cgr Q X A Y Cgr A X
31 2 9 30 3jca N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q X A Btwn Q X Q A Cgr Q A A X Cgr A X Q Y Cgr Q X A Y Cgr A X
32 31 ex N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C A Btwn Q X A Btwn Q X Q A Cgr Q A A X Cgr A X Q Y Cgr Q X A Y Cgr A X
33 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N N
34 simp31 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q 𝔼 N
35 simp21 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N A 𝔼 N
36 simp32 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N X 𝔼 N
37 simp33 N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Y 𝔼 N
38 brofs N Q 𝔼 N A 𝔼 N X 𝔼 N Y 𝔼 N Q 𝔼 N A 𝔼 N X 𝔼 N X 𝔼 N Q A X Y OuterFiveSeg Q A X X A Btwn Q X A Btwn Q X Q A Cgr Q A A X Cgr A X Q Y Cgr Q X A Y Cgr A X
39 33 34 35 36 37 34 35 36 36 38 syl333anc N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A X Y OuterFiveSeg Q A X X A Btwn Q X A Btwn Q X Q A Cgr Q A A X Cgr A X Q Y Cgr Q X A Y Cgr A X
40 32 39 sylibrd N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q A X Y OuterFiveSeg Q A X X
41 simp1 Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q A
42 41 a1i N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q A
43 40 42 jcad N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C Q A X Y OuterFiveSeg Q A X X Q A
44 5segofs N Q 𝔼 N A 𝔼 N X 𝔼 N Y 𝔼 N Q 𝔼 N A 𝔼 N X 𝔼 N X 𝔼 N Q A X Y OuterFiveSeg Q A X X Q A X Y Cgr X X
45 33 34 35 36 37 34 35 36 36 44 syl333anc N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A X Y OuterFiveSeg Q A X X Q A X Y Cgr X X
46 axcgrid N X 𝔼 N Y 𝔼 N X 𝔼 N X Y Cgr X X X = Y
47 33 36 37 36 46 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N X Y Cgr X X X = Y
48 43 45 47 3syld N A 𝔼 N B 𝔼 N C 𝔼 N Q 𝔼 N X 𝔼 N Y 𝔼 N Q A A Btwn Q X A X Cgr B C A Btwn Q Y A Y Cgr B C X = Y