Metamath Proof Explorer


Theorem flatcgra

Description: Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023)

Ref Expression
Hypotheses cgracol.p P=BaseG
cgracol.i I=ItvG
cgracol.m -˙=distG
cgracol.g φG𝒢Tarski
cgracol.a φAP
cgracol.b φBP
cgracol.c φCP
cgracol.d φDP
cgracol.e φEP
cgracol.f φFP
flatcgra.1 φBAIC
flatcgra.2 φEDIF
flatcgra.3 φAB
flatcgra.4 φCB
flatcgra.5 φDE
flatcgra.6 φFE
Assertion flatcgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩

Proof

Step Hyp Ref Expression
1 cgracol.p P=BaseG
2 cgracol.i I=ItvG
3 cgracol.m -˙=distG
4 cgracol.g φG𝒢Tarski
5 cgracol.a φAP
6 cgracol.b φBP
7 cgracol.c φCP
8 cgracol.d φDP
9 cgracol.e φEP
10 cgracol.f φFP
11 flatcgra.1 φBAIC
12 flatcgra.2 φEDIF
13 flatcgra.3 φAB
14 flatcgra.4 φCB
15 flatcgra.5 φDE
16 flatcgra.6 φFE
17 eqid 𝒢G=𝒢G
18 4 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CG𝒢Tarski
19 5 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CAP
20 6 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CBP
21 7 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CCP
22 simpllr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CxP
23 9 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEP
24 simplr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CyP
25 simprlr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CE-˙x=B-˙A
26 1 3 2 18 23 22 20 19 25 tgcgrcomlr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙Cx-˙E=A-˙B
27 26 eqcomd φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CA-˙B=x-˙E
28 simprrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CE-˙y=B-˙C
29 28 eqcomd φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CB-˙C=E-˙y
30 10 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CFP
31 8 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CDP
32 16 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CFE
33 15 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CDE
34 1 3 2 4 8 9 10 12 tgbtwncom φEFID
35 34 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEFID
36 simprll φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEFIx
37 simprrl φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEDIy
38 1 2 18 30 23 31 22 24 32 33 35 36 37 tgbtwnconn22 φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CExIy
39 11 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CBAIC
40 1 3 2 18 22 23 24 19 20 21 38 39 26 28 tgcgrextend φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙Cx-˙y=A-˙C
41 40 eqcomd φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CA-˙C=x-˙y
42 1 3 2 18 19 21 22 24 41 tgcgrcomlr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CC-˙A=y-˙x
43 1 3 17 18 19 20 21 22 23 24 27 29 42 trgcgr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙C⟨“ABC”⟩𝒢G⟨“xEy”⟩
44 25 eqcomd φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CB-˙A=E-˙x
45 13 necomd φBA
46 45 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CBA
47 1 3 2 18 20 19 23 22 44 46 tgcgrneq φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEx
48 47 necomd φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CxE
49 1 2 18 30 23 22 31 32 36 35 tgbtwnconn2 φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CxEIDDEIx
50 48 33 49 3jca φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CxEDExEIDDEIx
51 eqid hl𝒢G=hl𝒢G
52 1 2 51 22 31 23 18 ishlg φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙Cxhl𝒢GEDxEDExEIDDEIx
53 50 52 mpbird φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙Cxhl𝒢GED
54 14 necomd φBC
55 54 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CBC
56 1 3 2 18 20 21 23 24 29 55 tgcgrneq φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEy
57 56 necomd φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CyE
58 12 ad3antrrr φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CEDIF
59 1 2 18 31 23 24 30 33 37 58 tgbtwnconn2 φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CyEIFFEIy
60 57 32 59 3jca φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CyEFEyEIFFEIy
61 1 2 51 24 30 23 18 ishlg φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙Cyhl𝒢GEFyEFEyEIFFEIy
62 60 61 mpbird φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙Cyhl𝒢GEF
63 43 53 62 3jca φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙C⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEF
64 1 3 2 4 10 9 6 5 axtgsegcon φxPEFIxE-˙x=B-˙A
65 1 3 2 4 8 9 6 7 axtgsegcon φyPEDIyE-˙y=B-˙C
66 reeanv xPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙CxPEFIxE-˙x=B-˙AyPEDIyE-˙y=B-˙C
67 64 65 66 sylanbrc φxPyPEFIxE-˙x=B-˙AEDIyE-˙y=B-˙C
68 63 67 reximddv2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEF
69 1 2 51 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEF
70 68 69 mpbird φ⟨“ABC”⟩𝒢G⟨“DEF”⟩