Metamath Proof Explorer

Theorem cgrahl

Description: Angle congruence preserves null 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 ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgrahl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
cgrahl.2 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
Assertion cgrahl ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )

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 cgrahl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
13 cgrahl.2 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
14 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ∈ 𝑃 )
15 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ∈ 𝑃 )
16 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐹 ∈ 𝑃 )
17 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
18 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ 𝑃 )
19 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ∈ 𝑃 )
20 simpr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 )
21 1 2 12 19 14 18 17 20 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑥 )
22 1 2 12 19 14 18 17 20 hlne1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ≠ 𝐸 )
23 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 )
24 1 2 12 15 16 18 17 23 hlne1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ≠ 𝐸 )
25 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
26 17 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
27 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
28 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
29 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
30 18 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐸 ∈ 𝑃 )
31 19 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝑥 ∈ 𝑃 )
32 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝑦 ∈ 𝑃 )
33 simplr1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
34 1 3 2 25 26 28 27 29 31 30 32 33 cgr3swap12 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑥 𝑦 ”⟩ )
35 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )
36 1 3 2 25 26 27 28 29 30 31 32 34 35 tgbtwnxfr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) )
37 36 orcd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) )
38 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
39 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑃 )
40 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐶 ∈ 𝑃 )
41 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
42 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐸 ∈ 𝑃 )
43 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝑦 ∈ 𝑃 )
44 19 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝑥 ∈ 𝑃 )
45 simplr1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
46 1 3 2 25 38 41 39 40 44 42 43 45 cgr3rotl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑥 ”⟩ )
47 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) )
48 1 3 2 25 38 39 40 41 42 43 44 46 47 tgbtwnxfr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) )
49 48 olcd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) )
50 1 2 12 5 7 6 4 ishlg ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) ) ) )
51 13 50 mpbid ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) ) )
52 51 simp3d ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) )
53 52 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) )
54 37 49 53 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) )
55 1 2 12 19 15 18 17 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑦 ↔ ( 𝑥 ≠ 𝐸 ∧ 𝑦 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) ) ) )
56 22 24 54 55 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑦 )
57 1 2 12 14 19 15 17 18 21 56 hltr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑦 )
58 1 2 12 14 15 16 17 18 57 23 hltr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
59 1 2 12 4 5 6 7 8 9 10 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
60 11 59 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
61 58 60 r19.29vva ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )