Metamath Proof Explorer

Theorem cgrabtwn

Description: Angle congruence preserves flat angles. Part of Theorem 11.21 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses cgracol.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgracol.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
cgracol.m ⊢ − = ( dist ‘ 𝐺 )
cgracol.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
cgracol.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
cgracol.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
cgracol.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
cgracol.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
cgracol.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
cgracol.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
cgracol.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgrabtwn.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
Assertion cgrabtwn ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )

Proof

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