Metamath Proof Explorer


Theorem cgracol

Description: Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020)

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
cgracol.1 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
cgracol.l L=Line𝒢G
cgracol.2 φCALBA=B
Assertion cgracol φFDLED=E

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 cgracol.1 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
12 cgracol.l L=Line𝒢G
13 cgracol.2 φCALBA=B
14 4 adantr φCAIBACIBG𝒢Tarski
15 5 adantr φCAIBACIBAP
16 6 adantr φCAIBACIBBP
17 7 adantr φCAIBACIBCP
18 8 adantr φCAIBACIBDP
19 9 adantr φCAIBACIBEP
20 10 adantr φCAIBACIBFP
21 11 adantr φCAIBACIB⟨“ABC”⟩𝒢G⟨“DEF”⟩
22 eqid hl𝒢G=hl𝒢G
23 1 2 22 4 5 6 7 8 9 10 11 cgrane2 φBC
24 23 necomd φCB
25 24 adantr φCAIBCB
26 1 2 22 4 5 6 7 8 9 10 11 cgrane1 φAB
27 26 adantr φCAIBAB
28 4 adantr φCAIBG𝒢Tarski
29 5 adantr φCAIBAP
30 7 adantr φCAIBCP
31 6 adantr φCAIBBP
32 simpr φCAIBCAIB
33 1 3 2 28 29 30 31 32 tgbtwncom φCAIBCBIA
34 33 orcd φCAIBCBIAABIC
35 25 27 34 3jca φCAIBCBABCBIAABIC
36 24 adantr φACIBCB
37 26 adantr φACIBAB
38 4 adantr φACIBG𝒢Tarski
39 7 adantr φACIBCP
40 5 adantr φACIBAP
41 6 adantr φACIBBP
42 simpr φACIBACIB
43 1 3 2 38 39 40 41 42 tgbtwncom φACIBABIC
44 43 olcd φACIBCBIAABIC
45 36 37 44 3jca φACIBCBABCBIAABIC
46 35 45 jaodan φCAIBACIBCBABCBIAABIC
47 1 2 22 7 5 6 4 ishlg φChl𝒢GBACBABCBIAABIC
48 47 adantr φCAIBACIBChl𝒢GBACBABCBIAABIC
49 46 48 mpbird φCAIBACIBChl𝒢GBA
50 1 2 22 17 15 16 14 49 hlcomd φCAIBACIBAhl𝒢GBC
51 1 2 3 14 15 16 17 18 19 20 21 22 50 cgrahl φCAIBACIBDhl𝒢GEF
52 1 2 22 18 20 19 14 ishlg φCAIBACIBDhl𝒢GEFDEFEDEIFFEID
53 51 52 mpbid φCAIBACIBDEFEDEIFFEID
54 53 simp3d φCAIBACIBDEIFFEID
55 4 adantr φDEIFG𝒢Tarski
56 9 adantr φDEIFEP
57 8 adantr φDEIFDP
58 10 adantr φDEIFFP
59 simpr φDEIFDEIF
60 1 3 2 55 56 57 58 59 tgbtwncom φDEIFDFIE
61 60 olcd φDEIFFDIEDFIE
62 4 adantr φFEIDG𝒢Tarski
63 9 adantr φFEIDEP
64 10 adantr φFEIDFP
65 8 adantr φFEIDDP
66 simpr φFEIDFEID
67 1 3 2 62 63 64 65 66 tgbtwncom φFEIDFDIE
68 67 orcd φFEIDFDIEDFIE
69 61 68 jaodan φDEIFFEIDFDIEDFIE
70 54 69 syldan φCAIBACIBFDIEDFIE
71 70 orcd φCAIBACIBFDIEDFIEEDIF
72 df-3or FDIEDFIEEDIFFDIEDFIEEDIF
73 71 72 sylibr φCAIBACIBFDIEDFIEEDIF
74 1 2 4 22 5 6 7 8 9 10 11 cgracom φ⟨“DEF”⟩𝒢G⟨“ABC”⟩
75 1 2 22 4 8 9 10 5 6 7 74 cgrane1 φDE
76 1 12 2 4 8 9 75 10 tgellng φFDLEFDIEDFIEEDIF
77 76 adantr φCAIBACIBFDLEFDIEDFIEEDIF
78 73 77 mpbird φCAIBACIBFDLE
79 78 orcd φCAIBACIBFDLED=E
80 4 adantr φBAICG𝒢Tarski
81 8 adantr φBAICDP
82 9 adantr φBAICEP
83 10 adantr φBAICFP
84 5 adantr φBAICAP
85 6 adantr φBAICBP
86 7 adantr φBAICCP
87 11 adantr φBAIC⟨“ABC”⟩𝒢G⟨“DEF”⟩
88 simpr φBAICBAIC
89 1 2 3 80 84 85 86 81 82 83 87 88 cgrabtwn φBAICEDIF
90 1 12 2 80 81 82 83 89 btwncolg3 φBAICFDLED=E
91 26 neneqd φ¬A=B
92 13 orcomd φA=BCALB
93 92 ord φ¬A=BCALB
94 91 93 mpd φCALB
95 1 12 2 4 5 6 26 7 tgellng φCALBCAIBACIBBAIC
96 94 95 mpbid φCAIBACIBBAIC
97 df-3or CAIBACIBBAICCAIBACIBBAIC
98 96 97 sylib φCAIBACIBBAIC
99 79 90 98 mpjaodan φFDLED=E