Metamath Proof Explorer


Theorem cgratr

Description: Angle congruence is transitive. Theorem 11.8 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020)

Ref Expression
Hypotheses cgraid.p P=BaseG
cgraid.i I=ItvG
cgraid.g φG𝒢Tarski
cgraid.k K=hl𝒢G
cgraid.a φAP
cgraid.b φBP
cgraid.c φCP
cgracom.d φDP
cgracom.e φEP
cgracom.f φFP
cgracom.1 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
cgratr.h φHP
cgratr.i φUP
cgratr.j φJP
cgratr.1 φ⟨“DEF”⟩𝒢G⟨“HUJ”⟩
Assertion cgratr φ⟨“ABC”⟩𝒢G⟨“HUJ”⟩

Proof

Step Hyp Ref Expression
1 cgraid.p P=BaseG
2 cgraid.i I=ItvG
3 cgraid.g φG𝒢Tarski
4 cgraid.k K=hl𝒢G
5 cgraid.a φAP
6 cgraid.b φBP
7 cgraid.c φCP
8 cgracom.d φDP
9 cgracom.e φEP
10 cgracom.f φFP
11 cgracom.1 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
12 cgratr.h φHP
13 cgratr.i φUP
14 cgratr.j φJP
15 cgratr.1 φ⟨“DEF”⟩𝒢G⟨“HUJ”⟩
16 eqid distG=distG
17 eqid 𝒢G=𝒢G
18 3 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCG𝒢Tarski
19 5 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCAP
20 6 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCBP
21 7 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCCP
22 simpllr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCxP
23 13 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCUP
24 simplr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCyP
25 simprlr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCUdistGx=BdistGA
26 25 eqcomd φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCBdistGA=UdistGx
27 1 16 2 18 20 19 23 22 26 tgcgrcomlr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCAdistGB=xdistGU
28 simprrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCUdistGy=BdistGC
29 28 eqcomd φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCBdistGC=UdistGy
30 18 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFG𝒢Tarski
31 19 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFAP
32 20 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFBP
33 21 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFCP
34 simpllr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFuP
35 9 ad6antr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFEP
36 simplr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFvP
37 simpr1 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF⟨“ABC”⟩𝒢G⟨“uEv”⟩
38 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp3 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFCdistGA=vdistGu
39 22 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFxP
40 24 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFyP
41 8 ad6antr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFDP
42 10 ad6antr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFFP
43 23 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFUP
44 14 ad6antr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFJP
45 12 ad6antr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFHP
46 15 ad6antr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF⟨“DEF”⟩𝒢G⟨“HUJ”⟩
47 simprll φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCxKUH
48 47 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFxKUH
49 1 2 4 30 41 35 42 45 43 44 46 39 48 cgrahl1 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF⟨“DEF”⟩𝒢G⟨“xUJ”⟩
50 simprrl φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCyKUJ
51 50 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFyKUJ
52 1 2 4 30 41 35 42 39 43 44 49 40 51 cgrahl2 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF⟨“DEF”⟩𝒢G⟨“xUy”⟩
53 simpr2 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFuKED
54 simpr3 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFvKEF
55 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp1 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFAdistGB=udistGE
56 55 eqcomd φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFudistGE=AdistGB
57 1 16 2 30 34 35 31 32 56 tgcgrcomlr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFEdistGu=BdistGA
58 26 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFBdistGA=UdistGx
59 57 58 eqtrd φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFEdistGu=UdistGx
60 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp2 φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFBdistGC=EdistGv
61 29 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFBdistGC=UdistGy
62 60 61 eqtr3d φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFEdistGv=UdistGy
63 1 2 4 30 41 35 42 39 43 40 52 34 16 36 53 54 59 62 cgracgr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFudistGv=xdistGy
64 1 16 2 30 34 36 39 40 63 tgcgrcomlr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFvdistGu=ydistGx
65 38 64 eqtrd φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEFCdistGA=ydistGx
66 1 2 4 3 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩uPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF
67 11 66 mpbid φuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF
68 67 ad3antrrr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCuPvP⟨“ABC”⟩𝒢G⟨“uEv”⟩uKEDvKEF
69 65 68 r19.29vva φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCCdistGA=ydistGx
70 1 16 17 18 19 20 21 22 23 24 27 29 69 trgcgr φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGC⟨“ABC”⟩𝒢G⟨“xUy”⟩
71 70 47 50 3jca φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGC⟨“ABC”⟩𝒢G⟨“xUy”⟩xKUHyKUJ
72 1 2 4 3 8 9 10 12 13 14 15 cgrane3 φUH
73 72 necomd φHU
74 1 2 4 3 5 6 7 8 9 10 11 cgrane1 φAB
75 74 necomd φBA
76 1 2 4 13 6 5 3 12 16 73 75 hlcgrex φxPxKUHUdistGx=BdistGA
77 1 2 4 3 8 9 10 12 13 14 15 cgrane4 φUJ
78 77 necomd φJU
79 1 2 4 3 5 6 7 8 9 10 11 cgrane2 φBC
80 1 2 4 13 6 7 3 14 16 78 79 hlcgrex φyPyKUJUdistGy=BdistGC
81 reeanv xPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGCxPxKUHUdistGx=BdistGAyPyKUJUdistGy=BdistGC
82 76 80 81 sylanbrc φxPyPxKUHUdistGx=BdistGAyKUJUdistGy=BdistGC
83 71 82 reximddv2 φxPyP⟨“ABC”⟩𝒢G⟨“xUy”⟩xKUHyKUJ
84 1 2 4 3 5 6 7 12 13 14 iscgra φ⟨“ABC”⟩𝒢G⟨“HUJ”⟩xPyP⟨“ABC”⟩𝒢G⟨“xUy”⟩xKUHyKUJ
85 83 84 mpbird φ⟨“ABC”⟩𝒢G⟨“HUJ”⟩