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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
iscgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
iscgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
iscgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
iscgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
iscgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
iscgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
iscgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
iscgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
iscgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
cgrahl1.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgrahl1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
cgrahl1.1 ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 )
Assertion cgrahl1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 iscgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 iscgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 iscgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 iscgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 iscgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 iscgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 iscgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 iscgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 iscgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 iscgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 cgrahl1.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12 cgrahl1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
13 cgrahl1.1 ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 )
14 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
15 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐴 ∈ 𝑃 )
16 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ∈ 𝑃 )
17 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐶 ∈ 𝑃 )
18 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑋 ∈ 𝑃 )
19 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ 𝑃 )
20 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐹 ∈ 𝑃 )
21 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ∈ 𝑃 )
22 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ∈ 𝑃 )
23 simpr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
24 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ∈ 𝑃 )
25 simpr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 )
26 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 )
27 1 2 3 18 24 19 14 26 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑋 )
28 1 2 3 21 24 18 14 19 25 27 hltr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 )
29 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 )
30 1 2 3 14 15 16 17 18 19 20 21 22 23 28 29 iscgrad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝐹 ”⟩ )
31 1 2 3 4 5 6 7 8 9 10 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
32 11 31 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
33 30 32 r19.29vva ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝐹 ”⟩ )