Metamath Proof Explorer

Theorem cgraswap

Description: Swap rays in a congruence relation. Theorem 11.9 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020)

Ref Expression
Hypotheses cgraid.p âŠĒ 𝑃 = ( Base ‘ 𝐚 )
cgraid.i âŠĒ 𝐞 = ( Itv ‘ 𝐚 )
cgraid.g âŠĒ ( 𝜑 → 𝐚 ∈ TarskiG )
cgraid.k âŠĒ ðū = ( hlG ‘ 𝐚 )
cgraid.a âŠĒ ( 𝜑 → ðī ∈ 𝑃 )
cgraid.b âŠĒ ( 𝜑 → ðĩ ∈ 𝑃 )
cgraid.c âŠĒ ( 𝜑 → ðķ ∈ 𝑃 )
cgraid.1 âŠĒ ( 𝜑 → ðī ≠ ðĩ )
cgraid.2 âŠĒ ( 𝜑 → ðĩ ≠ ðķ )
Assertion cgraswap ( 𝜑 → âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrA ‘ 𝐚 ) âŸĻ“ ðķ ðĩ ðī ”âŸĐ )

Proof

Step Hyp Ref Expression
1 cgraid.p âŠĒ 𝑃 = ( Base ‘ 𝐚 )
2 cgraid.i âŠĒ 𝐞 = ( Itv ‘ 𝐚 )
3 cgraid.g âŠĒ ( 𝜑 → 𝐚 ∈ TarskiG )
4 cgraid.k âŠĒ ðū = ( hlG ‘ 𝐚 )
5 cgraid.a âŠĒ ( 𝜑 → ðī ∈ 𝑃 )
6 cgraid.b âŠĒ ( 𝜑 → ðĩ ∈ 𝑃 )
7 cgraid.c âŠĒ ( 𝜑 → ðķ ∈ 𝑃 )
8 cgraid.1 âŠĒ ( 𝜑 → ðī ≠ ðĩ )
9 cgraid.2 âŠĒ ( 𝜑 → ðĩ ≠ ðķ )
10 eqid âŠĒ ( dist ‘ 𝐚 ) = ( dist ‘ 𝐚 )
11 eqid âŠĒ ( cgrG ‘ 𝐚 ) = ( cgrG ‘ 𝐚 )
12 3 ad3antrrr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → 𝐚 ∈ TarskiG )
13 5 ad3antrrr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ðī ∈ 𝑃 )
14 6 ad3antrrr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ðĩ ∈ 𝑃 )
15 7 ad3antrrr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ðķ ∈ 𝑃 )
16 simpllr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ð‘Ĩ ∈ 𝑃 )
17 simplr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ð‘Ķ ∈ 𝑃 )
18 simprlr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) )
19 1 10 2 12 14 16 14 13 18 tgcgrcomlr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ĩ ( dist ‘ 𝐚 ) ðĩ ) = ( ðī ( dist ‘ 𝐚 ) ðĩ ) )
20 19 eqcomd âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðī ( dist ‘ 𝐚 ) ðĩ ) = ( ð‘Ĩ ( dist ‘ 𝐚 ) ðĩ ) )
21 simprrr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) )
22 21 eqcomd âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðĩ ( dist ‘ 𝐚 ) ðķ ) = ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) )
23 eqid âŠĒ ( LineG ‘ 𝐚 ) = ( LineG ‘ 𝐚 )
24 simprll âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ð‘Ĩ ( ðū ‘ ðĩ ) ðķ )
25 1 2 4 16 15 14 12 23 24 hlln âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ð‘Ĩ ∈ ( ðķ ( LineG ‘ 𝐚 ) ðĩ ) )
26 25 orcd âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ĩ ∈ ( ðķ ( LineG ‘ 𝐚 ) ðĩ ) âˆĻ ðķ = ðĩ ) )
27 1 23 2 12 15 14 16 26 colrot1 âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðķ ∈ ( ðĩ ( LineG ‘ 𝐚 ) ð‘Ĩ ) âˆĻ ðĩ = ð‘Ĩ ) )
28 eqid âŠĒ ( â‰ĪG ‘ 𝐚 ) = ( â‰ĪG ‘ 𝐚 )
29 1 2 4 16 15 14 12 ishlg âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ↔ ( ð‘Ĩ ≠ ðĩ ∧ ðķ ≠ ðĩ ∧ ( ð‘Ĩ ∈ ( ðĩ 𝐞 ðķ ) âˆĻ ðķ ∈ ( ðĩ 𝐞 ð‘Ĩ ) ) ) ) )
30 24 29 mpbid âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ĩ ≠ ðĩ ∧ ðķ ≠ ðĩ ∧ ( ð‘Ĩ ∈ ( ðĩ 𝐞 ðķ ) âˆĻ ðķ ∈ ( ðĩ 𝐞 ð‘Ĩ ) ) ) )
31 30 simp3d âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ĩ ∈ ( ðĩ 𝐞 ðķ ) âˆĻ ðķ ∈ ( ðĩ 𝐞 ð‘Ĩ ) ) )
32 31 orcomd âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðķ ∈ ( ðĩ 𝐞 ð‘Ĩ ) âˆĻ ð‘Ĩ ∈ ( ðĩ 𝐞 ðķ ) ) )
33 simprrl âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ð‘Ķ ( ðū ‘ ðĩ ) ðī )
34 1 2 4 17 13 14 12 ishlg âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ↔ ( ð‘Ķ ≠ ðĩ ∧ ðī ≠ ðĩ ∧ ( ð‘Ķ ∈ ( ðĩ 𝐞 ðī ) âˆĻ ðī ∈ ( ðĩ 𝐞 ð‘Ķ ) ) ) ) )
35 33 34 mpbid âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ķ ≠ ðĩ ∧ ðī ≠ ðĩ ∧ ( ð‘Ķ ∈ ( ðĩ 𝐞 ðī ) âˆĻ ðī ∈ ( ðĩ 𝐞 ð‘Ķ ) ) ) )
36 35 simp3d âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ķ ∈ ( ðĩ 𝐞 ðī ) âˆĻ ðī ∈ ( ðĩ 𝐞 ð‘Ķ ) ) )
37 1 10 2 28 12 14 15 16 14 14 17 13 32 36 22 18 tgcgrsub2 âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðķ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ð‘Ķ ( dist ‘ 𝐚 ) ðī ) )
38 1 10 11 12 14 15 16 14 17 13 22 37 19 trgcgr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → âŸĻ“ ðĩ ðķ ð‘Ĩ ”âŸĐ ( cgrG ‘ 𝐚 ) âŸĻ“ ðĩ ð‘Ķ ðī ”âŸĐ )
39 1 10 2 12 15 17 axtgcgrrflx âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðķ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ð‘Ķ ( dist ‘ 𝐚 ) ðķ ) )
40 9 ad3antrrr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ðĩ ≠ ðķ )
41 1 23 2 12 14 15 16 11 14 17 10 17 13 15 27 38 21 39 40 tgfscgr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðī ( dist ‘ 𝐚 ) ðķ ) )
42 1 10 2 12 16 17 13 15 41 tgcgrcomlr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ð‘Ķ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðķ ( dist ‘ 𝐚 ) ðī ) )
43 42 eqcomd âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( ðķ ( dist ‘ 𝐚 ) ðī ) = ( ð‘Ķ ( dist ‘ 𝐚 ) ð‘Ĩ ) )
44 1 10 11 12 13 14 15 16 14 17 20 22 43 trgcgr âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrG ‘ 𝐚 ) âŸĻ“ ð‘Ĩ ðĩ ð‘Ķ ”âŸĐ )
45 44 24 33 3jca âŠĒ ( ( ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑃 ) ∧ ð‘Ķ ∈ 𝑃 ) ∧ ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ) → ( âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrG ‘ 𝐚 ) âŸĻ“ ð‘Ĩ ðĩ ð‘Ķ ”âŸĐ ∧ ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ð‘Ķ ( ðū ‘ ðĩ ) ðī ) )
46 9 necomd âŠĒ ( 𝜑 → ðķ ≠ ðĩ )
47 8 necomd âŠĒ ( 𝜑 → ðĩ ≠ ðī )
48 1 2 4 6 6 5 3 7 10 46 47 hlcgrex âŠĒ ( 𝜑 → ∃ ð‘Ĩ ∈ 𝑃 ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) )
49 1 2 4 6 6 7 3 5 10 8 9 hlcgrex âŠĒ ( 𝜑 → ∃ ð‘Ķ ∈ 𝑃 ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) )
50 reeanv âŠĒ ( ∃ ð‘Ĩ ∈ 𝑃 ∃ ð‘Ķ ∈ 𝑃 ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) ↔ ( ∃ ð‘Ĩ ∈ 𝑃 ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ∃ ð‘Ķ ∈ 𝑃 ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) )
51 48 49 50 sylanbrc âŠĒ ( 𝜑 → ∃ ð‘Ĩ ∈ 𝑃 ∃ ð‘Ķ ∈ 𝑃 ( ( ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ĩ ) = ( ðĩ ( dist ‘ 𝐚 ) ðī ) ) ∧ ( ð‘Ķ ( ðū ‘ ðĩ ) ðī ∧ ( ðĩ ( dist ‘ 𝐚 ) ð‘Ķ ) = ( ðĩ ( dist ‘ 𝐚 ) ðķ ) ) ) )
52 45 51 reximddv2 âŠĒ ( 𝜑 → ∃ ð‘Ĩ ∈ 𝑃 ∃ ð‘Ķ ∈ 𝑃 ( âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrG ‘ 𝐚 ) âŸĻ“ ð‘Ĩ ðĩ ð‘Ķ ”âŸĐ ∧ ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ð‘Ķ ( ðū ‘ ðĩ ) ðī ) )
53 1 2 4 3 5 6 7 7 6 5 iscgra âŠĒ ( 𝜑 → ( âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrA ‘ 𝐚 ) âŸĻ“ ðķ ðĩ ðī ”âŸĐ ↔ ∃ ð‘Ĩ ∈ 𝑃 ∃ ð‘Ķ ∈ 𝑃 ( âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrG ‘ 𝐚 ) âŸĻ“ ð‘Ĩ ðĩ ð‘Ķ ”âŸĐ ∧ ð‘Ĩ ( ðū ‘ ðĩ ) ðķ ∧ ð‘Ķ ( ðū ‘ ðĩ ) ðī ) ) )
54 52 53 mpbird âŠĒ ( 𝜑 → âŸĻ“ ðī ðĩ ðķ ”âŸĐ ( cgrA ‘ 𝐚 ) âŸĻ“ ðķ ðĩ ðī ”âŸĐ )