Metamath Proof Explorer

Theorem tgcgrextend

Description: Link congruence over a pair of line segments. Theorem 2.11 of Schwabhauser p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019) (Shortened by David A. Wheeler and Thierry Arnoux, 22-Apr-2020.)

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

Proof

Step Hyp Ref Expression
1 tkgeom.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d ⊢ − = ( dist ‘ 𝐺 )
3 tkgeom.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tgcgrextend.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 tgcgrextend.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 tgcgrextend.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 tgcgrextend.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 tgcgrextend.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 tgcgrextend.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 tgcgrextend.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
12 tgcgrextend.2 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
13 tgcgrextend.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
14 tgcgrextend.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
17 16 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 − 𝐶 ) = ( 𝐵 − 𝐶 ) )
18 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
19 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑃 )
21 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐷 ∈ 𝑃 )
22 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐸 ∈ 𝑃 )
23 13 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
24 1 2 3 18 19 20 21 22 23 16 tgcgreq ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐷 = 𝐸 )
25 24 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐷 − 𝐹 ) = ( 𝐸 − 𝐹 ) )
26 15 17 25 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
27 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
28 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ∈ 𝑃 )
29 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
30 10 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐹 ∈ 𝑃 )
31 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 ∈ 𝑃 )
32 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
33 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐸 ∈ 𝑃 )
34 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
35 11 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
36 12 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
37 13 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
38 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
39 1 2 3 27 29 31 tgcgrtriv ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐴 ) = ( 𝐷 − 𝐷 ) )
40 1 2 3 27 29 32 31 33 37 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
41 1 2 3 27 29 32 28 31 33 30 29 31 34 35 36 37 38 39 40 axtg5seg ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
42 1 2 3 27 28 29 30 31 41 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
43 26 42 pm2.61dane ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )