Metamath Proof Explorer


Theorem cgrahl

Description: Angle congruence preserves null 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”⟩
cgrahl.k K=hl𝒢G
cgrahl.2 φAKBC
Assertion cgrahl φDKEF

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 cgrahl.k K=hl𝒢G
13 cgrahl.2 φAKBC
14 8 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDP
15 simplr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyP
16 10 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFFP
17 4 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFG𝒢Tarski
18 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEP
19 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxP
20 simpr2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKED
21 1 2 12 19 14 18 17 20 hlcomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDKEx
22 1 2 12 19 14 18 17 20 hlne1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxE
23 simpr3 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyKEF
24 1 2 12 15 16 18 17 23 hlne1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyE
25 eqid 𝒢G=𝒢G
26 17 adantr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICG𝒢Tarski
27 6 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICBP
28 5 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICAP
29 7 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICCP
30 18 adantr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICEP
31 19 adantr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICxP
32 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICyP
33 simplr1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABIC⟨“ABC”⟩𝒢G⟨“xEy”⟩
34 1 3 2 25 26 28 27 29 31 30 32 33 cgr3swap12 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABIC⟨“BAC”⟩𝒢G⟨“Exy”⟩
35 simpr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICABIC
36 1 3 2 25 26 27 28 29 30 31 32 34 35 tgbtwnxfr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICxEIy
37 36 orcd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICxEIyyEIx
38 4 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAG𝒢Tarski
39 6 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIABP
40 7 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIACP
41 5 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAAP
42 9 ad4antr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAEP
43 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAyP
44 19 adantr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAxP
45 simplr1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIA⟨“ABC”⟩𝒢G⟨“xEy”⟩
46 1 3 2 25 38 41 39 40 44 42 43 45 cgr3rotl φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIA⟨“BCA”⟩𝒢G⟨“Eyx”⟩
47 simpr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIACBIA
48 1 3 2 25 38 39 40 41 42 43 44 46 47 tgbtwnxfr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAyEIx
49 48 olcd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCBIAxEIyyEIx
50 1 2 12 5 7 6 4 ishlg φAKBCABCBABICCBIA
51 13 50 mpbid φABCBABICCBIA
52 51 simp3d φABICCBIA
53 52 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFABICCBIA
54 37 49 53 mpjaodan φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxEIyyEIx
55 1 2 12 19 15 18 17 ishlg φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKEyxEyExEIyyEIx
56 22 24 54 55 mpbir3and φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKEy
57 1 2 12 14 19 15 17 18 21 56 hltr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDKEy
58 1 2 12 14 15 16 17 18 57 23 hltr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDKEF
59 1 2 12 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
60 11 59 mpbid φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
61 58 60 r19.29vva φDKEF