Metamath Proof Explorer

Theorem tgfscgr

Description: Congruence law for the general five segment configuration. Theorem 4.16 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
lnxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
lnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
lnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
lnxfr.d ⊢ − = ( dist ‘ 𝐺 )
tgfscgr.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
tgfscgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgfscgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgfscgr.1 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
tgfscgr.2 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
tgfscgr.3 ⊢ ( 𝜑 → ( 𝑋 − 𝑇 ) = ( 𝐴 − 𝐷 ) )
tgfscgr.4 ⊢ ( 𝜑 → ( 𝑌 − 𝑇 ) = ( 𝐵 − 𝐷 ) )
tgfscgr.5 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion tgfscgr ( 𝜑 → ( 𝑍 − 𝑇 ) = ( 𝐶 − 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 lnxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
9 lnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 lnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11 lnxfr.d ⊢ − = ( dist ‘ 𝐺 )
12 tgfscgr.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
13 tgfscgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
14 tgfscgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
15 tgfscgr.1 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
16 tgfscgr.2 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
17 tgfscgr.3 ⊢ ( 𝜑 → ( 𝑋 − 𝑇 ) = ( 𝐴 − 𝐷 ) )
18 tgfscgr.4 ⊢ ( 𝜑 → ( 𝑌 − 𝑇 ) = ( 𝐵 − 𝐷 ) )
19 tgfscgr.5 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
20 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐺 ∈ TarskiG )
21 5 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ∈ 𝑃 )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ 𝑃 )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑍 ∈ 𝑃 )
24 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐴 ∈ 𝑃 )
25 10 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐵 ∈ 𝑃 )
26 13 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐶 ∈ 𝑃 )
27 12 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑇 ∈ 𝑃 )
28 14 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐷 ∈ 𝑃 )
29 19 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ≠ 𝑌 )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
31 16 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
32 1 11 3 8 20 21 22 23 24 25 26 31 30 tgbtwnxfr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
33 1 11 3 8 20 21 22 23 24 25 26 31 cgr3simp1 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
34 1 11 3 8 20 21 22 23 24 25 26 31 cgr3simp2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑌 − 𝑍 ) = ( 𝐵 − 𝐶 ) )
35 17 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑋 − 𝑇 ) = ( 𝐴 − 𝐷 ) )
36 18 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑌 − 𝑇 ) = ( 𝐵 − 𝐷 ) )
37 1 11 3 20 21 22 23 24 25 26 27 28 29 30 32 33 34 35 36 axtg5seg ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑍 − 𝑇 ) = ( 𝐶 − 𝐷 ) )
38 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝐺 ∈ TarskiG )
39 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝑌 ∈ 𝑃 )
40 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝑋 ∈ 𝑃 )
41 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝑍 ∈ 𝑃 )
42 10 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝐵 ∈ 𝑃 )
43 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝐴 ∈ 𝑃 )
44 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝐶 ∈ 𝑃 )
45 12 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝑇 ∈ 𝑃 )
46 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝐷 ∈ 𝑃 )
47 19 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝑌 ≠ 𝑋 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) )
50 16 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
51 1 11 3 8 38 40 39 41 43 42 44 50 cgr3swap12 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ∼ ⟨“ 𝐵 𝐴 𝐶 ”⟩ )
52 1 11 3 8 38 39 40 41 42 43 44 51 49 tgbtwnxfr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )
53 1 11 3 8 38 39 40 41 42 43 44 51 cgr3simp1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ( 𝑌 − 𝑋 ) = ( 𝐵 − 𝐴 ) )
54 1 11 3 8 38 39 40 41 42 43 44 51 cgr3simp2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ( 𝑋 − 𝑍 ) = ( 𝐴 − 𝐶 ) )
55 18 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ( 𝑌 − 𝑇 ) = ( 𝐵 − 𝐷 ) )
56 17 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ( 𝑋 − 𝑇 ) = ( 𝐴 − 𝐷 ) )
57 1 11 3 38 39 40 41 42 43 44 45 46 48 49 52 53 54 55 56 axtg5seg ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ( 𝑍 − 𝑇 ) = ( 𝐶 − 𝐷 ) )
58 4 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐺 ∈ TarskiG )
59 5 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ∈ 𝑃 )
60 7 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ 𝑃 )
61 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑌 ∈ 𝑃 )
62 12 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑇 ∈ 𝑃 )
63 9 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐴 ∈ 𝑃 )
64 13 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐶 ∈ 𝑃 )
65 10 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐵 ∈ 𝑃 )
66 14 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐷 ∈ 𝑃 )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) )
68 16 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
69 1 11 3 8 58 59 61 60 63 65 64 68 cgr3swap23 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝐶 𝐵 ”⟩ )
70 1 11 3 8 58 59 60 61 63 64 65 69 67 tgbtwnxfr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
71 1 11 3 8 58 59 61 60 63 65 64 68 cgr3simp1 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
72 1 11 3 8 58 59 60 61 63 64 65 69 cgr3simp2 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑍 − 𝑌 ) = ( 𝐶 − 𝐵 ) )
73 17 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑋 − 𝑇 ) = ( 𝐴 − 𝐷 ) )
74 18 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑌 − 𝑇 ) = ( 𝐵 − 𝐷 ) )
75 1 11 3 58 59 60 61 62 63 64 65 66 67 70 71 72 73 74 tgifscgr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑍 − 𝑇 ) = ( 𝐶 − 𝐷 ) )
76 1 2 3 4 5 7 6 tgcolg ⊢ ( 𝜑 → ( ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ∨ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ∨ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ) )
77 15 76 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ∨ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ∨ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )
78 37 57 75 77 mpjao3dan ⊢ ( 𝜑 → ( 𝑍 − 𝑇 ) = ( 𝐶 − 𝐷 ) )