Metamath Proof Explorer


Theorem cgrahl2

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
cgrahl2.1 φXKEF
Assertion cgrahl2 φ⟨“ABC”⟩𝒢G⟨“DEX”⟩

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 cgrahl2.1 φXKEF
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 8 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDP
19 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEP
20 12 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFXP
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 simpr2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKED
25 10 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFFP
26 simpr3 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyKEF
27 13 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFXKEF
28 1 2 3 20 25 19 14 27 hlcomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFFKEX
29 1 2 3 22 25 20 14 19 26 28 hltr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyKEX
30 1 2 3 14 15 16 17 18 19 20 21 22 23 24 29 iscgrad φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF⟨“ABC”⟩𝒢G⟨“DEX”⟩
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⟨“DEX”⟩