Metamath Proof Explorer

Theorem tgifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H K , with B between A and C and F between E and K . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019)

Ref Expression
Hypotheses tgbtwncgr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgbtwncgr.m ⊢ − = ( dist ‘ 𝐺 )
tgbtwncgr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgbtwncgr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwncgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwncgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwncgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgbtwncgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgifscgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgifscgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgifscgr.g ⊢ ( 𝜑 → 𝐾 ∈ 𝑃 )
tgifscgr.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
tgifscgr.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgifscgr.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 𝐼 𝐾 ) )
tgifscgr.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐸 − 𝐾 ) )
tgifscgr.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐾 ) )
tgifscgr.5 ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐻 ) )
tgifscgr.6 ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = ( 𝐾 − 𝐻 ) )
Assertion tgifscgr ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )

Proof

Step Hyp Ref Expression
1 tgbtwncgr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwncgr.m ⊢ − = ( dist ‘ 𝐺 )
3 tgbtwncgr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgbtwncgr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tgbtwncgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 tgbtwncgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 tgbtwncgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 tgbtwncgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 tgifscgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 tgifscgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 tgifscgr.g ⊢ ( 𝜑 → 𝐾 ∈ 𝑃 )
12 tgifscgr.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
13 tgifscgr.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
14 tgifscgr.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 𝐼 𝐾 ) )
15 tgifscgr.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐸 − 𝐾 ) )
16 tgifscgr.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐾 ) )
17 tgifscgr.5 ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐻 ) )
18 tgifscgr.6 ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = ( 𝐾 − 𝐻 ) )
19 4 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵 ∈ 𝑃 )
21 8 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐷 ∈ 𝑃 )
22 10 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐹 ∈ 𝑃 )
23 simpr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
24 12 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐻 ∈ 𝑃 )
25 1 2 3 19 20 21 22 23 24 tgldim0cgr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )
26 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐶 − 𝐷 ) = ( 𝐾 − 𝐻 ) )
27 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
28 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐶 ∈ 𝑃 )
29 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐵 ∈ 𝑃 )
30 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
31 simpr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
32 31 oveq1d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐴 𝐼 𝐶 ) = ( 𝐶 𝐼 𝐶 ) )
33 30 32 eleqtrd ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 𝐶 ) )
34 1 2 3 27 28 29 33 axtgbtwnid ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐶 = 𝐵 )
35 34 oveq1d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐶 − 𝐷 ) = ( 𝐵 − 𝐷 ) )
36 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐾 ∈ 𝑃 )
37 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐹 ∈ 𝑃 )
38 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐹 ∈ ( 𝐸 𝐼 𝐾 ) )
39 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐸 ∈ 𝑃 )
40 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ 𝑃 )
41 31 oveq2d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐴 − 𝐴 ) = ( 𝐴 − 𝐶 ) )
42 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐴 − 𝐶 ) = ( 𝐸 − 𝐾 ) )
43 41 42 eqtr2d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐸 − 𝐾 ) = ( 𝐴 − 𝐴 ) )
44 1 2 3 27 39 36 40 43 axtgcgrid ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐸 = 𝐾 )
45 44 oveq1d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐸 𝐼 𝐾 ) = ( 𝐾 𝐼 𝐾 ) )
46 38 45 eleqtrd ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐹 ∈ ( 𝐾 𝐼 𝐾 ) )
47 1 2 3 27 36 37 46 axtgbtwnid ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → 𝐾 = 𝐹 )
48 47 oveq1d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐾 − 𝐻 ) = ( 𝐹 − 𝐻 ) )
49 26 35 48 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 = 𝐶 ) → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )
50 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
51 50 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → 𝐺 ∈ TarskiG )
52 51 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐺 ∈ TarskiG )
53 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝑒 ∈ 𝑃 )
54 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
55 54 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → 𝐶 ∈ 𝑃 )
56 55 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐶 ∈ 𝑃 )
57 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐵 ∈ 𝑃 )
58 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝑓 ∈ 𝑃 )
59 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → 𝐾 ∈ 𝑃 )
60 59 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐾 ∈ 𝑃 )
61 10 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐹 ∈ 𝑃 )
62 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐷 ∈ 𝑃 )
63 12 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐻 ∈ 𝑃 )
64 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) )
65 64 simprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐶 ≠ 𝑒 )
66 65 necomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝑒 ≠ 𝐶 )
67 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
68 67 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐴 ∈ 𝑃 )
69 13 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
70 64 simpld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) )
71 1 2 3 52 68 57 56 53 69 70 tgbtwnexch3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑒 ) )
72 1 2 3 52 57 56 53 71 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐶 ∈ ( 𝑒 𝐼 𝐵 ) )
73 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐸 ∈ 𝑃 )
74 14 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝐾 ) )
75 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) )
76 1 2 3 52 73 61 60 58 74 75 tgbtwnexch3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐾 ∈ ( 𝐹 𝐼 𝑓 ) )
77 1 2 3 52 61 60 58 76 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐾 ∈ ( 𝑓 𝐼 𝐹 ) )
78 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) )
79 78 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐶 − 𝑒 ) = ( 𝐾 − 𝑓 ) )
80 1 2 3 52 56 53 60 58 79 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝑒 − 𝐶 ) = ( 𝑓 − 𝐾 ) )
81 16 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐾 ) )
82 1 2 3 52 57 56 61 60 81 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝐾 − 𝐹 ) )
83 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → 𝐴 ≠ 𝐶 )
84 15 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐴 − 𝐶 ) = ( 𝐸 − 𝐾 ) )
85 17 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐻 ) )
86 18 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐶 − 𝐷 ) = ( 𝐾 − 𝐻 ) )
87 1 2 3 52 68 56 53 73 60 58 62 63 83 70 75 84 79 85 86 axtg5seg ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝑒 − 𝐷 ) = ( 𝑓 − 𝐻 ) )
88 1 2 3 52 53 56 57 58 60 61 62 63 66 72 77 80 82 87 86 axtg5seg ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) ) → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )
89 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → 𝐸 ∈ 𝑃 )
90 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → 𝑒 ∈ 𝑃 )
91 1 2 3 51 89 59 55 90 axtgsegcon ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → ∃ 𝑓 ∈ 𝑃 ( 𝐾 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐾 − 𝑓 ) = ( 𝐶 − 𝑒 ) ) )
92 88 91 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) ) → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )
93 simplr ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
94 1 2 3 50 67 54 93 tgbtwndiff ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑒 ∈ 𝑃 ( 𝐶 ∈ ( 𝐴 𝐼 𝑒 ) ∧ 𝐶 ≠ 𝑒 ) )
95 92 94 r19.29a ⊢ ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )
96 49 95 pm2.61dane ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )
97 1 5 tgldimor ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
98 25 96 97 mpjaodan ⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐻 ) )