Metamath Proof Explorer


Theorem cgrabtwn

Description: Angle congruence preserves flat angles. Part of Theorem 11.21 of Schwabhauser p. 97. (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”⟩
cgrabtwn.2 φBAIC
Assertion cgrabtwn φEDIF

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 cgrabtwn.2 φBAIC
13 eqid hl𝒢G=hl𝒢G
14 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFxP
15 8 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFDP
16 10 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFFP
17 4 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFG𝒢Tarski
18 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFEP
19 simpr2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFxhl𝒢GED
20 simplr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFyP
21 simpr3 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFyhl𝒢GEF
22 eqid 𝒢G=𝒢G
23 5 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFAP
24 6 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFBP
25 7 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFCP
26 simpr1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEF⟨“ABC”⟩𝒢G⟨“xEy”⟩
27 12 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFBAIC
28 1 3 2 22 17 23 24 25 14 18 20 26 27 tgbtwnxfr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFExIy
29 1 3 2 17 14 18 20 28 tgbtwncom φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFEyIx
30 1 2 13 20 16 14 17 18 21 29 btwnhl φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFEFIx
31 1 3 2 17 16 18 14 30 tgbtwncom φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFExIF
32 1 2 13 14 15 16 17 18 19 31 btwnhl φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEFEDIF
33 1 2 13 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEF
34 11 33 mpbid φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xhl𝒢GEDyhl𝒢GEF
35 32 34 r19.29vva φEDIF