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 = Base G
iscgra.i I = Itv G
iscgra.k K = hl 𝒢 G
iscgra.g φ G 𝒢 Tarski
iscgra.a φ A P
iscgra.b φ B P
iscgra.c φ C P
iscgra.d φ D P
iscgra.e φ E P
iscgra.f φ F P
cgrahl1.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
cgrahl1.x φ X P
cgrahl1.1 φ X K E D
Assertion cgrahl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEF ”⟩

Proof

Step Hyp Ref Expression
1 iscgra.p P = Base G
2 iscgra.i I = Itv G
3 iscgra.k K = hl 𝒢 G
4 iscgra.g φ G 𝒢 Tarski
5 iscgra.a φ A P
6 iscgra.b φ B P
7 iscgra.c φ C P
8 iscgra.d φ D P
9 iscgra.e φ E P
10 iscgra.f φ F P
11 cgrahl1.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
12 cgrahl1.x φ X P
13 cgrahl1.1 φ X K E D
14 4 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F G 𝒢 Tarski
15 5 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A P
16 6 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B P
17 7 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F C P
18 12 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F X P
19 9 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F E P
20 10 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F F P
21 simpllr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x P
22 simplr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y P
23 simpr1 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩
24 8 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F D P
25 simpr2 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x K E D
26 13 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F X K E D
27 1 2 3 18 24 19 14 26 hlcomd φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F D K E X
28 1 2 3 21 24 18 14 19 25 27 hltr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x K E X
29 simpr3 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y K E F
30 1 2 3 14 15 16 17 18 19 20 21 22 23 28 29 iscgrad φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEF ”⟩
31 1 2 3 4 5 6 7 8 9 10 iscgra φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
32 11 31 mpbid φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
33 30 32 r19.29vva φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEF ”⟩