Metamath Proof Explorer


Theorem sacgr

Description: Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020) (Proof shortened by Igor Ieskov, 16-Feb-2023)

Ref Expression
Hypotheses dfcgra2.p 𝑃 = ( Base ‘ 𝐺 )
dfcgra2.i 𝐼 = ( Itv ‘ 𝐺 )
dfcgra2.m = ( dist ‘ 𝐺 )
dfcgra2.g ( 𝜑𝐺 ∈ TarskiG )
dfcgra2.a ( 𝜑𝐴𝑃 )
dfcgra2.b ( 𝜑𝐵𝑃 )
dfcgra2.c ( 𝜑𝐶𝑃 )
dfcgra2.d ( 𝜑𝐷𝑃 )
dfcgra2.e ( 𝜑𝐸𝑃 )
dfcgra2.f ( 𝜑𝐹𝑃 )
sacgr.x ( 𝜑𝑋𝑃 )
sacgr.y ( 𝜑𝑌𝑃 )
sacgr.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
sacgr.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝑋 ) )
sacgr.3 ( 𝜑𝐸 ∈ ( 𝐷 𝐼 𝑌 ) )
sacgr.4 ( 𝜑𝐵𝑋 )
sacgr.5 ( 𝜑𝐸𝑌 )
Assertion sacgr ( 𝜑 → ⟨“ 𝑋 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑌 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 dfcgra2.p 𝑃 = ( Base ‘ 𝐺 )
2 dfcgra2.i 𝐼 = ( Itv ‘ 𝐺 )
3 dfcgra2.m = ( dist ‘ 𝐺 )
4 dfcgra2.g ( 𝜑𝐺 ∈ TarskiG )
5 dfcgra2.a ( 𝜑𝐴𝑃 )
6 dfcgra2.b ( 𝜑𝐵𝑃 )
7 dfcgra2.c ( 𝜑𝐶𝑃 )
8 dfcgra2.d ( 𝜑𝐷𝑃 )
9 dfcgra2.e ( 𝜑𝐸𝑃 )
10 dfcgra2.f ( 𝜑𝐹𝑃 )
11 sacgr.x ( 𝜑𝑋𝑃 )
12 sacgr.y ( 𝜑𝑌𝑃 )
13 sacgr.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
14 sacgr.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝑋 ) )
15 sacgr.3 ( 𝜑𝐸 ∈ ( 𝐷 𝐼 𝑌 ) )
16 sacgr.4 ( 𝜑𝐵𝑋 )
17 sacgr.5 ( 𝜑𝐸𝑌 )
18 eqid ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
19 4 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
20 11 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑋𝑃 )
21 6 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐵𝑃 )
22 7 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐶𝑃 )
23 12 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑌𝑃 )
24 9 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸𝑃 )
25 10 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐹𝑃 )
26 eqid ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
27 eqid ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
28 eqid ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 )
29 simpllr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑥𝑃 )
30 1 3 2 26 27 19 24 28 29 mircl ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ∈ 𝑃 )
31 simplr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑦𝑃 )
32 eqid ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 )
33 1 3 2 26 27 4 6 32 11 mirmir ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) = 𝑋 )
34 eqidd ( 𝜑𝐵 = 𝐵 )
35 eqidd ( 𝜑𝐶 = 𝐶 )
36 33 34 35 s3eqd ( 𝜑 → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) 𝐵 𝐶 ”⟩ = ⟨“ 𝑋 𝐵 𝐶 ”⟩ )
37 36 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) 𝐵 𝐶 ”⟩ = ⟨“ 𝑋 𝐵 𝐶 ”⟩ )
38 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
39 1 3 2 26 27 4 6 32 11 mircl ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ∈ 𝑃 )
40 39 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ∈ 𝑃 )
41 16 necomd ( 𝜑𝑋𝐵 )
42 1 3 2 26 27 4 6 32 11 41 mirne ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ≠ 𝐵 )
43 42 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ≠ 𝐵 )
44 simpr1 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
45 1 3 2 26 27 19 38 32 28 40 21 29 24 22 31 43 44 mirtrcgr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) 𝐸 𝑦 ”⟩ )
46 37 45 eqbrtrrd ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝑋 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) 𝐸 𝑦 ”⟩ )
47 17 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸𝑌 )
48 47 necomd ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑌𝐸 )
49 8 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐷𝑃 )
50 simpr2 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
51 1 2 18 29 49 24 19 50 hlne1 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑥𝐸 )
52 1 3 2 26 27 19 24 28 29 51 mirne ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ≠ 𝐸 )
53 1 2 18 29 49 24 19 50 hlcomd ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑥 )
54 15 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑌 ) )
55 1 2 18 49 29 23 19 24 53 54 btwnhl ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝑥 𝐼 𝑌 ) )
56 1 3 2 19 29 24 23 55 tgbtwncom ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝑌 𝐼 𝑥 ) )
57 1 3 2 26 27 19 24 28 29 mirmir ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) = 𝑥 )
58 57 oveq2d ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( 𝑌 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) ) = ( 𝑌 𝐼 𝑥 ) )
59 56 58 eleqtrrd ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝑌 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) ) )
60 1 3 2 26 27 19 28 18 24 23 30 24 48 52 59 mirhl2 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑌 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) )
61 1 2 18 23 30 24 19 60 hlcomd ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑌 )
62 simpr3 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
63 1 2 18 19 20 21 22 23 24 25 30 31 46 61 62 iscgrad ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝑋 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑌 𝐸 𝐹 ”⟩ )
64 1 2 18 4 5 6 7 8 9 10 13 cgrane2 ( 𝜑𝐵𝐶 )
65 1 2 4 18 39 6 7 42 64 cgraid ( 𝜑 → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ )
66 1 2 18 4 5 6 7 8 9 10 13 cgrane1 ( 𝜑𝐴𝐵 )
67 33 oveq2d ( 𝜑 → ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) ) = ( 𝐴 𝐼 𝑋 ) )
68 14 67 eleqtrrd ( 𝜑𝐵 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) ) )
69 1 3 2 26 27 4 32 18 6 5 39 5 66 42 68 mirhl2 ( 𝜑𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) )
70 1 2 18 4 39 6 7 39 6 7 65 5 69 cgrahl1 ( 𝜑 → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
71 1 2 4 18 39 6 7 5 6 7 70 8 9 10 13 cgratr ( 𝜑 → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
72 1 2 18 4 39 6 7 8 9 10 iscgra ( 𝜑 → ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥𝑃𝑦𝑃 ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) )
73 71 72 mpbid ( 𝜑 → ∃ 𝑥𝑃𝑦𝑃 ( ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) )
74 63 73 r19.29vva ( 𝜑 → ⟨“ 𝑋 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑌 𝐸 𝐹 ”⟩ )