Metamath Proof Explorer


Theorem cgrahl1

Description: Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of Schwabhauser p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020)

Ref Expression
Hypotheses iscgra.p P=BaseG
iscgra.i I=ItvG
iscgra.k K=hl𝒢G
iscgra.g φG𝒢Tarski
iscgra.a φAP
iscgra.b φBP
iscgra.c φCP
iscgra.d φDP
iscgra.e φEP
iscgra.f φFP
cgrahl1.2 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
cgrahl1.x φXP
cgrahl1.1 φXKED
Assertion cgrahl1 φ⟨“ABC”⟩𝒢G⟨“XEF”⟩

Proof

Step Hyp Ref Expression
1 iscgra.p P=BaseG
2 iscgra.i I=ItvG
3 iscgra.k K=hl𝒢G
4 iscgra.g φG𝒢Tarski
5 iscgra.a φAP
6 iscgra.b φBP
7 iscgra.c φCP
8 iscgra.d φDP
9 iscgra.e φEP
10 iscgra.f φFP
11 cgrahl1.2 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
12 cgrahl1.x φXP
13 cgrahl1.1 φXKED
14 4 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFG𝒢Tarski
15 5 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFAP
16 6 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFBP
17 7 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCP
18 12 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFXP
19 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEP
20 10 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFFP
21 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxP
22 simplr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyP
23 simpr1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF⟨“ABC”⟩𝒢G⟨“xEy”⟩
24 8 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDP
25 simpr2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKED
26 13 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFXKED
27 1 2 3 18 24 19 14 26 hlcomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDKEX
28 1 2 3 21 24 18 14 19 25 27 hltr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKEX
29 simpr3 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyKEF
30 1 2 3 14 15 16 17 18 19 20 21 22 23 28 29 iscgrad φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF⟨“ABC”⟩𝒢G⟨“XEF”⟩
31 1 2 3 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
32 11 31 mpbid φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
33 30 32 r19.29vva φ⟨“ABC”⟩𝒢G⟨“XEF”⟩