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 ‘ 𝐺 ) ⟨“ 𝑌 𝐸 𝐹 ”⟩ )