Metamath Proof Explorer

Theorem tgcgrxfr

Description: A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019)

Ref Expression
Hypotheses tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgcgrxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgcgrxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgcgrxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgcgrxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgcgrxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgcgrxfr.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgcgrxfr.2 ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
Assertion tgcgrxfr ( 𝜑 → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
3 tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
5 tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgcgrxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tgcgrxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tgcgrxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgcgrxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgcgrxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 tgcgrxfr.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
12 tgcgrxfr.2 ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
13 6 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐴 ∈ 𝑃 )
14 5 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
15 9 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐷 ∈ 𝑃 )
16 10 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐹 ∈ 𝑃 )
17 simpr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
18 1 2 3 14 13 15 16 17 tgldim0itv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐴 ∈ ( 𝐷 𝐼 𝐹 ) )
19 7 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵 ∈ 𝑃 )
20 8 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐶 ∈ 𝑃 )
21 1 2 3 14 13 19 15 17 13 tgldim0cgr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐴 ) )
22 1 2 3 14 19 20 13 17 16 tgldim0cgr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐵 − 𝐶 ) = ( 𝐴 − 𝐹 ) )
23 1 2 3 14 20 13 16 17 15 tgldim0cgr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
24 1 2 4 14 13 19 20 15 13 16 21 22 23 trgcgr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐴 𝐹 ”⟩ )
25 eleq1 ⊢ ( 𝑒 = 𝐴 → ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ↔ 𝐴 ∈ ( 𝐷 𝐼 𝐹 ) ) )
26 s3eq2 ⊢ ( 𝑒 = 𝐴 → ⟨“ 𝐷 𝑒 𝐹 ”⟩ = ⟨“ 𝐷 𝐴 𝐹 ”⟩ )
27 26 breq2d ⊢ ( 𝑒 = 𝐴 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐴 𝐹 ”⟩ ) )
28 25 27 anbi12d ⊢ ( 𝑒 = 𝐴 → ( ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ↔ ( 𝐴 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐴 𝐹 ”⟩ ) ) )
29 28 rspcev ⊢ ( ( 𝐴 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐴 𝐹 ”⟩ ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
30 13 18 24 29 syl12anc ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
31 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → 𝐺 ∈ TarskiG )
32 simplr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → 𝑔 ∈ 𝑃 )
33 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → 𝐷 ∈ 𝑃 )
34 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → 𝐴 ∈ 𝑃 )
35 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → 𝐵 ∈ 𝑃 )
36 1 2 3 31 32 33 34 35 axtgsegcon ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) )
37 5 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
38 32 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑔 ∈ 𝑃 )
39 38 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑔 ∈ 𝑃 )
40 9 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ 𝑃 )
41 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → 𝑒 ∈ 𝑃 )
42 41 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑒 ∈ 𝑃 )
43 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ∈ 𝑃 )
44 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) )
45 44 simpld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) )
46 simprl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) )
47 1 2 3 37 39 40 42 43 45 46 tgbtwnexch3 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑒 ∈ ( 𝐷 𝐼 𝑓 ) )
48 6 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∈ 𝑃 )
49 8 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
50 10 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ∈ 𝑃 )
51 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) )
52 51 simprd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ≠ 𝑔 )
53 52 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑔 ≠ 𝐷 )
54 1 2 3 37 39 40 42 43 45 46 tgbtwnexch ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ ( 𝑔 𝐼 𝑓 ) )
55 51 simpld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) )
56 1 2 3 37 50 40 39 55 tgbtwncom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ ( 𝑔 𝐼 𝐹 ) )
57 7 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐵 ∈ 𝑃 )
58 11 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
59 44 simprd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) )
60 simprr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) )
61 1 2 3 37 40 42 43 48 57 49 47 58 59 60 tgcgrextend ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐷 − 𝑓 ) = ( 𝐴 − 𝐶 ) )
62 12 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
63 62 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐷 − 𝐹 ) = ( 𝐴 − 𝐶 ) )
64 1 2 3 37 40 48 49 39 43 50 53 54 56 61 63 tgsegconeq ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 = 𝐹 )
65 64 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐷 𝐼 𝑓 ) = ( 𝐷 𝐼 𝐹 ) )
66 47 65 eleqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) )
67 59 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝑒 ) )
68 64 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝑒 − 𝑓 ) = ( 𝑒 − 𝐹 ) )
69 60 68 eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝑒 − 𝐹 ) )
70 1 2 3 5 6 8 9 10 12 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
71 70 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
72 1 2 4 37 48 57 49 40 42 50 67 69 71 trgcgr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ )
73 66 72 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
74 31 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
75 35 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
76 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → 𝐶 ∈ 𝑃 )
77 1 2 3 74 38 41 75 76 axtgsegcon ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → ∃ 𝑓 ∈ 𝑃 ( 𝑒 ∈ ( 𝑔 𝐼 𝑓 ) ∧ ( 𝑒 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) )
78 73 77 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) ) → ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
79 78 ex ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) ∧ 𝑒 ∈ 𝑃 ) → ( ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) → ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) )
80 79 reximdva ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → ( ∃ 𝑒 ∈ 𝑃 ( 𝐷 ∈ ( 𝑔 𝐼 𝑒 ) ∧ ( 𝐷 − 𝑒 ) = ( 𝐴 − 𝐵 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) ) )
81 36 80 mpd ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑔 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
82 5 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐺 ∈ TarskiG )
83 10 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐹 ∈ 𝑃 )
84 9 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐷 ∈ 𝑃 )
85 simpr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
86 1 2 3 82 83 84 85 tgbtwndiff ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑔 ∈ 𝑃 ( 𝐷 ∈ ( 𝐹 𝐼 𝑔 ) ∧ 𝐷 ≠ 𝑔 ) )
87 81 86 r19.29a ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )
88 1 6 tgldimor ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
89 30 87 88 mpjaodan ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝑒 𝐹 ”⟩ ) )